In this licentiate thesis we present a proof of the initiality conjecture for Martin-Löf’s type theory with 0, 1, N, A+B, ∏_AB, ∑_AB_, Id_A(u,v), countable hierarchy of universes (U_i)_iєN closed under these type constructors and with type of elements (EL_i(a))_iєN. We employ the categorical semantics of contextual categories. The proof is based on a formalization in the proof assistant Agda done by Guillaume Brunerie and the author. This work was part of a joint project with Peter LeFanu Lumsdaine and Anders Mörtberg, who are developing a separate formalization of this conjecture with respect to categories with attributes and using the proof assistant Coq over the UniMath library instead. Results from this project are planned to be published in the future.

We start by carefully setting up the syntax and rules for the dependent type theory in question followed by an introduction to contextual categories. We then define the partial interpretation of raw syntax into a contextual category and we prove that this interpretation is total on well-formed input. By doing so, we define a functor from the term model, which is built out of the syntax, into any contextual category and we show that any two such functors are equal. This establishes that the term model is initial among contextual categories. At the end we discuss details of the formalization and future directions for research. In particular, we discuss a memory issue that arose in type checking the formalization and how it was resolved.