Removing `TypeMax` and friends

Stream: mathlib4

[Dagur Asgeirsson]

I tried removing TopCatMax, CompHausMax and ProfiniteMax in #12599, which aren't necessary anymore with the newest version of Lean (after https://github.com/leanprover/lean4/pull/3981). Is this something we want to do? There is also TypeMax and the algebraic versions ModuleCatMax etc.

[Matthew Ballard]

That looks pretty clean!

[Adam Topaz]

With this new universe approximation, will we have issues if we want to take finite limits in category theory? Recall that essentially all the finite limits with an explicit shape have the universe level of the diagram category being 0.

[Matthew Ballard]

It isn't enabled during typeclass search. I did an experiment and turned it on in #12522 and indeed the worst part was limits.

[Matthew Ballard]

Can I use something like leaff to easily check if the universe signatures change between commits?

[Dagur Asgeirsson]

@Alex J. Best?

[Matthew Ballard]

I think the main factors for ripping this out are

• unnecessary specialization of universe levels in declarations
• performance impacts and
• effect on user ergonomics

[Alex J. Best]

Sorry to reply so late. I try to do the bare minimum to make sure Leaff still works, but I don't have enough time to run it myself sadly