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
Chronological Thread
- From: Cody Roux <cody.roux AT andrew.cmu.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq
- Date: Wed, 08 Jan 2014 14:08:36 -0500
On 01/08/2014 01:34 PM, Frédéric Blanqui wrote:
>
> Where n, m are natural numbers (the "skeleton" of List). I think I can
> define such a modified inductive type for every instance of inductive
> definitions in Coq. This would certainly revert us back to the sinless
> state desired by Thorsten and Vladimir, while preserving the paradise
> offered by the relaxed guard condition.
> Including strictly positive inductive types, that is, with constructors
> taking functions as recursive arguments?
Well there's the rub :), I haven't worked it out for such types yet. I
think it's possible though, given the appropriate "skeleton" (which
would be a "Brower-type" ordinal) and the right notion of "less-than".
The harder question is: what kind of proof irrelevance is needed?
Surely more research is needed.
Best,
Cody
>> About K: Coq has managed to describe a pattern-match which does not
>> allow it (by making less unification information available in the
>> branches), and I don't think it's that relevant to the problem at hand,
>> which is mostly concerned about when a term is a subterm of another.
>>
>> Best,
>>
>>
>> Cody
>>
>>> All the best,
>>>
>>> - -- Jean.
>>>
>>>
>>> -----BEGIN PGP SIGNATURE-----
>>> Version: GnuPG/MacGPG2 v2.0.18 (Darwin)
>>> Comment: GPGTools - http://gpgtools.org
>>> Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
>>>
>>> iQEcBAEBAgAGBQJSzY/DAAoJEBO3J6HB7Rh1WyUH/3uim2ZTsfzddH0gbCngNeFu
>>> vqnvXmd8VPKNoH4LE9Ydhi2J4ibCmnyPH2sFi1ee6t5Kt9Oz8GhOc7HzRdlB2qsq
>>> GpD+lxDE8I9HdokfDyYnP2RP2ZiUs2/2m1bcAJkWVZLwlcKyKiwr/yzY/lNdSIRS
>>> J/YYIXMI/wCw1b38ZoFXvaa0okOS8IDDde2W1lybvRSO0F1ZO6qMzWwas5hD78mC
>>> FU8MeU7xYvWOv30GRyYEl0PaUswCmmGhvVqZDH0Ttum2ONnQpQ9JhMKB6AaVZQu/
>>> hB7/PE8vOXCFLBUMkBTfn/R655VHbs87tytgMLKE5Q+eMs5hA7u3lfEMIzzP+io=
>>> =JLKR
>>> -----END PGP SIGNATURE-----
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, (continued)
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Altenkirch Thorsten, 01/07/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Martin Escardo, 01/07/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Vladimir Voevodsky, 01/07/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Matthieu Sozeau, 01/07/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Prof. Robert Harper, 01/07/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Vladimir Voevodsky, 01/07/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Jean Goubault-Larrecq, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Frédéric Blanqui, 01/08/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/08/2014
- Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Matthieu Sozeau, 01/08/2014
- Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Frédéric Blanqui, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Altenkirch Thorsten, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Matthieu Sozeau, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Conor McBride, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Bruno Barras, 01/09/2014
- RE: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Nikhil Swamy, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Cody Roux, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Andreas Abel, 01/09/2014
- Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq, Jorge Luis Sacchini, 01/10/2014
Archive powered by MHonArc 2.6.18.