The Coq mailing list

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

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

However I look at it
- when Prop and Set have no inhabitants
- or when Prop and Set has the same inhabitants
then X:Set implies X:Prop.

Because:

  X:Set  Y:Prop   X:Set → Y:Prop
  ────────────────────────────
  false   false      true
  true    true       true

these two cases:

  false   true       true
  true    false      false

are excluded if Prop and Set have the same inhabitants.

So I do not follow why do you say that "if Prop and Set have the same 
inhabitants, Y:Prop does not follow from Y:Set.