Peter LeFanu Lumsdaine: A general definition of dependent type theories.

Abstract: We propose a general definition of (syntactic presentations of) *type theories* which yields, as instances, Martin-Löf’s various type theories (intensional, extensional, …) and their various later extensions by further type- and term-formers — inductive families, inductive-recursive types à la Dybjer/Setzer, the various higher inductive types of Homotopy Type Theory, and so on.

The novelty compared to existing approaches (logical frameworks, …) is that it yields not some embedded counterpart of a theory, whose equivalence with the original theory may be non-trivial, but literally the original type theory itself as it would typically be presented in a paper.

The need for such a framework has been sorely felt recently, since without one, theorems in the meta-theory of type theory can be stated and proved only for specific type theories (usually just small toy examples), not in the natural generality in which they are believed to hold.

It is a truism of implementation that fully precise definitions of type theories are so large and intricate as to be almost impossible to get right without extensive debugging — almost (though not quite) all presentations in the prose literature contain some errors (usually minor).  To this end, we are formalising the present definition in Coq, to give confidence in its rigour and fitness-for-purpose.