coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Partially applied types and sort-polymorphism
- Date: Thu, 2 Aug 2012 16:40:16 -0400
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 have
Parameter Category : forall (obj : Type) (hom : obj -> obj -> Type), Type.
currently, I could have
Parameter Functor : forall objA homA objB homB, @Category objA homA -> @Category objB homB.
I'd like to instead be able to do something like
Parameter 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 like
Record 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.