Email Gateway (Aug 22 2022 at 18:00): Email Gateway (Aug 22 2022 at 18:00):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
As far as I know, there are two approaches to homotopy type theory: UniMath and HoTT. HoTT uses all CIC, but UniMath, which was Voevodsky’s approach, only uses the Martin-Lof part of CIC and they avoid, as an informal convention among users, the problematic parts of CIC according to Voevodsky’s system.
Voevodsky said in an interview (available in his website) that he learned Isabelle very quickly, but he experienced a very hard time with Coq. Why he used Coq in place of Isabelle? Maybe Voevodsky did not know about the existence of Isabelle/CTT and he used Coq as a temporary solution for his UniMath library. Anyway, Voevodsky’s main contribution to the foundations of mathematics, the so-called synthetic homotopy, is independent of Coq in the same sense that Euclidean Geometry is independent of Coq.
Jose M.
Last updated: Apr 24 2024 at 08:20 UTC