Commit 2026-03-07 13:38 31948536

View on Github →

chore(CategoryTheory/Limits/Cones): rename namespace from Cones to Cone (#36293) This PR changes the CategoryTheory.Limits.Cones and CategoryTheory.Limits.Cocones namespaces by removing the s at the end. This is so that the namespace correspond to an actual declaration, namely CategoryTheory.Limits.Cone and CategoryTheory.Limits.Cocone. This makes more sense for the automatic name translation used by to_dual. The fixes in other files were done using a text-based search & replace. Note: Cones.extend has been renamed to Cone.extendHom, in order to not clash with the already existing Cone.extend.

Estimated changes