The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/22/2012 11:25 PM, Lucian M. Patcas wrote:

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?

I'm not sure I was using standard terminology above, but I, at least, think of [Set] and [Prop] as universes.