Commit 2026-03-24 13:52 d19bfe46
View on Github →feat(CategoryTheory/ObjectProperty): binaryProductsClosure (#37085)
Define an abbreviation limitClosure where you only take limits of one shape. Then this is used to define binaryProductsClosure and its dual.
This is used in the definition of strong generators in #37046.