Models of dependent type theory from algebraic weak factorisation systems

Dr Nicola Gambino, University of Leeds. Part of the Proofs, Constructions and Computations Seminar Series.

Constructing models of dependent type theory is hard: one needs to find a category with sufficient structure and then find a way to turn this category into an ‘honest’ model of the logical system, in which certain strictness conditions are required to hold. Dr Nicola Gambino will report on a new method for constructing models, based on the notion of an algebraic weak factorisation system. Several examples of models fit into this framework. This is based on joint work with Marco Federico Larrea.