The Coq mailing list

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

On 19/01/2017 13:48, Matej Kosik wrote:

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

If your question is about some other formal system with different
definitions of Prop and Set, then yes, all bets are off. Otherwise no,
bool:Set does not imply bool:Prop in Coq.

Best regards,

Guillaume