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...