module Cat.Monoidal.Functor {oc βc od βd} {C : Precategory oc βc} (Cα΅ : Monoidal-category C) {D : Precategory od βd} (Dα΅ : Monoidal-category D) where

# 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
$FAβFBβF(AβB),$
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
$F:$
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 field Ξ΅ : 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)) Ο = Ο.Ξ· _ field 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.Οβ

F-Ξ±β : β {A B C} β F.β (C.Ξ±β A B C) β Ο β (id D.ββ Ο) β‘ Ο β (Ο D.ββ id) β D.Ξ±β _ _ _ F-Ξ±β = swizzle (sym (F-Ξ±β β assoc _ _ _)) (D.Ξ±β .invl) (F.F-map-iso C.Ξ±β .invr) β sym (assoc _ _ _) private unquoteDecl eqv = declare-record-iso eqv (quote Lax-monoidal-functor-on) Lax-monoidal-functor-on-path : β {F} {l l' : Lax-monoidal-functor-on F} β l .Lax-monoidal-functor-on.Ξ΅ β‘ l' .Lax-monoidal-functor-on.Ξ΅ β l .Lax-monoidal-functor-on.F-mult β‘ l' .Lax-monoidal-functor-on.F-mult β l β‘ l' Lax-monoidal-functor-on-path p q = Iso.injective eqv (Ξ£-pathp p (Ξ£-prop-pathp (Ξ» _ _ β hlevel 1) q))

Lax-monoidal-functor : Type (oc β βc β od β βd) Lax-monoidal-functor = Ξ£ (Functor C D) Lax-monoidal-functor-on

A **monoidal functor**, or **strong monoidal
functor**^{1}, 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 field lax : Lax-monoidal-functor-on F open Lax-monoidal-functor-on lax public field Ξ΅-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**.

module _ (Cα΅ : Braided-monoidal Cα΅) (Dα΅ : Braided-monoidal Dα΅) where module Cα΅ = Braided-monoidal Cα΅ module Dα΅ = Braided-monoidal Dα΅

is-braided-functor : Lax-monoidal-functor β Type (oc β βd) is-braided-functor (F , lax) = β {A B} β Ο β Dα΅.Ξ²β β‘ F.β Cα΅.Ξ²β β Ο {A} {B} where 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.

module _ (CΛ’ : Symmetric-monoidal Cα΅) (DΛ’ : Symmetric-monoidal Dα΅) where open Symmetric-monoidal CΛ’ using (Cα΅) open Symmetric-monoidal DΛ’ using () renaming (Cα΅ to Dα΅)

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:

module _ (Cα΅ : Diagonals Cα΅) (Dα΅ : Diagonals Dα΅) where module Cα΅ = Diagonals Cα΅ module Dα΅ = Diagonals Dα΅

is-diagonal-functor : Lax-monoidal-functor β Type (oc β βd) is-diagonal-functor (F , lax) = β {A} β Ο β Dα΅.Ξ΄ β‘ F.β (Cα΅.Ξ΄ {A}) where 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**
$Ξ±:FβG$
is one such that the following diagrams commute.

module _ ((F , F-monoidal) (G , G-monoidal) : Lax-monoidal-functor) where module FM = Lax-monoidal-functor-on F-monoidal module GM = Lax-monoidal-functor-on G-monoidal open _=>_

record is-monoidal-transformation (Ξ± : F => G) : Type (oc β βc β βd) where field 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)!