Commit 2024-03-26 07:43 a57ceda5

View on Github →

refactor: generalize universes for commuting filtered colimits and finite limits (#11325)

Estimated changes

Modified Mathlib/CategoryTheory/Functor/Flat.lean

Modified Mathlib/CategoryTheory/Limits/ColimitLimit.lean

modified theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Limits/Types.lean