Commit 2024-06-17 14:41 57aa9c9a

View on Github →

feat(CategoryTheory/Category/Cat): add Cat API (#13809) Add API for Bicategory.whiskerRight and Bicategory.whiskerLeft

Estimated changes

Modified Mathlib/CategoryTheory/Category/Cat.lean

added theorem CategoryTheory.Cat.associator_hom_app

added theorem CategoryTheory.Cat.associator_inv_app

added theorem CategoryTheory.Cat.leftUnitor_hom_app

added theorem CategoryTheory.Cat.leftUnitor_inv_app

added theorem CategoryTheory.Cat.rightUnitor_hom_app

added theorem CategoryTheory.Cat.rightUnitor_inv_app

added theorem CategoryTheory.Cat.whiskerLeft_app

added theorem CategoryTheory.Cat.whiskerRight_app