A general definition of dependent type theories

TL;DR

This paper introduces a broad, syntax-based framework for dependent type theories, unifying various existing theories and ensuring their well-behavedness through formalised metatheorems in Coq.

Contribution

It provides a general, syntax-oriented definition of dependent type theories, unifying and organizing their study with formal proofs of key properties.

Findings

Framework encompasses Martin-Löf's type theories and variants

Metatheorems hold in the general class of theories

Formalised proofs in Coq

Abstract

We define a general class of dependent type theories, encompassing Martin-L\"of's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive reading of syntax, yielding the traditional presentations of specific theories as closely as possible. Specifically, we give three main definitions: raw type theories, a minimal setup for discussing dependently typed derivability; acceptable type theories, including extra conditions ensuring well-behavedness; and well-presented type theories, generalising how in traditional presentations, the well-behavedness of a type theory is established step by step as the type theory is built up. Following these, we show that various fundamental fitness-for-purpose metatheorems hold in this generality. Much of the present work has been formalised in the proof assistant Coq.