category_theory.lax_monoidal_functor

A lax monoidal functor is a functor F : C ⥤ D between monoidal categories, equipped with morphisms ε : 𝟙 _D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y), satisfying the the appropriate coherences.

category_theory.monoidal_functor

A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.

category_theory.monoidal_functor.μ_nat_iso

The tensorator as a natural isomorphism.

category_theory.monoidal_functor.id

The identity monoidal functor.

category_theory.lax_monoidal_functor.comp

The composition of two lax monoidal functors is again lax monoidal.

category_theory.monoidal_functor.comp

The composition of two monoidal functors is again monoidal.