[Agda] Autophagia

[Martin Escardo]

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:

http://www.cs.bham.ac.uk/~mhe/TT-perhaps-eating-itself/TT-perhaps-eating-itself.html

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

http://www.cs.bham.ac.uk/~mhe/TT-perhaps-eating-itself/TT-perhaps-eating-itself-without-comments.html

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)

   http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/

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
equality.

Martin