Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-15 12:18 1f72be1f

View on Github →

feat(category_theory/whiskering): simp-lemmas for unitors and associators (#505)

Estimated changes

Modified category_theory/whiskering.lean

added theorem category_theory.functor.associator_hom_app

added theorem category_theory.functor.associator_inv_app

added theorem category_theory.functor.left_unitor_hom_app

added theorem category_theory.functor.left_unitor_inv_app

added theorem category_theory.functor.right_unitor_hom_app

added theorem category_theory.functor.right_unitor_inv_app