Commit 2025-10-29 00:03 60994424

feat(CategoryTheory/ObjectProperty): closure of a property under certain limits (#29854) In this PR, given a property P of objects in a category C and family of categories J : α → Type _, we introduce the closure P.limitsClosure J of P under limits of shapes J a for all a : α, and under certain smallness circumstances, we show that its essentially small.

• depends on: #29851
• depends on: #29881
• depends on: #29903
• depends on: #29849
• depends on: #29843