random universe permutation

Stream: lean4

[Kevin Buzzard]

I was trying to keep universes sorted in some kind of order, but was really scratching my head about where a max u1 u2 was coming from in my terms, because u1 and u2 never appeared together without a bunch of other universes. I've minimised it to this:

import Mathlib.CategoryTheory.ConcreteCategory.Basic

universe u₂ v₁ u₁

open CategoryTheory

variable {C : Type 0} [Category.{0} C] (P : C ⥤ Type max (max u₁ v₁) u₂)

set_option pp.universes true in
#check P -- P : CategoryTheory.Functor.{0, max (max u₁ u₂) v₁, 0, max (max (u₁ + 1) (u₂ + 1)) (v₁ + 1)}...
--                                         ^^^^^^^^^^^^^^^^^^

-- Why the heck not `max (max u₁ v₁) u₂`?

#check Type max (max u₁ v₁) u₂ -- ((max (max u₁ v₁) u₂) + 1) as expected

which really surprises me. Lean is applying random theorems about max universes like associativity or commutativity or something, without even mentioning it, at a kind of random time.

[Gabriel Ebner]

Yes, Lean sorts the arguments to max.

[Gabriel Ebner]

(Sometimes.)

[Kevin Buzzard]

Does it sort arguments of the form max b c a sometimes too?

[Kevin Buzzard]

I wasn't sure whether to try and manipulate things this way, or whether I should do what Adam suggested and give up and hope that lean 4 comes up with better universe unification algorithms.

[Gabriel Ebner]

There's only a binary max under the hood.

[Gabriel Ebner]

I don't think that changing max u v w to max (max u w) v will have any observable effect right now. The only workaround we have that works is TypeMax.

[Kevin Buzzard]

I've found that Lean is actually quite good at unifying things like max (max a b) (max a+1 c) = max b c (a+1), it's just that it fails the moment anything is a ?u.

[Gabriel Ebner]

This is a great summary of the current situation with universe unification.