module Cat.Monoidal.Functor {oc β„“c od β„“d}
  {C : Precategory oc β„“c} (Cᡐ : Monoidal-category C)
  {D : Precategory od β„“d} (Dᡐ : Monoidal-category D)

Monoidal functorsπŸ”—

Categorifying the fact that a morphism between monoids is expected to preserve the unit and multiplication, a functor between monoidal categories should come equipped with natural isomorphisms

witnessing that it preserves the tensor product and unit.

However, just like for lax functors between bicategories, we have the option of requiring only a natural transformation in one direction or the other. If we choose the forward direction we obtain the notion of a lax monoidal functor; choosing the opposite direction instead would yield an oplax monoidal functor.

We begin by defining the structure of a lax monoidal functor on a given functor this consists of the aforementioned morphisms, as well as some coherence conditions similar to the ones for a lax functor.

record Lax-monoidal-functor-on (F : Functor C D) : Type (oc βŠ” β„“c βŠ” od βŠ” β„“d) where
  private module F = Cat.Functor.Reasoning F

    Ξ΅ : Hom D.Unit (F.β‚€ C.Unit)
    F-mult : D.-βŠ—- F∘ (F FΓ— F) => F F∘ C.-βŠ—-

  module Ο† = _=>_ F-mult

  Ο† : βˆ€ {A B} β†’ Hom (F.β‚€ A D.βŠ— F.β‚€ B) (F.β‚€ (A C.βŠ— B))
  Ο† = Ο†.Ξ· _

    F-Ξ±β†’ : βˆ€ {A B C}
      β†’ F.₁ (C.Ξ±β†’ A B C) ∘ Ο† ∘ (Ο† D.βŠ—β‚ id) ≑ Ο† ∘ (id D.βŠ—β‚ Ο†) ∘ D.Ξ±β†’ _ _ _
    F-λ← : βˆ€ {A} β†’ F.₁ (C.λ← {A}) ∘ Ο† ∘ (Ξ΅ D.βŠ—β‚ id) ≑ D.λ←
    F-ρ← : βˆ€ {A} β†’ F.₁ (C.ρ← {A}) ∘ Ο† ∘ (id D.βŠ—β‚ Ξ΅) ≑ D.ρ←
Lax-monoidal-functor : Type (oc βŠ” β„“c βŠ” od βŠ” β„“d)
Lax-monoidal-functor = Ξ£ (Functor C D) Lax-monoidal-functor-on

A monoidal functor, or strong monoidal functor1, is then simply a lax monoidal functor whose structure morphisms are invertible.

record Monoidal-functor-on (F : Functor C D) : Type (oc βŠ” β„“c βŠ” od βŠ” β„“d) where
    lax : Lax-monoidal-functor-on F

  open Lax-monoidal-functor-on lax public

    Ξ΅-inv : is-invertible Ξ΅
    F-mult-inv : is-invertibleⁿ F-mult

Monoidal-functor : Type (oc βŠ” β„“c βŠ” od βŠ” β„“d)
Monoidal-functor = Ξ£ (Functor C D) Monoidal-functor-on

Braided and symmetric monoidal functorsπŸ”—

A monoidal functor between braided monoidal categories can additionally preserve the braiding in the sense that the following diagram commutes, yielding the notion of a braided monoidal functor.

  is-braided-functor : Lax-monoidal-functor β†’ Type (oc βŠ” β„“d)
  is-braided-functor (F , lax) = βˆ€ {A B} β†’ Ο† ∘ Dᡇ.Ξ²β†’ ≑ F.₁ Cᡇ.Ξ²β†’ ∘ Ο† {A} {B}
      module F = Functor F
      open Lax-monoidal-functor-on lax

A symmetric monoidal functor between symmetric monoidal categories is just a braided monoidal functor, since there is no extra structure to preserve.

  is-symmetric-functor : Lax-monoidal-functor β†’ Type (oc βŠ” β„“d)
  is-symmetric-functor = is-braided-functor Cᡇ Dᡇ

Diagonal monoidal functorsπŸ”—

If the source and target categories are equipped with diagonal morphisms, then a diagonal monoidal functor, or idempotent monoidal functor is a monoidal functor that makes the following diagram commute:

  is-diagonal-functor : Lax-monoidal-functor β†’ Type (oc βŠ” β„“d)
  is-diagonal-functor (F , lax) = βˆ€ {A} β†’ Ο† ∘ Dᡈ.Ξ΄ ≑ F.₁ (Cᡈ.Ξ΄ {A})
      module F = Functor F
      open Lax-monoidal-functor-on lax

The β€œidempotent” terminology comes from the semantics of programming languages, where lax monoidal functors are used to model certain kinds of effectful computations, as a β€œstatic” alternative to monads. In that setting, an idempotent monoidal functor (or β€œidempotent applicative functor”) represents an effect that can be executed multiple times with the same effect as executing it once: for example, reading from an immutable data source or throwing an exception.

Monoidal natural transformationsπŸ”—

The notion of natural transformation between functors can also be refined in the case of monoidal functors: a monoidal natural transformation is one such that the following diagrams commute.

  record is-monoidal-transformation (Ξ± : F => G) : Type (oc βŠ” β„“c βŠ” β„“d) where
      nat-Ξ΅ : Ξ± .Ξ· C.Unit ∘ FM.Ξ΅ ≑ GM.Ξ΅
      nat-Ο† : βˆ€ {A B} β†’ Ξ± .Ξ· _ ∘ FM.Ο† {A} {B} ≑ GM.Ο† ∘ (Ξ± .Ξ· _ D.βŠ—β‚ Ξ± .Ξ· _)

Note that, since monoidal categories can be thought of as one-object bicategories, we may expect to also have modifications between monoidal natural transformations, but this is not the case: the categorical ladder ends here. This is analogous to the fact that monoids only form a category and not a bicategory, even when viewed as one-object categories: there simply aren’t enough objects to have interesting 3-cells (resp. 2-cells)!

  1. Not to be confused with a strong monoidal functor, in the sense of a monoidal functor equipped with a strength.β†©οΈŽ