Abstract

In the last few years, several authors have proposed quite general definitions of dependent type theories. Previously this has been a major gap in the literature; a good such definition should allow a more unified study of type theories and their models, with theorems and constructions given in a precise and broad generality, instead of (as currently) given for specific individual type theories, and adapted to others as needed, with their range of applicability understood at best heuristically.

With several proposals now available, the stage is set to develop and compare them. The main proposals so far are:

- Uemura (arXiv:1904.04097) gives an abstract categorical definition, categories with representable maps, together with several syntactic definitions, and a fruitful ∞-categorical generalisation.

- Bauer–Haselwarter–Lumsdaine (arXiv:2009.05539) give a concrete syntactic definition (based on Fiore-Plutkin-Turi or similar syntax with binding), and have formalised this definition in Coq. A similar definition was independently given by Brunerie (unpublished).

- Isaev (arXiv:1602.08504) gives an essentially-algebraic definition

I will concisely present these definitions, and survey the connections between them.