Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added these pointers to earlier status reports on the project:
Andrej Bauer (with Philipp Haselwarter and Peter Lumsdaine), Toward an initiality theorem for general type theories, talk at Types, Homotopy Type theory, and Verification, June 2018 (abstract, video recording)
Peter LeFanu Lumsdaine (joint with Menno de Boer, Guillaume Brunerie , Anders Mörtberg), Formalising the initiality conjecture in Coq, Göteborg–Stockholm Joint Type Theory Seminar, December 2018 (pdf)
Are there earlier ones?
added this pointer and quote:
Vladimir Voevodsky, HoTT is not an interpretation of MLTT into abstract homotopy theory, Jan 2015
Peter Lumsdaine (13 January 2015):
I am still confident that initiality (for MLTT, and other specific type theories) is a straightforward extension of Streicher’s proof. But I no longer feel that confidence justifies treating it as proven. We can’t be certain that it’s as straightforward as we think it is until someone has actually written it out — carefully, correctly, and publicly, so that multiple sets of eyes can check for errors.
I wonder if there’s anything in the proof of broader significance than merely establishing the result.
András Kovács here claims to see some value in the proof.
1 to 5 of 5