Commit 2024-05-24 19:08 e73c3366

View on Github →

feat: oplax monoidal functors (#12856) Basic definitions of oplax monoidal functors. (Setting up towards bimonoids and hopf monoids.)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

added theorem CategoryTheory.OplaxMonoidalFunctor.associativity_inv

added def CategoryTheory.OplaxMonoidalFunctor.comp

added def CategoryTheory.OplaxMonoidalFunctor.id

added theorem CategoryTheory.OplaxMonoidalFunctor.left_unitality_hom

added theorem CategoryTheory.OplaxMonoidalFunctor.right_unitality_hom

added theorem CategoryTheory.OplaxMonoidalFunctor.δ_natural

added structure CategoryTheory.OplaxMonoidalFunctor