Hacker News Reader

I got lost on one basic thing. I thought Coq wasn't based on HoTT. I thought Agda was based on Martin-Lof; Coq was based on calculus of constructions, and that would mean that the HoTT people are looking to develop a new proof assistant that is based on HoTT. Is that true?

View on HN

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

The 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.

Reply on news.ycombinator.com