Commit 2023-09-21 19:25 89ce9cfc

View on Github →

feat: the category of CategoryTheory.Limits.Bicones (#7209) We already had this for Limits.Cone and Limits.Cocone. This also promotes Bicone.toCone and Bicone.toCocone to functors, leaving the old names as a shorthand for Functor.obj.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

deleted def CategoryTheory.Limits.Bicone.toCocone

added def CategoryTheory.Limits.Bicone.toCoconeFunctor

deleted def CategoryTheory.Limits.Bicone.toCone

added def CategoryTheory.Limits.Bicone.toConeFunctor

added theorem CategoryTheory.Limits.BiconeMorphism.ext

added structure CategoryTheory.Limits.BiconeMorphism

added def CategoryTheory.Limits.Bicones.ext

added def CategoryTheory.Limits.Bicones.functoriality