The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

To make sure I understand the terminology, synthetic in the sense of, "lets us take points, functions, loops, homotopy and whatnot as our basic elements and build from there", rather than "lets start with ZFC and construct homotopy"?

Thanks.

On Sun 27 May, 2018, 20:37 José Manuel Rodriguez Caballero, <josephcmac AT gmail.com> wrote:

Siddharth said

I do not understand why there has been an explosion of interest in HoTT, when it seems to me that CIC can do whatever HoTT can?

One of the more interesting features of HoTT is that it allows to do synthetic homotopy theory.

Is possible to do synthetic homotopy theory in CiC without introducing new axioms, just like it is done in HoTT? Are there some essential differences?

--

Sending this from my phone, please excuse any typos!