The Coq mailing list

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

On 01/19/2017 05:31 PM, Jonathan Leivent wrote:
> 
> 
> 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.

I was not aware of that but I did not want to suggest modification of Coq so 
that

  Check Prop : Set.

succeeds.

When reading the above note, I was assuming that Bruno reacts to Théo.
(where Théo expressed his surprise that Set is not the type of Prop)
(which consequently surprised me that he could assume something like that)

The way how I interpreted Bruno's note is that the desirable property

  "All theorem provable in Coq if Set is predicative (the default situation)
   should also be provable in Coq if Set is impredicative (i.e. if we use 
-impredicative-set option)."

would be violated only if it would be the case that "Prop:Set", which is not 
what I was suggesting.

My question is, would that property be also violated if we relax "Prop ≤ Set" 
only for the case when Set is predicative
and keep it as is (Prop < Set) in case when Set is impredicative?

If yes, is there a theorem such that:
- it is provable if Set is predicative and we have relaxed "Prop < Set" to 
"Prop ≤ Set"
- and at the same time non-provable if Set is impredicative and we have kept 
the original "Prop < Set" constraint.

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