The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 01/19/2017 01:36 PM, Guillaume Melquiond wrote:
> 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.

Not even when:
- Prop and Set have no inhabitants
- or Prop and Set have the same inhabitants
?

> 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.