The Coq mailing list

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

Hi Emilio,

On 01/19/2017 02:02 PM, Emilio Jesús Gallego Arias wrote:
> Hi Matej,
> 
> Matej Kosik 
> <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
>  writes:
> 
>> after starting the toplevel like this:
>>
>>   coqtop -noinit
>>
>> neither Prop nor Set have any inhabitants and thus it is not the case that 
>> "Prop < Set".
>> The only thing that we can claim is "Prop ≤ Set".
> 
> What do you mean by inhabitant?

I try to use this word in the same way as it is used by both Coq'Art as well 
as Coq Reference Manual.

I am not quite sure if it is wise to use this word like this, but that 
question I would not like to open now.
(we may be creating unnecessary confusion by using words with means that can 
already have more usual denotations)

> I am not sure what you mean here, but
> note that `forall x : Prop, x` is an inhabitant of Prop.

This is a great example! Thank you!

So, indeed, this is related to what Théo said.

Even if we do not define any inductive propositions, Prop is inhabited. I 
should have known this but I did not. So thank you!

Indeed:

  Coq < Check (forall x : Prop, x) : Prop.
  (forall x : Prop, x) : Prop
     : Prop

This, still does not invalidated my objection to "Prop < Set" as long as ...

  Check (forall x : Prop, x) : Set.
  (forall x : Prop, x) : Set
     : Set

... unless, Set has some inhabitants that are not inhabitants of Prop. Let's 
try this:

  Coq < Set Printing Universes.

  Coq < Check (forall x : Prop, x) : Set.
  (forall x : Prop, x) : Set
     : Set

  Coq < Check (forall x : Set, x) : Set.
  Toplevel input, characters 0-32:
  > Check (forall x : Set, x) : Set.
  > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Error:
  The term "forall x : Set, x" has type "Type@{Set+1}"
  while it is expected to have type "Set".


So this is not the counter-example that would show that, when I start "coqtop 
-noinit" it would be the case that:

  Set not only has all the inhabitants of Prop, but it also has some such 
inhabitants, which are not in Prop.

(in which case we could relax "Prop < Set" to "Prop ≤ Set").

Are there such counter-examples?