Contents

category theory

# Contents

## Idea

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.

## References

Proof of the initiality conjecture for the calculus of constructions is due to:

• Thomas Streicher, Chapter 4 of: Semantics of type theory – Correctness, completeness and independence results, Progress in Theoretical Computer Science, Birkhäuser Boston, Inc., Boston, MA, 1991, xii+298 pp., (ISBN:0-8176-3594-7, doi:10.1007/978-1-4612-0433-6)

Relevance of proof of more general versions of the conjecture was amplified in:

• 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:

A full proof of the initiality conjecture for full Martin-Löf type theory, formalized in Agda, is given/announced in:

Last revised on September 5, 2020 at 05:09:38. See the history of this page for a list of all contributions to it.