Models of Dependent Type Theory from Algebraic Weak Factorisation Systems

The main purpose of this dissertation is to analyse the extent to which algebraic weak factorisation systems provide models of Martin-L ̈of dependent type theory. To this end, we develop the notion of a type-theoretic awfs; this is a category equipped with an algebraic weak factorisation system and some additional structure, such that after performing a splitting procedure, a model of Martin-L ̈of dependent type theory is obtained. We proceed to construct examples of such type-theoretic awfs’s; first in the category of small groupoids, which produces the Hofmann and Streicher groupoid model. Later we make use of the machinery of uniform fibrations of Gambino and Sattler to produce type-theoretic awfs’s in Grothendieck toposes equipped with an interval object satisfying some additional properties; from this we obtain concrete examples in the categories of simplicial sets and cubical sets. We also study the notion of a normal uniform fibration, a strengthening of the notion of a uniform fibration, which allows us to address a question regarding the constructive nature of type-theoretic awfs’s. In addition, we show that the procedure of constructing type-theoretic awfs’s from uniform fibrations is functorial, thus providing a method for comparing models of dependent type theory.