The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Discussion of universes turns up regularly on this list.  I have
nothing new to add, but maybe not everyone on this thread understands
the situation in Coq:

Unless things have changed recently, Coq does not have full "universe
polymorphism".  E.g. merely duplicating a definition (thus allowing
more opportunity for choosing fresh universes) can extend what Coq
will accept as correctly stratified.  Coq is ad hoc in this respect.

I guess the reason for this is efficiency.

LEGO had features like "Type" (indeterminate, floating, as in Coq),
"Type(3)", "Type(alpha)"  (named universe levels; every occurrence is
given the same but indeterminate level) and "Type(alpha+3)".  LEGO had
a switch to turn on full universe polymorphism (but a naive
implementation), and indeed using that option made the system too slow
to use in practice.  Lego had a slightly different universe system
(Luo's Extended Calculus of Constructions) than Coq does.  Lego also
had a switch to turn off universe checking all together: Type-in-Type,
\lambda^*.

Randy
--

On Thu, Apr 19, 2012 at 5:34 AM, Bernard Hurley 
<bernard AT marcade.biz>
 wrote:
> On Thu, Apr 19, 2012 at 07:18:58AM +0200, Andrej Bauer wrote:
>>
>> First, casting to "Type" is not a type annotation because Type is not
>> a type...
>
> First could I say that I've found reading this thread very useful in 
> understanding the Type heirarchy. (Yes, I know it's in the docs!)
> It does strike me, however, that someone might want to define something to 
> be at a particular place, e.g. Type(3) or above.
>
> Regards,
>
> Bernard.
>