The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

---

De: "Théo Zimmermann" <theo.zimmi AT gmail.com>
À: coq-club AT inria.fr
Envoyé: Mercredi 18 Janvier 2017 17:56:19
Objet: Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?

In fact, having Prop < Set, or Prop <= Set as a universe constraint does not force Prop : Set.

And indeed:
Coq < Set Printing Universes.

Coq < Check Prop.
Prop
     : Type@{Set+1}

Coq < Check Set.
Set
     : Type@{Set+1}

That is Prop and Set both are at bottom of the type hierarchy: there are just two distinct bottoms.
One of them is predicative:
Coq < Check (forall P : Prop, P).
forall P : Prop, P
     : Prop

And one is impredicative:
Coq < Check (forall P : Set, P).
forall P : Set, P
     : Type@{Set+1}

Thanks Theo and Guillaume for the clarification about the difference between the typing relation and the cumulativity relation.

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.

Bruno Barras.