The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you write
  (fun x : Set => (x : Prop))
Coq will currently reject that.  If you relax Prop < Set to Prop ≤ Set, Coq will add the global constraint that Set ≤ Prop and hence that Prop = Set, just as when you write
(fun x : Type@{i} => (x : Type@{j}))
Coq adds the constraint that i ≤ j.

It might also be the case that you'd get this constraint in more subtle situations, such as if you write
  Inductive inhabited (X : Set) : Prop := inhabits (_ : X).
or if you write
  (forall X : Set, X) : Set

Does this answer your question?

On Sat, Jan 21, 2017, 11:27 AM Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

Hi Hugo,

For me, the most surprising parts of you reply are:

On 01/19/2017 11:58 PM, Hugo Herbelin wrote:
>
> The "Prop < Set" is technical: the universe-acyclicity algorithm
> internally needs to consider Prop <> Set to ensure that Prop is not
> accidentally equated to Set (*). Matthieu, who introduced this for the
> polymorphism of universes, confirmed.

...

> (*) In particular, changing the line "enforce_univ_lt Level.prop
> Level.set empty" into "enforce_univ_le Level.prop Level.set empty"
> would be incorrect, unless other means are used to ensure that the
> algorithm does not eventually incorrectly conclude that Prop = Set is
> part of the logic.

I wouldn't be surprised if Coq concluded that:

  X ≤ Z      (* all inhabitants of X are also inhabitants of Z *)

from the following two universe constraints:

  X ≤ Y      (* all inhabitants of X are also inhabitants of Y *)

  Y ≤ Z      (* all inhabitants of Y are also inhabitants of Z *)


Similarly, no surprise when it concludes:

  X = Y      (* X and Y have the same inhabitants *)

from these constraints:

  X ≤ Y      (* all inhabitants of X are also inhabitants of Y *)

  Y ≤ X      (* all inhabitants of Y are also inhabitants of X *)


However, when you claim that Coq can conclude

  Prop = Set   (* Prop and Set have the same inhabitants *)

from, and solely from:

  Prop ≤ Set   (* all inhabitants of Prop are also inhabitants of Set *)

isn't that counterintuitive for the user?

Did I understand you correctly when you said that this could really happen (if we imagine that "Prop < Set" was relaxed to "Prop ≤ Set") ?

Would Coq do this only in case of Prop and Set or in general for any two universes?