Peter LeFanu Lumsdaine: Towards a general meta-theory of dependent type theories

Abstract: This talk is an update on work in progress with Andrej Bauer and Philipp Haselwarter, on formulating and formalising a general definition of dependent type theories which is:

- *direct*, yielding specific theories roughly as one would naïvely present them, not embedded in a logical framework or other larger system;

- *general* enough to cover many important type theories, including Martin-Löf’s original theories and extensions of them by further type-constructors (e.g. inductive-recursive and higher inductive types);

- *controlled* enough to allow many fundamental meta-theorems to be stated and proved, from basics such as derivability of presuppositions and uniqueness of typing, up to (conjecturally) initiality for categorical semantics.

We have now formalised the definition in Coq (and are working on proving the first metatheorems). I’ll present and discuss the definition, and discuss the specific challenges involved in formalising it.

I previously spoke about this project in the seminar in February 2017.