Commit 2023-02-23 12:23 db3e3bdc

View on Github →

feat: port CategoryTheory.Monoidal.Functor (#2445)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Functor.lean

added theorem CategoryTheory.LaxMonoidalFunctor.associativity_inv

added def CategoryTheory.LaxMonoidalFunctor.comp

added def CategoryTheory.LaxMonoidalFunctor.id

added theorem CategoryTheory.LaxMonoidalFunctor.left_unitality_inv

added def CategoryTheory.LaxMonoidalFunctor.prod'

added theorem CategoryTheory.LaxMonoidalFunctor.prod'_toFunctor

added theorem CategoryTheory.LaxMonoidalFunctor.prod'_ε

added theorem CategoryTheory.LaxMonoidalFunctor.prod'_μ

added def CategoryTheory.LaxMonoidalFunctor.prod

added theorem CategoryTheory.LaxMonoidalFunctor.right_unitality_inv

added structure CategoryTheory.LaxMonoidalFunctor

added def CategoryTheory.MonoidalFunctor.comp

added def CategoryTheory.MonoidalFunctor.diag

added def CategoryTheory.MonoidalFunctor.id

added theorem CategoryTheory.MonoidalFunctor.map_leftUnitor

added theorem CategoryTheory.MonoidalFunctor.map_rightUnitor

added theorem CategoryTheory.MonoidalFunctor.map_tensor

added def CategoryTheory.MonoidalFunctor.prod'

added theorem CategoryTheory.MonoidalFunctor.prod'_toLaxMonoidalFunctor

added def CategoryTheory.MonoidalFunctor.prod

added theorem CategoryTheory.MonoidalFunctor.εIso_hom

added theorem CategoryTheory.MonoidalFunctor.ε_hom_inv_id

added theorem CategoryTheory.MonoidalFunctor.ε_inv_hom_id

added theorem CategoryTheory.MonoidalFunctor.μIso_hom

added theorem CategoryTheory.MonoidalFunctor.μ_hom_inv_id

added theorem CategoryTheory.MonoidalFunctor.μ_inv_hom_id

added structure CategoryTheory.MonoidalFunctor