Algebra.Category.Algebra.Limits #5716

Stream: mathlib4

[Calvin Lee]

Just started this one, but every error seems to be due to universe unification (max v w =?= max v ?u)
I've seen https://github.com/leanprover/lean4/issues/2297, but not much discussion on this topic. Is there an "easy" way to solve or work around universe unification bugs?

[Scott Morrison]

You'll need (until we do a big refactor using UnivLE) to copy what is done in the analogous files. See ModuleCat/Limits.lean.

[Scott Morrison]

i.e. define AlgebraCatMax.

[Calvin Lee]

There seem to be 3 universe bugs that aren't fixed by the AlgebraCatMax trick.
I'm currently experimenting with UnivLE on a new branch to see if it can solve them

[Scott Morrison]

I don't see any sign of universe problems on this branch. It looks like some broken defeq problems.

[Scott Morrison]

I've finished this file.

[Calvin Lee]

yep i just fixed the last universe issues with a few manual annotations
thanks for the help!

[Scott Morrison]

I'm confused --- I don't see any further commits from you? In any case, it has been merged by now.