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.
I have finally removed the word “(upcoming)” from the talk announcement Brunerie & Lumsdaine 2020.
But has there meanwhile been any publication beyond de Boer 2020?
I have added these pointers:
Taichi Uemura, A General Framework for the Semantics of Type Theory [arXiv:1904.04097, talk slides: pdf]
Taichi Uemura, Abstract and concrete type theories, PhD thesis (2021) [hdl:11245.1/41ff0b60-64d4-4003-8182-c244a9afab3b, pdf]
and this comment:
all the the main hold-outs who believed initiality to remain unresolved have been all convinced by Taichi Uemura’s doctoral thesis, which gives a more detailed and mathematically satisfactory alternative to Cartmell’s 1978 proof for a broader class of theories — a class that includes homotopy type theory, cubical type theory, and many other type theories. [Jon Sterling, Jul 19, 2022]
1 to 8 of 8