Commit 2023-06-12 05:44 f9de2aa4

View on Github →

feat: port CategoryTheory.Bicategory.FunctorBicategory (#4976)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/FunctorBicategory.lean

added def CategoryTheory.OplaxNatTrans.associator

added def CategoryTheory.OplaxNatTrans.leftUnitor

added def CategoryTheory.OplaxNatTrans.rightUnitor

added def CategoryTheory.OplaxNatTrans.whiskerLeft

added def CategoryTheory.OplaxNatTrans.whiskerRight

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean

added theorem CategoryTheory.OplaxNatTrans.Modification.comp_app'

added theorem CategoryTheory.OplaxNatTrans.Modification.id_app'

added theorem CategoryTheory.OplaxNatTrans.ext