2 ms·
Coq isn't based on HoTT, however, the people working on HoTT use a modified version of Coq in conjunction with a library that contains the essential elements. h
by chas 13y ago
Coq isn't based on HoTT, however, the people working on HoTT use a modified version of Coq in conjunction with a library that contains the essential elements. https://github.com/HoTT/HoTT https://github.com/HoTT/HoTT
- nardi 13y agoThe lightbulb moment for Voevodsky was apparently realizing that CoC (used in Coq) is almost entirely equivalent to HoTT. So in a sense, Coq actually is kind of based on HoTT, just using different words. (One could maybe say there is a homotopy between CoC and HoTT?? IANAM.) The library they are developing is basically a restatement of HoTT in Coq using more familiar terms/concepts.