Commit 2025-07-15 10:09 a5d42804

View on Github →

feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): bicategory-like lemmas for CatCospanTransforms (#26447) We complete the proof that categorical cospan transforms introduced in #26412 form an "unbundled bicategory".

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean

added theorem CategoryTheory.Limits.CatCospanTransform.comp_whiskerLeft

added theorem CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight

added theorem CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft

added theorem CategoryTheory.Limits.CatCospanTransform.id_whiskerRight

added theorem CategoryTheory.Limits.CatCospanTransform.inv_whiskerLeft

added theorem CategoryTheory.Limits.CatCospanTransform.inv_whiskerRight

added theorem CategoryTheory.Limits.CatCospanTransform.pentagon

added theorem CategoryTheory.Limits.CatCospanTransform.triangle

added theorem CategoryTheory.Limits.CatCospanTransform.triangle_inv

added theorem CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp

added theorem CategoryTheory.Limits.CatCospanTransform.whiskerRight_comp

added theorem CategoryTheory.Limits.CatCospanTransform.whiskerRight_id

added theorem CategoryTheory.Limits.CatCospanTransform.whisker_exchange

added theorem CategoryTheory.Limits.CatCospanTransform.whiskerleft_id