Commit 2022-12-20 20:06 e49a66f4

View on Github →

feat: port CategoryTheory.Whiskering (#1071)

depends on: #846

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Whiskering.lean

added def CategoryTheory.Functor.associator

added def CategoryTheory.Functor.leftUnitor

added theorem CategoryTheory.Functor.pentagon

added def CategoryTheory.Functor.rightUnitor

added theorem CategoryTheory.Functor.triangle

added def CategoryTheory.isoWhiskerLeft

added theorem CategoryTheory.isoWhiskerLeft_hom

added theorem CategoryTheory.isoWhiskerLeft_inv

added def CategoryTheory.isoWhiskerRight

added theorem CategoryTheory.isoWhiskerRight_hom

added theorem CategoryTheory.isoWhiskerRight_inv

added def CategoryTheory.whiskerLeft

added theorem CategoryTheory.whiskerLeft_comp

added theorem CategoryTheory.whiskerLeft_id'

added theorem CategoryTheory.whiskerLeft_id

added theorem CategoryTheory.whiskerLeft_twice

added def CategoryTheory.whiskerRight

added theorem CategoryTheory.whiskerRight_comp

added theorem CategoryTheory.whiskerRight_id'

added theorem CategoryTheory.whiskerRight_id

added theorem CategoryTheory.whiskerRight_left

added theorem CategoryTheory.whiskerRight_twice

added def CategoryTheory.whiskeringLeft

added def CategoryTheory.whiskeringRight