coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- Cc: Jason Gross <jasongross9 AT gmail.com>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Partially applied types and sort-polymorphism
- Date: Fri, 3 Aug 2012 06:48:24 -0400
- Envelope-to: aspiwack AT lix.polytechnique.fr, jasongross9 AT gmail.com, coq-club AT inria.fr
May be this would help. In the Univalent Foundations library I routinely had to deal with two universe levels (originally with three). I wrote all the constructions which used only one universe in file uu.v where at the start one introduces a universe by
Definition UU:=Type.
and then works consistently with this UU. Then made copies of this file uu0, uu1, uu2. When I need two universes I import uu0 and uu1 and introduce notations
Notation UU0: = uu0.UU .
Notation UU1 := uu1.UU .
and then consistently use these two universes. Then, if really needed one can make several copies of the files with two-level universe hierarchies and import them to the ones using three levels.
It is certainly better than to use the opaque and messy universe management of Coq.
Vladimir.
. Then created copies of this file
On Aug 3, 2012, at 5:55 AM, Arnaud Spiwack wrote:
Well, that doesn't really make sense on the logic side of the world. So I'm guessing it's just a printing issue? If so there is no such thing, though it may be possible to implement (I'm not familiar with this side of the system). I find it somewhat worrying though, that we would need such a large amount of apparently situational featurettes for Coq to be useable. We seem to rely on trickery most of the time. Though maybe controlling what shows on a goal makes sense. I wouldn't know.
ArnaudOn 3 August 2012 11:34, Jason Gross <jasongross9 AT gmail.com> wrote:Thanks, but that's not quite what I'm looking for, unless I'm mis-understanding it; I'm looking for some way to reduce the size of my proof goals by eliminating unnecessary arguments (rather than reduce how much I have to type to define them, which seems to be what [Generalizable All Variables] does). For example, it would be nice if I could not have to say that a natural transformation was of typeNaturalTransformation : forall objC homC (C : @Category objC homC) objD homD (D : @Category objD homD), @Functor objC homC C objD homD D -> @Functor objC homC C objD homD D -> Typeand instead say that a NaturalTransformation was of typeNaturalTransformation : forall (C : @Category _ _) (D : @Category _ _), @Functor C D -> @Functor C D -> TypeI realize that I can do
NaturalTransformation : forall `(F G : @Functor objC homC C objD homD D), Typeand while this is useful, it does not reduce the size of my proof goals (because it simply de-sugars to the first form that I typed).I guess I'm looking for something like telling Coq that the internal representation of [NaturalTransformation] should be something like [forall `(F G : @Functor objC homC C objD homD D), Type], but that Coq shouldn't carry around the types of all the arguments to [Functor], or something like that.-JasonOn Fri, Aug 3, 2012 at 2:55 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:
Not exactly what you want. But close enough:
http://coq.inria.fr/doc/Reference-Manual004.html#@command88On 2 August 2012 22:40, Jason Gross <jasongross9 AT gmail.com> wrote:Hi,I'm trying to encode some category theory in Coq, and have run in to problems with comma categories; I'm passing around objects and hom sets as arguments to everything, because I need to be able to deal with functors from the category of functors between two categories, and for this I'm making using of sort-polymorphism. However, my sort-polymorphic comma category construction routinely gives me goals of ~300,000 terms (thank goodness for the ability to hide implicit arguments), and operating on these goals takes a long time.Is there any support (either in the literature, in theory, in the works for Coq, or elsewhere) for talking about "partially applied types" without talking about their arguments, and having these types carry around their universe level?For example, say I haveParameter Category : forall (obj : Type) (hom : obj -> obj -> Type), Type.currently, I could haveParameter Functor : forall objA homA objB homB, @Category objA homA -> @Category objB homB.I'd like to instead be able to do something likeParameter Functor : @Cateogry _ _ -> @Category _ _.so that the [Functor] does not carry around the information of objects and hom-sets with it. I can do this by saying something likeRecord Category' := { obj : Type; hom : obj -> obj -> Type; Cat : @Category obj hom }.but this [Category'] is not universe polymorphic, and so any [Functor]s that I build with it all live at the same universe-level.Thanks.-Jason
- [Coq-Club] Partially applied types and sort-polymorphism, Jason Gross, 08/02/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Arnaud Spiwack, 08/03/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Jason Gross, 08/03/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Arnaud Spiwack, 08/03/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Vladimir Voevodsky, 08/03/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Adam Chlipala, 08/03/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Jason Gross, 08/06/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Adam Chlipala, 08/06/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Jason Gross, 08/06/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Arnaud Spiwack, 08/03/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Jason Gross, 08/03/2012
- Re: [Coq-Club] Partially applied types and sort-polymorphism, Arnaud Spiwack, 08/03/2012
Archive powered by MHonArc 2.6.18.