The Coq mailing list

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

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?