Commit 2024-12-23 08:45 e258ed24

chore(CategoryTheory): generalize universes for WellPowered (#19992) If C : Type u and Category.{v} C, we generalize WellPowered C by introducing an auxiliary universe w. The category C satisfies WellPowered.{w} C now if it is locally small relative to w and the type of subobjects of any X : C is w-small. The previous definition corresponds to the case w = v. It was necessary to introduce a new file CategoryTheory.Comma.LocallySmall: it contains various LocallySmall instances for categories like Comma, StructuredArrow, Over, etc. Apart from this, the only "new" result is a WellPowered.{w} C instance for abelian categories satisfying IsGrothendieckAbelian.{w} C. This generalization of WellPowered is used in #20014.