Highest universe in mathlib

Stream: general

[Yaël Dillies]

We all know we have infinitely many universes in Lean, and basically everything is universe-polymorphic in mathlib, but how many universes do we really need currently? That is, to which point can we squish down all universes in mathlib and still have everything typecheck? Kevin argued that Type 1 was enough, but I suspect some constructions in category might something higher.

[Johan Commelin]

Certainly Type 2 will be good enough. I think that's what's needed for LTE.

[Yaël Dillies]

I must say I'm surprised we don't need anything higher!

[Kevin Buzzard]

I'm not. If you're a set theorist then you think everything is a set so everything's in Type. Definitions like ordinals and the category of all sets/groups etc are called classes, and they're all in Type 1.

[Kevin Buzzard]

Classically in mathematics you only deal with sets and classes

[Kevin Buzzard]

Remember that historically mathematicians didn't even need sets! People like Gauss and Euler worked with terms and functions. Then Galois came along and said "I think it would be helpful if we could identify the permutation group of +-sqrt(2) with the permutation group of +-sqrt(3) because I think I'm on to something". It was only around then that we started needing to talk about some kind of holder type G for a collection of terms g. So in some sense before that we didn't even need Type. We just had concrete examples like the naturals, reals and complexes

[Kevin Buzzard]

The push to develop abstract group theory and then abstract algebra and ideas like homomorphisms of groups are historically very recent. This is when people started to want to talk about maps between abstract types -- functions had of course existed for centuries before that but again only between concrete types such as the sine and cosine function on the reals

[Kevin Buzzard]

So types became "things" and then set theory gave a name to the things, but Russell's paradox showed that you had to be careful so then we got things like ZFC and at that point mathematics was going on purely within Type.

[Kevin Buzzard]

Then category theory and homological algebra and Grothendieck came along and then people wanted to start talking about abstract mathematical objects such as the category of all sets, which weren't even in Type. Grothendieck fixed this by adding an extra axiom to set theory to enable more than one universe of types, or of sets as he called them, and even then you don't need infinitely many, you just need to allow yourself to do the occasional universe bump. Hence Type 1

[Mario Carneiro]

I've been curious about this question for a while, so I decided to answer it for real instead of theorizing.

open tactic

meta inductive level_spec
| const : level → level_spec
| parametric : list name → level → level_spec

meta def level.has_any_param : level → bool
| (level.succ l)     :=  l.has_any_param
| (level.max l₁ l₂)  :=  l₁.has_any_param ||  l₂.has_any_param
| (level.imax l₁ l₂) :=  l₁.has_any_param ||  l₂.has_any_param
| (level.param _)    := tt
| l                  := ff

meta def level.at_zero : level → nat
| (level.succ l)     := l.at_zero + 1
| (level.max l₁ l₂)  := max l₁.at_zero l₂.at_zero
| (level.imax l₁ l₂) := let n := l₂.at_zero in if n = 0 then 0 else max l₁.at_zero n
| _                  := 0

meta def level_spec.at_zero : level_spec → nat
| (level_spec.const l) := l.at_zero
| (level_spec.parametric _ l)  := l.at_zero

meta mutual def get_expr_level, get_const_spec (env : environment) (r : ref (name_map level_spec))
with get_expr_level : expr → level → tactic level
| v l := v.fold (pure l) $ λ e _ r, r >>= λ l,
  match e with
  | expr.const n us := do
    sp ← get_const_spec n,
    match sp with
    | level_spec.const l' := pure $ l.max l'
    | level_spec.parametric us' l' := pure $ l.max $ l'.instantiate (us'.zip us)
    end
  | expr.sort l' := pure $ l.max l'
  | _ := pure l
  end
with get_const_spec : name → tactic level_spec
| n := do
  m ← read_ref r,
  match m.find n with
  | some sp := pure sp
  | none := do
    let process_decl (n : name) (us : list name) (l : level) : tactic level_spec := (do
      let l := l.normalize,
      let sp := if l.has_any_param then level_spec.parametric us l else level_spec.const l,
      m ← read_ref r,
      write_ref r (m.insert n sp),
      pure sp),
    d ← env.get n,
    match d with
    | (declaration.defn n us t v _ _) :=
      get_expr_level t level.zero >>= get_expr_level v >>= process_decl n us
    | (declaration.thm n us t v) :=
      get_expr_level t level.zero >>= get_expr_level v.get >>= process_decl n us
    | (declaration.cnst n us t _) := get_expr_level t level.zero >>= process_decl n us
    | (declaration.ax n us t) := get_expr_level t level.zero >>= process_decl n us
    end
  end

