open import Cat.Functor.Naturality
open import Cat.Monoidal.Diagonals
open import Cat.Instances.Product
open import Cat.Monoidal.Braided
open import Cat.Monoidal.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

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π

open Cat.Reasoning D

private
module C = Monoidal-category Cα΅
module D = Monoidal-category Dα΅


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

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 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
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 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)!

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