The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,

I think you are right and in these kind of examples having
universe polymorphism or not will make a big difference.

Note however that, AFAIK, universe polymorphism deals
with the way constants are treated. I think it means that
each *occurence* of a constant comes with its own set of
universe indices.

So if you have universe polymorphism you can prove surprising
statements like  "A is not equal to A" (for a well-chosen constant A).
(of course you can also prove A=A, but if you try to combine the two
proofs, then you get a universe inconsistency)


Now, in the example you give, you want also each occurence
of the *inductive type* Category to come with its own set of indices.
So one should check whether this last feature does not generate
more complex constraints on the indices. I have no idea whether
this feature has been studied or implemented.

Maybye it was done for Lego ?


Cheers,


Benjamin






Le 17 avr. 07 à 22:07, Lauri Alanko a écrit :

> On Sun, Apr 15, 2007 at 08:10:17AM -0700, Adam Chlipala wrote:
> > You can often get around this by turning on -impredicative-set and  
> > using
> > Set in place of Type.  You get the restrictions on elimination of  
> > large
> > inductive types, but often you can work around them.
>
> Alas, I fear the restrictions are crucial.
>
> The classical example is when trying to formalize category theory in
> the Aczel-Huet-Saïbi style. We define a category:
>
>         Structure Category : Type := {
>           Ob : Type;
>           Hom : Ob -> Ob -> Setoid;
>           (* id, compose and proofs *)
>         }.
>
> and functors and their equivalence and build a setoid on them:
>
>         Structure Functor (C D : Category) : Setoid := ... ;
>
> and then we find out, wow, categories and functors form a category:
>
>         Definition CAT : Category := Build_Category Category Functor ...;
>         
> and at this point we stumble into universe inconsistency.
>
> Impredicative sets obviously won't help, since we want to be able to
> extract the Ob type from a category.
>
>
> To answer Pierre Courtieu's question, my understanding of universe
> polymorphism is that it means that instead of each occurrence of Type
> having a fixed universe, all terms are parameterized by a
> universe. Currently, if I write:
>
> Structure T : Type := { t : Type }.
>
> The real internal types for the terms are (using OCaml's underscore
> syntax for uninstantiated variables):
>
>       T : Type (_u + 1)
> Build_T : Type _u -> T
>       t : T -> Type _u
>
> So if I now try to type the term (Build_T T), the constraint
> (_u + 1 <= _u) fails, so there's no way to instantiate _u and we get
> the universe inconsistency.
>
> With universe polymorphism, my understand is that the universe
> variables would get internally generalized:
>
>       T : forall u, Type (u + 1)
> Build_T : forall u, Type u -> T u
>       t : forall u, T (u + 1) -> Type u
>
> And (Build_T T) would be translated
>
> fun u -> Build_T (u + 1) (T u) : forall u, T (u + 1)
>
> Now the same constructions can be used in different universes,
> something that's needed if we want to speak of "the category of all
> categories" since we really mean "the u+1-category of all
> u-categories".
>
> This is just my hazy understanding of the situation, I have only
> glanced at Harper and Pollack's paper where the idea originated.
>
>
> Lauri
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club