The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac 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"? 

Synthetic homotopy theory means homotopy theory developed without real numbers and analytic homotopy theory means homotopy developed using real numbers. The same terminology apply to geometry. 

You can do analytic homotopy theory in HoTT, just repeating ZFC ideas and using the real numbers in HoTT. On the other hand, this is absurd from the point of view of formal verification as it was already remarked by Voevodsky in one of his lectures.

2018-05-27 17:50 GMT+02:00 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!