UnivLE for limits in MonCat, etc.

Stream: mathlib4

[Christian Merten]

Currently, the MonCat (and GroupCat etc.) API uses the TypeMax limit cone constructions. In particular docs#MonCat.hasLimitsOfSize only applies for MonCatMax constructions. I would like to have

instance hasLimitsOfSize' [UnivLE.{v, u}] :
    HasLimitsOfSize.{w, v} MonCat.{u} :=
  sorry

Is it advisable to have a version of docs#CategoryTheory.Limits.Types.Small.limitCone for MonCat? Or even just replace the MonCatMax versions with UnivLE versions?

[Christian Merten]

(note that having HasLimitsOfSize.{w, v} instead of HasLimitsOfSize.{v, v} is easy, it is only about the MonCat.{u} with UnivLE.{v, u} instead of MonCatMax.{v, u})

[Matthew Ballard]

TypeMax was a bit of a hack to deal with changes in universe unification. UnivLE is more principled. I would defer to the latter when possible.

[Christian Merten]

So you are suggesting to add UnivLE versions for limit constructions in MonCat, GroupCat, etc.?

[Matthew Ballard]

Replace MonCatMax etc if feasible

[Matthew Ballard]

Thanks!

[Christian Merten]

This is #11420.