The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 19/01/2017 11:43, Matej Kosik wrote:

>> Théo already explained it, so I just want to stress the important part
>> of his answer. "Prop < Set" does not mean that Prop is of type Set, it
>> just means that Prop is smaller than Set. In other words, any type of
>> Prop is a type of Set (but the converse does not hold).
> 
> That is an interesting question
> (If "X < Y", could we then conclude that "X : Y")
> but this is not what I wanted to ask now.
> 
> My question is, why do we insist upon universe constraint "Prop < Set" 
> instead of "Prop ≤ Set"?

As I explained, that is because A:Prop implies A:Set holds, but the
converse does not. So Prop is strictly smaller than Set.

There is absolutely nothing theoretically fancy here, so I am not sure
to understand where the confusion comes from.

Best regards,

Guillaume