The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/19/2017 11:20 AM, Matej Kosik wrote:
> ...
>    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?


I think you are missing some implications of what Bruno Barras said here:

> The reason why Prop:Set does not hold (although it is consistent in the 
> default settings of Coq: think of Set as Type(0) and Type(i) as Type(i+1)) is 
> that Coq allows to make Set impredicative, and we expect this to be an 
> extension of Coq without the option set (all theorems of Coq without the 
> option are theorems of Coq with it).
> With this option set and Prop:Set, Coq would then contain system U which is 
> inconsistent.

(this, by the way, would be a great addition to the FAQ).

Note that when -impredicative-set is used, then

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

succeeds.  I think that plus the design constraint on Coq Bruno 
mentioned above - all theorems without -impredicative-set are theorems 
with -impredicative-set - might imply that Prop can't bet <= Set even 
without -impredicative-set.

-- Jonathan