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: Vladimir Voevodsky <vladimir AT ias.edu>
To: Cody Roux <cody.roux AT andrew.cmu.edu>
Cc: Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>, Maxime Dénès <mail AT maximedenes.fr>, "homotopytypetheory AT googlegroups.com" <homotopytypetheory AT googlegroups.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: Wed, 8 Jan 2014 14:55:58 -0500

On Jan 8, 2014, at 12:40 PM, Cody Roux
<cody.roux AT andrew.cmu.edu>
wrote:
>>

> That's fair, but I don't see why eliminators have a more powerful
> ontological status than sized-types. They require work to be derived as
> well, and the correctness proofs for them are quite similar to that for
> sized types. This seems like a matter of preference. Obviously I'm not
> neutral in this matter though.
>
> Best,
>
> Cody
>

In the case of the univalent model eliminators are better because I have
invested a lot of effort into checking that they are compatible with the
model (some details of it are at the end of my "Notes on Type Systems").

No other work of this kind has been done as far as I know.

Vladimir.

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