Changed the quoted text to a paraphrase with a couple changes based on the nforum discussion.
]]>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]
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?
]]>András Kovács here claims to see some value in the proof.
]]>I wonder if there’s anything in the proof of broader significance than merely establishing the result.
]]>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.
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?
]]>pointer to the recent proof (the thesis and the announcements)
]]>