Skip to Content.
Sympa Menu

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

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-----




Archive powered by MHonArc 2.6.18.

Top of Page