Difference of universes in Lean vs Coq

Stream: lean4

[Son Ho]

I'm puzzled by a difference I see between universe inference in Lean and Coq and which I do not understand.
If I write the following definition in Lean, I get that Tree lives in Type 2:

inductive Tree (α : Type) : Type 2 where
| Ret (x : α)
| Act {β : Type} (f : β → Tree α)

However the equivalent Coq definition happily lives in Type:

Inductive tree (α : Type) : Type :=
| Ret (x : α)
| Act {β : Type} (f : β → tree α)
.

Could someone explain me the reason which leads to this discrepancy?

[Floris van Doorn]

Note: In Lean any universe > 0 is a valid target universe for this inductive type, in particular 1 also works:

inductive Tree (α : Type) : Type 1 where
| Ret (x : α)
| Act {β : Type} (f : β → Tree α)

About Coq, are you sure that there is no hidden universe parameters in these Types that are actually different? Otherwise setting β = Tree α, this seems inconsistent.

[Floris van Doorn]

IIRC in Coq, if you don't turn on universe polymorphism explicitly, your universe live in some universe parameters with some universe inequalities behind the scenes(?)

[Son Ho]

Oh indeed you're right, the universe was hidden in Coq.
Doing this:

Set Printing Universes.
Check tree.

gives me:

tree : Type@{tree.u0} → Type@{max(Set,tree.u0,exercises.lang.251+1)}

which seems to be the same. So everything is good (sorry for the noise :sweat_smile: )

[Edward van de Meent]

universe 252 :eyes:

[Edward van de Meent]

the language automatically going that high is wild

[Floris van Doorn]

I think foo.251 is just an internal number given to the universe variable as its name. In a small Lean file, I expect that the internal universe metavariable counter will exceed that very quickly.

[Edward van de Meent]

i suppose that is a more sensible explanation

[Shreyas Srinivas]

Isn’t Type in Coq equivalent to Type 2 in lean?

[Shreyas Srinivas]

I thought they called their Type Set?

[Shreyas Srinivas]

Source of my (mis?)-understanding : https://cs.stackexchange.com/a/80737

[Shreyas Srinivas]

I could be wrong and Set and Prop are at the same universe level in Rocq

[Mario Carneiro]

It's a bit complicated. The Rocq universe hierarchy has Prop : Type@{Set+1}, Set : Type@{Set+1} and Type@{u} : Type@{u+1}, or more generally Type@{u} : Type@{v} when u < v. Note that Set is both a universe name and also a level name, and Set means Type@{Set} and Prop = Type@{Prop} likewise. Prop+1 is not a well formed level expression, but from the typing relations it seems Prop+1 effectively evaluates to Set+1.

[Mario Carneiro]

One extra inclusion: SProp : Type@{Set+1} as well, but SProp is not a level name like the other two so it is not expressible as Type@{...}.

[Mario Carneiro]

oh and also they recently .generalized their universe hierarchy some more with sort polymorphism, so we have Type@{Prop|u} which means something. I think it doesn't add any actually new universes but there are now sort variables that range over SProp, Prop, Set

[Mario Carneiro]

Still, they still have a way to go to compete with the awe inspiring complexity of the agda universe hierarchy

[Matthew Ballard]

Sometimes I feel like I inhabit DummyS.

[Shreyas Srinivas]

So Coq’s universe hierarchy is a partial order with no ordering between Set and Prop