Commit 2024-10-24 12:28 dfb1dd38

View on Github →

chore(CategoryTheory): generalize universes for multiequalizers (#17997) Multi(co)equalizers involve two index sets. Until now, they were assumed to be in the same universe. In this PR, we allow two distinct universes. This shall ease the formalisation of (co)ends, which require heterogeneous universes.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

modified def CategoryTheory.Limits.Concrete.multiequalizerEquivAux

modified theorem CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply

modified theorem CategoryTheory.Limits.Concrete.multiequalizer_ext

Modified Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

modified def CategoryTheory.Limits.Multicofork.ofπ

modified def CategoryTheory.Limits.Multifork.ofι

modified inductive CategoryTheory.Limits.WalkingMulticospan.Hom

modified inductive CategoryTheory.Limits.WalkingMulticospan

modified inductive CategoryTheory.Limits.WalkingMultispan.Hom

modified inductive CategoryTheory.Limits.WalkingMultispan