Commit 2024-12-06 15:26 1957fef0

feat(CategoryTheory): expand the API for AB axioms (#19200) This PR introduces typeclasses HasExactColimitsOfShape J C and HasExactLimitsOfShape J C which say that a J-shaped colimits (resp. limits) in a category C are exact in the sense of commuting with finite limits (resp. colimits). We redefine AB4, AB4Star, etc. in terms of these, and add also countable versions. Further, we generalize the proof of AB5 implies AB4 to a statement about HasExactColimitsOfShape, and add API for transporting instances of these classes along final/initial functors.