Martin Escardo | 8 Mar 01:27 2014


I would like to advertise a concise approach to get type theory to eat
itself, by Chuangjie Xu and myself, written in Agda, in which type
theory is formulated without definitional equalities:

You may prefer to look at the version without any comments (or very few):

Many people have thought hard about this problem, both theoretically
and in practice in Agda. Mike Shulman recently wrote a nice post,
adapted to HoTT, with such ideas and also his own ideas:

   Homotopy Type Theory should eat itself
   (but so far, it's too big to swallow)

Here we don't consider HoTT. Only down to earth dependent type theory.

We do away with judgmental equalities in our (Agda-formulated)
presentation of the syntax of type theory. We replace them by
"syntactic transport maps" These are not functions, but rather term
constructors T. The interpreation of a term T u, defined in Agda, is
definitionally equal to that of u (the proof of this fact is refl).

The important point, compared to previous work, is that we don't need
to have a notion of definitional equality (in the syntax) to define
these transport (or coercion) maps. Thus, we have a formulation of
(intensional!) type theory (written in Agda) without definitional