Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-17 21:37 8c385bc4

View on Github →

feat(category_theory): associator and unitors for functors (#478) also check pentagon and triangle

Estimated changes

Modified category_theory/whiskering.lean

added def category_theory.functor.associator

added def category_theory.functor.left_unitor

added theorem category_theory.functor.pentagon

added def category_theory.functor.right_unitor

added theorem category_theory.functor.triangle