Commit 2025-10-27 09:15 180a3c43
View on Github →refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape (#29881)
This PR renames ClosedUnderLimitsOfShape as ObjectProperty.IsClosedUnderLimitsOfShape, and make it a typeclass.
The stability condition of a property P by (co)limits of shape J is now expressed as P.colimitsOfShape J ≤ P. This facilitates the connection with the relatively new API ColimitPresentation #29382 (and the related ObjectProperty.ColimitOfShape).
By using a typeclass for the stability condition, it will be possible to add instances HasLimitsOfShape instances for fullsubcategories.
This also makes the design more parallel to what we have for the stability under (co)limits of MorphismProperty.