Commit 2024-03-03 08:30 bf9724aa

View on Github →

feat: the category of CategoryTheory.Limits.BinaryBicones (#11102) This follows on from #7209

Estimated changes

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

modified def CategoryTheory.Functor.mapBinaryBicone

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

deleted def CategoryTheory.Limits.Bicone.toBinaryBicone

added def CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor

deleted def CategoryTheory.Limits.BinaryBicone.toBicone

added def CategoryTheory.Limits.BinaryBicone.toBiconeFunctor

added theorem CategoryTheory.Limits.BinaryBiconeMorphism.ext

added structure CategoryTheory.Limits.BinaryBiconeMorphism

added def CategoryTheory.Limits.BinaryBicones.ext

added def CategoryTheory.Limits.BinaryBicones.functoriality