Commit 2025-04-07 02:11 8e3bc147

View on Github →

chore(CategoryTheory/Whiskering): move definition of functor associators and unitors (#23699) The definition of functor associators and unitors are moved to CategoryTheory/Functor/Category.lean. Pentagon and triangle identities remain in CategoryTheory/Whiskering.lean.

Estimated changes

Modified Mathlib/CategoryTheory/Functor/Category.lean

added def CategoryTheory.Functor.associator

added def CategoryTheory.Functor.leftUnitor

added def CategoryTheory.Functor.rightUnitor

Modified Mathlib/CategoryTheory/Whiskering.lean

deleted def CategoryTheory.Functor.associator

deleted def CategoryTheory.Functor.leftUnitor

deleted def CategoryTheory.Functor.rightUnitor

modified theorem CategoryTheory.Functor.triangle