Commit 2025-09-29 04:37 75f8fee5
View on Github →feat(CategoryTheory/Limits/Cones): add Co(co)neMorphism.map_w (#29962)
This PR introduces ConeMorphism.map_w and CoconeMorphism.map_w, which assert that functors preserve the commutativity of (co)cone morphisms.
Thanks to @chrisflav for the review and suggestions on the earlier version of this PR.