10
$\begingroup$

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?

$\endgroup$
3
  • 1
    $\begingroup$ Are you referring to Type* vs Type u or foo X vs foo.{u} X? $\endgroup$
    – Eric
    Feb 24 at 8:58
  • 2
    $\begingroup$ 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). $\endgroup$ Feb 24 at 9:05
  • $\begingroup$ the former, I edited the question. $\endgroup$
    – mcd
    Feb 24 at 9:05

1 Answer 1

8
$\begingroup$

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
    
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.