In this mini-course, I will survey the use of categorical/algebraic structures in modelling type theories.

In the first lecture, I’ll introduce contextual categories and related structures, and show how they are used to construct and analyse concrete models of type theory, with the set and groupoid models as detailed illustrations.

In the second, I will discuss coherence problems/theorems and their impact on constructing abstract models; sketch the Clairambault–Dybjer equivalence between extensional type theories and locally cartesian closed categories; and survey the known homotopy-theoretic models.