Removing universe unification hack in AlgebraCat/Basic file

Stream: mathlib4

[Javier Lopez-Contreras]

Hello,

I'm trying to create CommAlgebraCat by copying around some stuff from https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/Category/AlgebraCat/Basic.lean and I have found the following:

-- Porting note: typemax hack to fix universe complaints
/-- An alias for `AlgebraCat.{max u₁ u₂}`, to deal around unification issues.
Since the universe the ring lives in can be inferred, we put that last. -/
@[nolint checkUnivs]
abbrev AlgebraCatMax.{v₁, v₂, u₁} (R : Type u₁) [CommRing R] := AlgebraCat.{max v₁ v₂} R

@Yaël Dillies claims that this is outdated and should be solved using UnivLE, does anyone know how to remove the hack?

[Christian Merten]

Note that there is an ongoing refactor of AlgebraCat in #19065.

[Javier Lopez-Contreras]

Had not seen that, thanks! Left #19299 as WIP, depending on #19065

[Christian Merten]

For now, can you work with Under R instead? Note that #19058 provides API for this case so it is quite convenient to work with.

[Javier Lopez-Contreras]

I was not aware this existed, thanks! (I'm a newbie)