The Coq mailing list

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

On 18/01/2017 17:30, Matej Kosik wrote:
> My question is about weakening (not strengthening)
> 
>   Prop < Set
> 
> to
> 
>   Prop <= Set

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

Best regards,

Guillaume