Algebraic Presentations of Dependent Type Theories

Abstract

In this paper, we propose an abstract definition of dependent type theories as essentially algebraic theories. One of the main advantages of this definition is its composability: simple theories can be combined into more complex ones, and different properties of the resulting theory may be deduced from properties of the basic ones. We define a category of algebraic dependent type theories which allows us not only to combine theories but also to consider equivalences between them. We also study models of such theories and show that one can think of them as contextual categories with additional structure.