natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The initiality conjecture in type theory states that the term model of a type theory should be an initial object in the category of models of that type theory. Initiality guarantees that the relation between type theory and category theory works as expected, hence that formal syntactical proofs in type theory match theorems in categories that interpret these type theories.
A careful proof of initiality for the special case of the calculus of constructions was given in Streicher 91. Since then, initiality for more complex type theories (such as Martin-Löf dependent type theory) has often been treated as established, as a straightforward extension of Streicher’s result, but never written up carefully for a larger theory.
Around 2010, various researchers (notably Voevodsky 15, 16, 17) raised the question of whether these extensions really were sufficiently straightforward to consider them established without further proof. Since then, views on the status of initiality have varied within the field; but the issue has been, at least, a frustrating unresolved point.
A proof of the initiality conjecture for a full-featured Martin-Löf type theory is given/announced in de Boer 20, Brunerie-Lumsdaine 20.
(text adapted from Brunerie-Lumsdaine 20)
A proof of the initiality conjecture for Martin-Löf dependent type theory is implicit in the proof of its generalized algebraic semantics (for more on this see Uemura 2019/21 below), due to:
John Cartmell, Generalised Algebraic Theories and Contextual Categories, PhD thesis, Oxford University (1978) [pdf]
John Cartmell, Generalised Algebraic Theories and Contextual Categories, Annals of Pure and Applied Logic, 32 (1986) 209-243 [doi:10.1016/0168-0072(86)90053-9]
Proof of the initiality conjecture for the calculus of constructions:
Relevance of proof of more general versions of the conjecture was amplified in:
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.
Vladimir Voevodsky, Mathematical theory of type theories and the initiality conjecture, April 2016 (pdf, pdf)
Vladimir Voevodsky, Models, Interpretations and the Initiality Conjecture, talk at Special session on category theory and type theory in honor of Per Martin-Löf on his 75th birthday, August 17–19, 2017, during the Logic Colloquium 2017, pdf)
Early status reports on the full proof appeared in:
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)
A full proof of the initiality conjecture for full Martin-Löf type theory, formalized in Agda, is given/announced in:
Guillaume Brunerie (with Menno de Boer, Peter Lumsdaine, Anders Mörtberg), A formalization of the initiality conjecture in Agda, talk at HoTT 2019, Pittsburgh (pdf)
Menno de Boer, A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory, Stockholm 2020 (diva2:1431287, pdf)
Guillaume Brunerie, Peter LeFanu Lumsdaine (joint with Menno de Boer, Anders Mörtberg), Initiality for Martin-Löf type theory, Homotopy Type Theory Electronic Seminar Talks, Sept 10, 2020
and in
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) [pdf, hdl:11245.1/41ff0b60-64d4-4003-8182-c244a9afab3b]
most of those who believed initiality to remain unresolved have been convinced by Taichi Uemura’s doctoral thesis, which gives a more detailed alternative to Cartmell’s 1978 proof for a more structured class of theories called second-order generalized algebraic theories — a class that includes homotopy type theory, cubical type theory, and many other type theories. [Paraphrased from a comment by Jon Sterling, Jul 19, 2022]
Last revised on July 22, 2022 at 11:34:17. See the history of this page for a list of all contributions to it.