Guillaume Brunerie: A proof sketch for the initiality conjecture

Abstract 

The initiality conjecture states that given a type theory, the syntactic model forms an initial object in the category of models of this type theory.

This fact is often assumed to be obvious and is rarely proved in detail. For instance it is implicitly assumed in order to show that there is a canonical way to interpret the syntax of type theory in any given model. However, there are many technical details that need to be taken care of in the proof, and it is not even clear what the precise
statement of the initiality conjecture is. What is a type theory? What is a model? What is the syntactic model?

This was particularly emphasized by Vladimir Voevodsky who couldn’t find any proof of the initiality conjecture in the literature that would apply to Martin-Löf type theory and allow for extensions like his resizing rules.

In this talk I will present work in progress on this problem. I will define a class of type theories general enough to allow for many variants of dependent type theory, and sketch the definition of the category of models, the definition of the syntactic model, and the proof of initiality.