The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

On Fri, Apr 20, 2012 at 18:08, Adam Chlipala <adamc AT csail.mit.edu> wrote:

...
 

It's an interesting coincidence that you bring this issue up so soon after the previous question relating to fake universe polymorphism in Coq!  The specific consequence of such polymorphism here is that the type [b] is interpreted as being at the lowest possible universe level, [Set].

I thought Type(0) was the lowest universe level in Coq and that Set and Prop were "only" sorts in Type(0)? What am I missing?

Thanks,
Lucian