Commit 2025-09-26 06:32 ea8a7df2
View on Github →feat(CategoryTheory): Limits in Subobject X (#29766)
Adds limits to Subobject X. Together with https://github.com/leanprover-community/mathlib4/pull/29253, this will show existence of glbs in the poset of subobjects.