The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

Dear Hugo,

This seems like a sensible idea. I do not see any problems with it (yet).
Thanks for the explanation!

Recently, while developing some simple category theory, we ran into a universe
inconsistency while working with the category of all categories.
(Perhaps we should have been using higher categories, but alas).
It seems that this could have been avoided if Definitions could be
universe polymorphic.
Are there any plans to change this?
Do you want me to try and make a minimal test case?

Best,

Bas


On Wed, Jan 20, 2010 at 7:08 PM, Hugo Herbelin 
<Hugo.Herbelin AT inria.fr>
 wrote:
> Hi Bas,
>
>> I recently learned that the Coq sort hierarchy has changed. Prop is
>> now a subsort of Set.
>>
>> Could anyone tell me about the reasons for this change and its
>> theoretical motivations?
>
> The practical motivation of this change is to have that the sorts
> assigned to sort-polymorphic inductive types are linearly ordered,
> and, in particular that whenever a sort-polymorphic type is set at
> some level Prop, predicative Set or Type(i), then it is also in all
> levels above.
>
> Before we had
>
>    Prop : Type0 : Type1 : ...
>    Set  : Type0 : Type1 : ...
>
> with the inclusions
>
>    Prop < Type0 < Type1 < ...
>    Set  < Type0 < Type1 < ...
>
> This meant that a sort-polymorphic inductive type on which no
> level constraints applied like
>
>  Inductive unit := tt
>
> could not be seen as a Set if placed in Prop as the absence of
> constraints tells it should be.
>
> With the new hierarchy, we have
>
>    Prop : Type0 : Type1 : ...
>    Set  : Type0 : Type1 : ...
>    Prop < Set   < Type1 < Type2 < ...
>
> which in fact is the same as
>
>    Prop            : Type0 : Type1 : ...
>           Type(-1) : Type0 : Type1 : ...
>    Prop < Type(-1) < Type0 < Type1 < ...
>
> if we interpret predicative Set as Type(-1), which, if we shift the
> indices used to number the levels, is the same as
>
>    Prop         : Type1 : Type2 : ...
>           Type0 : Type1 : Type2 : ...
>    Prop < Type0 < Type1 < Type2 < ...
>
> which differs only from the original hierarchy by not using Set and by
> enforcing the type of Prop to be Type1 instead of Type0, what at the
> end corresponds to a subset of the former system.
>
> With the new hierarchy, unit, while still put by default at level
> Prop, can now freely be used as a Set, what is more convenient and in
> my opinion more natural.
>
> One may argue that it could be as simpler to interpret predicative Set
> as Type0 (instead of a virtual Type(-1)) and to keep Prop of type
> Type0. My point is that it is in practise not more complicated to
> implement Prop of type Type1 than of Type0, and that this allows to
> keep a sort guaranteed not to contain Prop.
>
> I don't see any disavantage to this approach up to now, but comments
> are welcome.
>
> Hugo
>
> PS: I followed the convention of the Reference Manual of Coq
> (chapter 4) which numbers Type levels from 0 (what leads to introduce
> a negative level to interpret Set as a distinct Type). By the way, I
> just remarked that paragraph "Convertibility" in Section 4.3 of the
> reference manual is not up to date (though paragraph
> "Sort-polymorphism of inductive families" of Section 4.5.3 is).
>
> PS2: An alternative could have been to introduce a new base sort, say
> Singleton, to type the inductive types low enough to be put in Prop,
> with the associated subtyping Singleton < pSet and Singleton < Prop. My
> feeling was however that it would have made things more complicated
> than just having Prop < pSet and I renounced to it.
>