coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

From: Andreas Abel <andreas.abel AT ifi.lmu.de>
To: Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>, Conor McBride <conor AT strictlypositive.org>
Cc: Maxime Dénès <mail AT maximedenes.fr>, Abhishek Anand <abhishek.anand.iitg AT gmail.com>, coq-club Club <coq-club AT inria.fr>, "agda AT lists.chalmers.se" <agda AT lists.chalmers.se>
Subject: Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq
Date: Thu, 09 Jan 2014 20:09:08 +0100

On 09.01.2014 11:36, Altenkirch Thorsten wrote:

P.S. In our old foetus paper we also define an untyped structural ordering
on terms.

Yes, and we proved it well-founded, but only in a simply-typed setting. I think this makes the difference: The lack of rigorous meta-theory of MLTT with pattern matching and structural recursion.

Cheers,
and a belated happy new year,

Andreas

--
Andreas Abel <>< Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/

Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, (continued)