The Coq mailing list

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

On 01/19/2017 05:20 PM, Matej Kosik wrote:
> 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").

(I meant to say: in which case we *cannot* relax "Prop < Set" to "Prop ≤ 
Set").

> 
> Are there such counter-examples?
>