Commit 2026-03-03 15:46 c0c380ee

View on Github →

feat(CategoryTheory/Monoidal/Limits): generalise universes and explicit limits for limits of monoid objects (#35996) This PR makes two major refactors to the file. These are easiest to make simultaneously, as they are heavily linked.

Generalise the smallness assumptions on the shape category
Take explicit limit cones as inputs rather than assuming HasLimitsOfShape and using the choice-cone

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

modified def CategoryTheory.Mon.forgetMapConeLimitConeIso

modified def CategoryTheory.Mon.limit

modified def CategoryTheory.Mon.limitCone

modified def CategoryTheory.Mon.limitConeIsLimit

added def CategoryTheory.Mon.limitConeLiftsToLimit