The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 06/09/2011 03:01, Stefan Monnier a écrit :
>> It is a (modest) change of the theory introduced in Coq version 8.2
>> (with reference manual lately updated from version 8.2pl2). The change
>> is motivated by sort polymorphism of inductive types so that it works
>> smoothlier. Typically, sort-polymorphism places the definition of
>> unit:Type at level Prop, and Prop<=Set allows to freely use unit also
>> at level Set or Type(n), as intuitively expected.
> 
> To what extend is it different from "get rid of Set, and then rename
> Type(n+1)=>Type(n) and Type(0)=>Set"?

With the algebraic universe mechanism implemented in Coq, you can
"create" arbitrary "Type"s that are "smaller" than a given one (but
always in finite number...). With the Type(n) presentation, one could
say that Type(0) is not defined once and for all, and can be
"relabelled" to e.g. Type(1) (and Type(1) to Type(2) and so on) if
needed. On the contrary, Set is never relabelled. I am not aware of a
situation where this is really important, though.


Cheers,

-- 
Stéphane