run_cmd
  using_new_ref mk_name_map $ λ m, do
  env ← tactic.get_env,
  (n, z) ← env.fold (pure (name.anonymous, 0)) $ λ d r, (do
    p ← r,
    let n := d.to_name,
    sp ← get_const_spec env m n,
    let z := sp.at_zero,
    pure $ if p.2 < z then (n, z) else p),
  trace (n, z)

[Mario Carneiro]

For the core library, the output is (sigma.mk.inj_eq, 3), which is to say, if you were to specialize every definition to every concrete universe, then the largest subterm of the form Sort u that appears in the hierarchy of definitions leading to sigma.mk.inj_eq.{0, 0} is Sort 3, aka Type 2. sigma.mk.inj_eq is the only definition that gets as high as 3.

For mathlib, the output is (measure_theory.L1.set_to_L1_congr_left', 4), and I'm checking now to see if there are any others at height 4. So the official answer seems to be that you need Type 3 to compile mathlib, or alternatively, mathlib can be translated to work in ZFC with 4 inaccessible cardinals.

[Mario Carneiro]

It looks like there are a huge number of definitions at height 4 (and measure_theory.L1.set_to_L1_congr_left' is a random selection). I will look for minimal ones.

[Kevin Buzzard]

Just to be clear here -- if a random definition takes four types in, in universes u v w x, that doesn't artificially push the bound up to 4?

[Kevin Buzzard]

docs#measure_theory.L1.set_to_L1_congr_left'

[Mario Carneiro]

Here is the list of level 4 definitions that do not depend on any level 4 definitions (i.e. they are level 4 because they either directly use a large universe or reference a level 3 definition with a universe bump in the substitution):

ordinal.omin._match_1
nhds_is_measurably_generated
finprod_mem_def
finprod_eq_prod_of_mul_support_subset
add_monoid_hom.map_finsum
pSet.definable
pSet.arity.equiv._main
finprod_mem_univ
algebraic_geometry.LocallyRingedSpace.coproduct._proof_4
finprod_mem_empty
category_theory.types_glue._proof_1
category_theory.types_glue._proof_2
ordinal.lift.principal_seg._proof_1
hahn_series.summable_family.hsum._proof_1
smooth_partition_of_unity.mk
partition_of_unity.mk
bump_covering.to_pou_fun
finprod_cond_nonneg
finsum_eq_sum_of_support_subset
partition_of_unity.sum_eq_one'
partition_of_unity.sum_le_one'
smooth_partition_of_unity.sum_eq_one'
partition_of_unity.sum_nonneg
smooth_partition_of_unity.sum_le_one'
finsum_mem_def
finsum_mem_univ
finsum_mem_congr
algebraic_geometry.Scheme.basic_open_is_open_immersion
uchange
finsum_mem_induction
algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open._proof_2
algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open._proof_4
algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open._proof_8
algebraic_geometry.LocallyRingedSpace.has_coequalizer.coequalizer_π_app_is_local_ring_hom
finsum_mem_empty
algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_left
algebraic_geometry.LocallyRingedSpace.coproduct._proof_3
category_theory.subcanonical_types_grothendieck_topology
algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace._proof_4
algebraic_geometry.LocallyRingedSpace.coequalizer._proof_3
classical.all_definable._main._proof_1
finsum_mem_zero
monoid_hom.map_finprod
pSet.embed._match_1
finprod_mem_induction
classical.all_definable._main._proof_2
at_bot_is_measurably_generated
ordinal.typein_iso._match_1
ordinal.typein_iso._proof_1
pSet.arity.equiv._main._meta_aux
finsum_dmem
finprod_mem_one
finprod_mem_congr
category_theory.flat_iff_Lan_flat
finprod_dmem
at_top_is_measurably_generated

[Mario Carneiro]

@Kevin Buzzard No, having lots of universe parameters does not bump the level, but instantiating those parameters (directly or indirectly) with a u+1 somewhere does

[Kevin Buzzard]

measure_theory.L1.set_to_L1_congr_left' just looks to me like some random technical lemma in measure theory that has nothing to do with universes

[Mario Carneiro]

The new list is probably more useful

[Johan Commelin]

How the hack can something like finsum_mem_empty need a nontrivial amount of universes?

[Mario Carneiro]

One thing that is a bit dicey about any calculation like this is that if you just chop off the universe hierarchy, then not every term has a type. Right now, the program is asserting for every definition that its type and value have to be typecheckable; perhaps it would be better to skip the type for definitions and theorems

[Kevin Buzzard]

finprod_mem_empty needs four universes? I still don't think I understand the question :-)

[Mario Carneiro]

finsum_mem_empty.{u_1, u_4} has max universe max (u_1+4) (u_4+2)

[Johan Commelin]

docs#finsum_mem_empty

[Kevin Buzzard]

lol what is going on

[Yaël Dillies]

Wow! Thanks, Mario.

[Mario Carneiro]

• finsum_mem_empty.{u_1 u_4} has max universe max (u_1+4) (u_4+2) because it uses finsum.{u_4 u_1+1}
• finsum.{u_1 u_2} has max universe max (u_1+2) (u_2+3), still not sure where this is coming from, I will make a program to unravel it

[Kevin Buzzard]

lol I wrote finprod_mem_empty

[Kevin Buzzard]

oh! Oh so the issue is finsum, not my lemma

[Yaël Dillies]

You're in the highest universe, Kevin!

[Kevin Buzzard]

golly, I apparently wrote finprod too

[Yaël Dillies]

Mario Carneiro said:

still not sure where this is coming from, I will make a program to unravel it

The answer is Kevin :upside_down:

[Kevin Buzzard]

I'm pretty sure that other people told me what to write in that definition :-)

[Kevin Buzzard]

What is all this plift stuff?

[Mario Carneiro]

Here's the program for outputting the level of a definition and its direct dependencies:

meta def level_spec.level : level_spec → level
| (level_spec.const l) := l
| (level_spec.parametric _ l)  := l

meta def level_spec.args : level_spec → list name
| (level_spec.const l) := []
| (level_spec.parametric us _)  := us

set_option pp.all true
run_cmd
  using_new_ref mk_name_map $ λ m, do
  env ← tactic.get_env,
  let n := `finsum,
  l ← get_const_spec env m n,
  trace (l.args, l.level),
  d ← env.get n,
  let map := d.value.fold mk_name_set $ λ e _ m,
    if e.is_constant then m.insert e.const_name else m,
  map.fold (pure ()) $ λ n r, do
    r,
    l ← get_const_spec env m n,
    trace (n, l.args, l.level)

[Heather Macbeth]

Kevin Buzzard said:

finprod_mem_empty needs four universes? I still don't think I understand the question :-)

I don't think I understand most of these examples either ... is it possible that many of them are just "mistakes"? People mis-using universes when writing the lemma/definition?

[Mario Carneiro]

• finsum_mem_empty.{u_1 u_4} has max universe max (u_1+4) (u_4+2) because it uses finsum.{u_4 u_1+1}
• finsum.{u_1 u_2} has max universe max (u_1+2) (u_2+3), because it uses set.finite.to_finset.{u_2}
• set.finite.to_finset.{u} has max universe u+3, because it uses set.finite.fintype.{u}
• set.finite.fintype.{u} has max universe u+3, because it uses set.has_coe_to_sort.{u}
• set.has_coe_to_sort.{u} has max universe u+3, because it uses has_coe_to_sort.mk.{(max (u+1) 1) u+2}
• has_coe_to_sort.mk.{u v} has max universe max u (v+1), because its type uses out_param.{v+1}
• out_param.{u} has max universe u, because it mentions Sort u

[Kevin Buzzard]

It seems that the index types alpha,beta,iota are allowed to be Sorts however finset takes a Type, that's what all the plift nonsense is all about.

[Mario Carneiro]

I don't think that anything like that is going to cause spurious universe bumps

[Kevin Buzzard]

set.has_coe_to_sort.{u} has max universe u+3, because it uses has_coe_to_sort.mk.{(max (u+1) 1) u+2}

lol what is this?

[Mario Carneiro]

whether the indexing starts at 0 or 1 for a given universe variable doesn't really matter

[Mario Carneiro]

yeah that one is a bit surprising

[Mario Carneiro]

but you can see it clearly in the pp.all

[Mario Carneiro]

Note that in the has_coe_to_sort.mk step, I'm actually looking at the type of the definition rather than the value (since it's a constructor). Looking at types can cause universe bumps, since Type u : Type (u+1) - if you insist that the type be well formed for the value to be then you will get no upper bound

[Mario Carneiro]

Here's another way to look at the derivation:

• finsum_mem_empty.{0 0} uses finsum.{0 1}
• finsum.{0 1} uses set.finite.to_finset.{1}
• set.finite.to_finset.{1} uses set.finite.fintype.{1}
• set.finite.fintype.{1} uses set.has_coe_to_sort.{1}
• set.has_coe_to_sort.{1} uses has_coe_to_sort.mk.{2 3}
• has_coe_to_sort.mk.{2 3} uses out_param.{4}
• out_param.{4} contains Sort 4

The last two examples might help to understand what's happening:

#check @finsum_mem_empty.{0 0}
#check @finsum.{0 1}
#check @set.finite.to_finset.{1}
#check @set.finite.fintype.{1}
#check @set.has_coe_to_sort.{1}
#check @has_coe_to_sort.mk.{2 3}
-- has_coe_to_sort.mk.{2 3} : Π {a : Type 1} {S : out_param.{4} (Type 2)}, (a → S) → has_coe_to_sort.{2 3} a S
#check @out_param.{4}
-- out_param.{4} : Type 3 → Type 3

out_param is just an identity function, but in order to apply the identity function to Type 2 you need a Type 3 to write the type of the argument

[Heather Macbeth]

If the uses of set.has_coe_to_sort were replaced by subtype, would this get rid of the +3 universe bump?

[Mario Carneiro]

here's a simplified example how you can get lots of bumping without really doing anything weird

def foo : Prop := @id (@id (@id (@id (@id (Type 3) (Type 2)) (Type 1)) Type) Prop) true

[Mario Carneiro]

@Heather Macbeth Yes, you have to eliminate the uses of set.has_coe_to_sort in dependents as well, but this version drops the level of set.finite.fintype from u+3 to u+1:

inductive set.finite' {α} (s : set α) : Prop
| intro : fintype (subtype s) → set.finite'

lemma {u} set.finite_def' {α : Type u} {s : set α} : set.finite' s ↔ nonempty (fintype (subtype s)) := ⟨λ ⟨h⟩, ⟨h⟩, λ ⟨h⟩, ⟨h⟩⟩

noncomputable def {u} set.finite.fintype' {α : Type u} {s : set α} (h : set.finite' s) : fintype (subtype s) :=
classical.choice $ set.finite_def'.1 h

[Heather Macbeth]

Hmm, maybe set.has_coe_to_sort should be considered harmful ...

[Mario Carneiro]

Probably a better approach for determining the real axiomatic strength of mathlib would be to allow for higher universes that don't support inductive types at all. As long as you only use them in id applications like this that might be sufficient.

[Mario Carneiro]

Looking at this some more, finsum.{0 1} : Π {M α : Type}, ... which looks normal, but it references

set.finite.to_finset.{1} : Π {α : Type 1} {s : set α}, s.finite → finset α

which seems gratuitous (why are we dealing with sets of elements in Type 1?). I suspect the reason is plift : Sort u -> Type u. Perhaps we should try changing that to plift : Sort u -> Sort (max u 1) and see what breaks

[Mario Carneiro]

Oh, that won't work:

@[irreducible] noncomputable def finsum {M : Type u} {α : Sort v} [add_comm_monoid M] (f : α → M) : M :=
if h : finite (support (f ∘ plift.down)) then ∑ i in h.to_finset, f i.down else 0

Here support (f ∘ plift.down) is needed because support takes a Type u', and if you had a variant of plift returning Sort (max v 1) then it wouldn't unify with Type u' because u' + 1 = max v 1 does not have a solution for u' in level arithmetic

[Kevin Buzzard]

try induction v? ;-)

[Kevin Buzzard]

Whose idea was it to sum over Props anyway?

[Yury G. Kudryashov]

It was my idea

[Yury G. Kudryashov]

This way you can write \sum^f n < 5, n

[Kevin Buzzard]

We need pfinsum :-)

[Yury G. Kudryashov]

Why? You won't get nice notation if you don't use the same def for sums over n : nat and hn : n < 5.

[Yury G. Kudryashov]

Do you really care about universe bump here?

[Johan Commelin]

For me, I find ∑ᶠ n < 5, n more important than avoiding universe bumps.

[Anne Baanen]

I have heard of people who believe in the Axiom of Choice up to some aleph-n (n = 2 or 3 I think?). I haven't heard of anyone who doesn't believe in at most 3 inaccessible cardinals. So I'm curious why we care

[Kevin Buzzard]

Because I tell ZFC people that obviously it all works in ZFC?