# Explicit vs implicit universes in lean

I've seen in mathlib several cases where the universes are explicit, that is Type u instead of Type*. Is there any advantage in doing so and are there any (non-category theory) examples where universes have to be named explicitly in lean even though the mathematics does not run into universe issues?

• Are you referring to Type* vs Type u or foo X vs foo.{u} X?
– Eric
Feb 24, 2022 at 8:58
• Besides category theory, explicit universes are also used in set_theory/: cardinals, ordinals, a model of ZFC, surreal numbers, and game theory. All of these areas explicitly deal with size issues though (game theory is an outlier, but see the hypergame paradox to get a sense of why universes can get involved). Feb 24, 2022 at 9:05
• the former, I edited the question.
– mcd
Feb 24, 2022 at 9:05

Type* is just a shorthand for Type _, where the _ is a wildcard (or more accurately, a universe metavariable) that lean will try to fill in for you. Lean's options are to:

• Create a new universe for you, which it will give a name like u_1.
• Reuse an existing universe variable.
• Use max and similar to combine universe levels.

Usually then, explicit universe variables are used either when control over the names is wanted, or when the automatic behavior does the wrong thing.

To demonstrate the automatic behavior a little:

• In a variables line, lean will almost always create new variables; so

variables {α β : Type*}


is expanded to

universes u_1 u_2
variables {α : Type u_1} {β : Type u_2}

• In something like

example {α β : Type*} (h : α = β) : true := sorry


Lean is forced during elaboration of h to put both in the same universe, so it generates

universes u_1
example {α β : Type u_1} (h : α = β) : true := sorry