8 Mar 01:27 2014

## Autophagia

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