Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Martin Escardo <m.escardo-dxBOTFGcEFw2EctHIo1CcQ <at> public.gmane.org>
Subject: Autophagia
Newsgroups: gmane.comp.lang.agda
Date: Saturday 8th March 2014 00:27:29 UTC (over 2 years ago)
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
 
CD: 4ms