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?
$\begingroup$
$\endgroup$
3
1 Answer
$\begingroup$
$\endgroup$
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
maxand 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
variablesline, lean will almost always create new variables; sovariables {α β : Type*}is expanded to
universes u_1 u_2 variables {α : Type u_1} {β : Type u_2}In something like
example {α β : Type*} (h : α = β) : true := sorryLean is forced during elaboration of
hto put both in the same universe, so it generatesuniverses u_1 example {α β : Type u_1} (h : α = β) : true := sorry
Type*vsType uorfoo Xvsfoo.{u} X? $\endgroup$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). $\endgroup$