Commit 2023-06-05 02:03 116627d8

View on Github →

feat: port CategoryTheory.Bicategory.NaturalTransformation (#4594)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean

added def CategoryTheory.OplaxNatTrans.Modification.id

added def CategoryTheory.OplaxNatTrans.Modification.vcomp

added theorem CategoryTheory.OplaxNatTrans.Modification.whiskerLeft_naturality

added theorem CategoryTheory.OplaxNatTrans.Modification.whiskerRight_naturality

added structure CategoryTheory.OplaxNatTrans.Modification

added def CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents

added def CategoryTheory.OplaxNatTrans.id

added def CategoryTheory.OplaxNatTrans.vcomp

added theorem CategoryTheory.OplaxNatTrans.whiskerLeft_naturality_comp

added theorem CategoryTheory.OplaxNatTrans.whiskerLeft_naturality_id

added theorem CategoryTheory.OplaxNatTrans.whiskerLeft_naturality_naturality

added theorem CategoryTheory.OplaxNatTrans.whiskerRight_naturality_comp

added theorem CategoryTheory.OplaxNatTrans.whiskerRight_naturality_id

added theorem CategoryTheory.OplaxNatTrans.whiskerRight_naturality_naturality

added structure CategoryTheory.OplaxNatTrans