open import Cat.Monoidal.Strength.Monad
open import Cat.Functor.Naturality
open import Cat.Instances.Product
open import Cat.Monoidal.Strength
open import Cat.Monoidal.Braided
open import Cat.Monoidal.Reverse
open import Cat.Functor.Compose
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Monoidal.Functor
import Cat.Reasoning

module Cat.Monoidal.Monad where


module _ {o â}
{C : Precategory o â} (Cáµ : Monoidal-category C)
where
open Cat.Reasoning C
open Cat.Monoidal.Functor Cáµ Cáµ
open Monoidal-category Cáµ


A monoidal monad on a monoidal category is a monad on whose underlying endofunctor is also equipped with the structure of a lax monoidal functor, in a way that the two structures agree; alternatively, it is a monad in the bicategory of monoidal categories, lax monoidal functors and monoidal natural transformations.

  record Monoidal-monad-on (monad : Monad C) : Type (o â â) where
field

(F-mult to M-mult; F-Î±â to M-Î±â; F-Î±â to M-Î±â; F-Î»â to M-Î»â; F-Ïâ to M-Ïâ)
public


To summarise, we have the following data laying around:

The precise interaction we ask for is that the monadâs unit and multiplication be monoidal natural transformations1; this requires a total of four conditions.

That is a monoidal natural transformation is captured by the following two diagrams:

    field
unit-Îµ : Îµ â¡ Î· Unit
unit-Ï : â {A B} â Ï {A} {B} â (Î· A ââ Î· B) â¡ Î· (A â B)


Notice that the diagram on the left entirely determines to be

Then, for to be monoidal means that these two diagrams commute:

The diagram on the left automatically commutes because of the monad laws, since is forced to be so we only need to require the diagram on the right. This is the biggest requirement: so far, weâre describing a structure that any strong monad could be equipped with, but making the last diagram commute requires a commutative monad, as we will see in the rest of this module.

    mult-Îµ : Îµ â¡ ÎŒ Unit â Mâ Îµ â Îµ
mult-Îµ = insertl (ap (Î» x â _ â Mâ x) unit-Îµ â left-ident)

field
mult-Ï : â {A B} â Ï {A} {B} â (ÎŒ A ââ ÎŒ B) â¡ ÎŒ (A â B) â Mâ Ï â Ï

Monoidal-monad : Type (o â â)

  private unquoteDecl eqv = declare-record-iso eqv (quote Monoidal-monad-on)
: â {M} {a b : Monoidal-monad-on M}
â a â¡ b
Monoidal-monad-on-path p = Iso.injective eqv (Î£-prop-path (Î» _ â hlevel 1) p)


## Dualityð

module _ {o â}
{C : Precategory o â} {Cáµ : Monoidal-category C}
where
open Cat.Reasoning C
open Cat.Monoidal.Functor Cáµ Cáµ
open Monoidal-category Cáµ
private
module M = Cat.Functor.Reasoning M


As the definition of a monoidal monad is completely symmetric with respect to the tensor product, we straightforwardly get a monoidal monad on the reverse monoidal category from a monoidal monad on

  monoidal-monad^rev : Monoidal-monad-on Cáµ monad â Monoidal-monad-on (Cáµ ^rev) monad
{ Îµ = Îµ
; F-mult = NT (Î» _ â Ï) Î» _ _ _ â M-mult ._=>_.is-natural _ _ _
; F-Î±â = M-Î±â
; F-Î»â = M-Ïâ
; F-Ïâ = M-Î»â
}
; unit-Îµ = unit-Îµ
; unit-Ï = unit-Ï
; mult-Ï = mult-Ï


We now turn to proving the following result, alluded to above: the structure of a monoidal monad on a given monad is equivalent to the structure of a commutative strength for that monad!

Source

This is a slight generalisation of a result by Kock (1972), who proves that symmetric monoidal monads on a symmetric monoidal category correspond to commutative strengths (which are assumed to be symmetric).

The guiding intuition is that the monoidal structure on allows parallel, or âverticalâ composition of effects; this is illustrated by the mult-Ï diagram if we label the monadic âlayersâ as follows:

This should be reminiscent of the two composition structures in the hypotheses to the Eckmann-Hilton argument, which suggests that the two ways to sequence effects (âmonadicallyâ and âmonoidallyâ) should be the same, and, moreover, commutative.

We start by constructing a left monad strength from a monoidal monad, by composing the unit of the monad with the monoidal multiplication:

  monoidalâleft-strength
monoidalâleft-strength m = l where
open Left-strength

l .functor-strength .left-strength = M-mult ânt (-â- âž (unit ntÃ idnt))

We leave the verification of the strength axioms for the curious reader; they are entirely monotonous.
    l .functor-strength .left-strength-Î»â =
Mâ Î»â â Ï â (Î· _ ââ id) â¡Ëâš reflâ©ââš reflâ©ââš ap (_ââ id) unit-Îµ â©â¡Ë
Mâ Î»â â Ï â (Îµ ââ id)   â¡âš M-Î»â â©â¡
Î»â                      â
l .functor-strength .left-strength-Î±â =
Mâ (Î±â _ _ _) â Ï â (Î· _ ââ id)                          â¡Ëâš reflâ©ââš reflâ©ââš â.collapse unit-Ï â©â¡Ë
Mâ (Î±â _ _ _) â Ï â (Ï ââ id) â ((Î· _ ââ Î· _) ââ id)     â¡âš extendl3 M-Î±â â©â¡
Ï â (id ââ Ï) â Î±â _ _ _ â ((Î· _ ââ Î· _) ââ id)          â¡âš reflâ©ââš reflâ©ââš associator .Isoâ¿.to ._=>_.is-natural _ _ _ â©â¡
Ï â (id ââ Ï) â (Î· _ ââ (Î· _ ââ id)) â Î±â _ _ _          â¡âš reflâ©ââš â.pulll (idl _ ,â refl) â©â¡
Ï â (Î· _ ââ (Ï â (Î· _ ââ id))) â Î±â _ _ _                â¡âš pushr (â.pushl (sym (idr _) ,â sym (idl _))) â©â¡
(Ï â (Î· _ ââ id)) â (id ââ (Ï â (Î· _ ââ id))) â Î±â _ _ _ â
l .left-strength-Î· =
(Ï â (Î· _ ââ id)) â (id ââ Î· _) â¡âš pullr (â.collapse (idr _ ,â idl _)) â©â¡
Ï â (Î· _ ââ Î· _)                â¡âš unit-Ï â©â¡
Î· _                             â
l .left-strength-ÎŒ =
(Ï â (Î· _ ââ id)) â (id ââ ÎŒ _)                      â¡âš pullr (â.collapse (idr _ ,â idl _)) â©â¡
Ï â (Î· _ ââ ÎŒ _)                                     â¡Ëâš reflâ©ââš â.collapse3 (cancell left-ident ,â elimr (eliml M-id)) â©â¡Ë
Ï â (ÎŒ _ ââ ÎŒ _) â (Mâ (Î· _) ââ Mâ id) â (Î· _ ââ id) â¡âš pulll mult-Ï â©â¡
(ÎŒ _ â Mâ Ï â Ï) â (Mâ (Î· _) ââ Mâ id) â (Î· _ ââ id) â¡âš pullr (pullr (extendl (Ï.is-natural _ _ _))) â©â¡
ÎŒ _ â Mâ Ï â Mâ (Î· _ ââ id) â Ï â (Î· _ ââ id)        â¡âš reflâ©ââš M.pulll refl â©â¡
ÎŒ _ â Mâ (Ï â (Î· _ ââ id)) â Ï â (Î· _ ââ id)         â

module _ {o â}
{C : Precategory o â} (Cáµ : Monoidal-category C)
where
open Cat.Reasoning C
open Cat.Monoidal.Functor Cáµ Cáµ
open Monoidal-category Cáµ
private
module M = Cat.Functor.Reasoning M
module MÂ² = Cat.Functor.Reasoning (M Fâ M)
open is-iso


Reversing the construction, we also get a right strength.

  monoidalâcommutative
monoidalâcommutative = IsoâEquiv is where
is : Iso _ _
is .fst m = s , s-comm module to-strength where
s .strength-left = monoidalâleft-strength m

The coherence of the strengths is tedious; it involves the naturality of the associator and the coherence of the monoidal multiplication with the associator.
      s .strength-Î±â =
Mâ (Î±â _ _ _) â (Ï â (id ââ Î· _)) â ((Ï â (Î· _ ââ id)) ââ id) â¡âš reflâ©ââš pullr (â.weave (idl _ ,â id-comm)) â©â¡
Mâ (Î±â _ _ _) â Ï â (Ï ââ id) â ((Î· _ ââ id) ââ Î· _)          â¡âš extendl3 M-Î±â â©â¡
Ï â (id ââ Ï) â Î±â _ _ _ â ((Î· _ ââ id) ââ Î· _)               â¡âš reflâ©ââš reflâ©ââš associator .Isoâ¿.to ._=>_.is-natural _ _ _ â©â¡
Ï â (id ââ Ï) â (Î· _ ââ (id ââ Î· _)) â Î±â _ _ _               â¡âš pushr (extendl (â.weave (id-comm-sym ,â sym (idl _)))) â©â¡
(Ï â (Î· _ ââ id)) â (id ââ (Ï â (id ââ Î· _))) â Î±â _ _ _      â


The crucial part is the proof that the strength thus defined is commutative. Recall that this means that the two monoidal multiplications induced by the strength agree; in fact, we will show that they are both equal to

For the left-to-right composition, this is witnessed by the commutativity of the following diagram; the other direction is completely symmetric.

      opaque
leftâ¡Ï : left-Ï s â¡ M-mult
leftâ¡Ï = ext Î» (A , B) â
ÎŒ _ â Mâ (Ï â (Î· _ ââ id)) â Ï â (id ââ Î· _)       â¡âš reflâ©ââš M.popr (extendl (sym (Ï.is-natural _ _ _))) â©â¡
ÎŒ _ â Mâ Ï â Ï â (Mâ (Î· _) ââ Mâ id) â (id ââ Î· _) â¡âš pushr (pushr (reflâ©ââš â.collapse (elimr refl ,â M.eliml refl))) â©â¡
(ÎŒ _ â Mâ Ï â Ï) â (Mâ (Î· _) ââ Î· _)               â¡Ëâš pulll mult-Ï â©â¡Ë
Ï â (ÎŒ _ ââ ÎŒ _) â (Mâ (Î· _) ââ Î· _)               â¡âš elimr (â.annihilate (left-ident ,â right-ident)) â©â¡
Ï                                                  â

rightâ¡Ï : right-Ï s â¡ M-mult
rightâ¡Ï = ext Î» (A , B) â
ÎŒ _ â Mâ (Ï â (id ââ Î· _)) â Ï â (Î· _ ââ id)       â¡âš reflâ©ââš M.popr (extendl (sym (Ï.is-natural _ _ _))) â©â¡
ÎŒ _ â Mâ Ï â Ï â (Mâ id ââ Mâ (Î· _)) â (Î· _ ââ id) â¡âš pushr (pushr (reflâ©ââš â.collapse (M.eliml refl ,â elimr refl))) â©â¡
(ÎŒ _ â Mâ Ï â Ï) â (Î· _ ââ Mâ (Î· _))               â¡Ëâš pulll mult-Ï â©â¡Ë
Ï â (ÎŒ _ ââ ÎŒ _) â (Î· _ ââ Mâ (Î· _))               â¡âš elimr (â.annihilate (right-ident ,â left-ident)) â©â¡
Ï                                                  â

s-comm : is-commutative-strength s
s-comm = rightâ¡Ï â sym leftâ¡Ï


In the other direction, we are given a commutative strength and we must construct a monoidal monad. We already know how to construct a monoidal functor structure on a strong monad; all that remains is to check that it makes the monad structure monoidal.

    is .snd .inv (s , s-comm) = m where
open Lax-monoidal-functor-on



The monoidal unit is by definition.

      m .unit-Îµ = refl

The unit-Ï coherence is not very interesting.
      m .unit-Ï =
(ÎŒ _ â Mâ Ï â Ï) â (Î· _ ââ Î· _)            â¡âš pullr (pullr (reflâ©ââš â.expand (intror refl ,â introl refl))) â©â¡
ÎŒ _ â Mâ Ï â Ï â (Î· _ ââ id) â (id ââ Î· _) â¡âš reflâ©ââš reflâ©ââš pulll right-strength-Î· â©â¡
ÎŒ _ â Mâ Ï â Î· _ â (id ââ Î· _)             â¡Ëâš reflâ©ââš extendl (unit.is-natural _ _ _) â©â¡Ë
ÎŒ _ â Î· _ â Ï â (id ââ Î· _)                â¡âš cancell right-ident â©â¡
Ï â (id ââ Î· _)                            â¡âš left-strength-Î· â©â¡
Î· _                                        â


As expected, the proof of mult-Ï involves the commutativity of the strength. At a very high level, we are trying to collapse the sequence to we first need to commute the two strengths in the middle to obtain and then use the fact that two consecutive applications of the strengths result in just one after commuting with Concretely, this manifests as the following diagram, where the commutation of the strengths is highlighted.

The morphisms labelled alternate between being and in a way that is allowed by the associativity law because they are followed by

      m .mult-Ï =
(ÎŒ _ â Mâ Ï â Ï) â (ÎŒ _ ââ ÎŒ _)                        â¡âš reflâ©ââš â.expand (M.introl refl ,â intror refl) â©â¡
(ÎŒ _ â Mâ Ï â Ï) â (Mâ id ââ ÎŒ _) â (ÎŒ _ ââ id)        â¡âš pullr (pullr (extendl (Ï.is-natural _ _ _))) â©â¡
ÎŒ _ â Mâ Ï â Mâ (id ââ ÎŒ _) â Ï â (ÎŒ _ ââ id)          â¡âš reflâ©ââš reflâ©ââš reflâ©ââš right-strength-ÎŒ â©â¡
ÎŒ _ â Mâ Ï â Mâ (id ââ ÎŒ _) â ÎŒ _ â Mâ Ï â Ï           â¡âš reflâ©ââš M.pulll (left-strength-ÎŒ â assoc _ _ _) â©â¡
ÎŒ _ â Mâ ((ÎŒ _ â Mâ Ï) â Ï) â ÎŒ _ â Mâ Ï â Ï           â¡âš reflâ©ââš extendl (M.popr (sym (mult.is-natural _ _ _))) â©â¡
ÎŒ _ â Mâ (ÎŒ _ â Mâ Ï) â (ÎŒ _ â Mâ (Mâ Ï)) â Mâ Ï â Ï   â¡âš extendl (M.popl mult-assoc) â©â¡
(ÎŒ _ â ÎŒ _) â Mâ (Mâ Ï) â (ÎŒ _ â Mâ (Mâ Ï)) â Mâ Ï â Ï â¡âš pullr (extendl (mult.is-natural _ _ _)) â©â¡
ÎŒ _ â Mâ Ï â ÎŒ _ â (ÎŒ _ â Mâ (Mâ Ï)) â Mâ Ï â Ï        â¡Ëâš reflâ©ââš reflâ©ââš extendl (extendl mult-assoc) â©â¡Ë
ÎŒ _ â Mâ Ï â ÎŒ _ â (Mâ (ÎŒ _) â Mâ (Mâ Ï)) â Mâ Ï â Ï   â¡âš reflâ©ââš reflâ©ââš reflâ©ââš sym (assoc _ _ _) â M.extendl3 (sym (s-comm Î·â _)) â©â¡
ÎŒ _ â Mâ Ï â ÎŒ _ â Mâ (ÎŒ _) â Mâ (Mâ Ï) â Mâ Ï â Ï     â¡âš reflâ©ââš reflâ©ââš extendl mult-assoc â©â¡
ÎŒ _ â Mâ Ï â ÎŒ _ â ÎŒ _ â Mâ (Mâ Ï) â Mâ Ï â Ï          â¡âš reflâ©ââš reflâ©ââš reflâ©ââš extendl (mult.is-natural _ _ _) â©â¡
ÎŒ _ â Mâ Ï â ÎŒ _ â Mâ Ï â ÎŒ _ â Mâ Ï â Ï               â¡Ëâš reflâ©ââš extendl (mult.is-natural _ _ _) â©â¡Ë
ÎŒ _ â ÎŒ _ â Mâ (Mâ Ï) â Mâ Ï â ÎŒ _ â Mâ Ï â Ï          â¡Ëâš extendl mult-assoc â©â¡Ë
ÎŒ _ â Mâ (ÎŒ _) â Mâ (Mâ Ï) â Mâ Ï â ÎŒ _ â Mâ Ï â Ï     â¡âš reflâ©ââš M.pulll3 refl â©â¡
ÎŒ _ â Mâ (ÎŒ _ â Mâ Ï â Ï) â ÎŒ _ â Mâ Ï â Ï             â


### Wrapping upð

Finally, we check that these two transformations are mutual inverses.

Given a commutative strength, we must check that the round-trip defined above yields the same left and right strengths we started with; the situation isnât entirely symmetric because weâve made a choice to use the right strength first when defining the monoidal structure, but both verifications are straightforward.

    is .snd .rinv (s , s-comm) = Î£-prop-path (Î» _ â hlevel 1)
(Left-strength-path Cáµ M (sym l)))
(Right-strength-path Cáµ M (sym r))))
where
l : left-strength â¡ is .fst (is .snd .inv (s , s-comm)) .fst .Monad-strength.left-strength
l = ext Î» (A , B) â
ÎŒ _ â Î· _ â Ï                  â¡âš reflâ©ââš unit.is-natural _ _ _ â©â¡
ÎŒ _ â Mâ Ï â Î· _               â¡Ëâš pullr (pullr right-strength-Î·) â©â¡Ë
(ÎŒ _ â Mâ Ï â Ï) â (Î· _ ââ id) â
r : right-strength â¡ is .fst (is .snd .inv (s , s-comm)) .fst .Monad-strength.right-strength
r = ext Î» (A , B) â
ÎŒ _ â Mâ (Î· _) â Ï                    â¡Ëâš reflâ©ââš M.pulll left-strength-Î· â©â¡Ë
ÎŒ _ â Mâ Ï â Mâ (id ââ Î· _) â Ï       â¡Ëâš pullr (pullr (Ï.is-natural _ _ _)) â©â¡Ë
(ÎŒ _ â Mâ Ï â Ï) â (â Mâ id â ââ Î· _) â¡âš ap! M-id â©â¡
(ÎŒ _ â Mâ Ï â Ï) â (id ââ Î· _)        â


For the other round-trip, weâve already proved above that we get the same we started with; moreover, the monoidal unit becomes but the axioms of a monoidal monad force those to be the same, so weâre done.

    is .snd .linv m = Monoidal-monad-on-path Cáµ
(Lax-monoidal-functor-on-path
(sym unit-Îµ)
(to-strength.leftâ¡Ï m))

  module monoidalâcommutative = Equiv monoidalâcommutative


### Symmetric monoidal monads and commutative symmetric strengthsð

We can now refine this to Kockâs (1972) original result, which concerns symmetric monoidal monads in a symmetric monoidal category.

  module _ (CË¢ : Symmetric-monoidal Cáµ) where
open Symmetric-monoidal CË¢


We define a symmetric monoidal monad as a monoidal monad whose underlying monoidal functor is symmetric.

    is-symmetric-monoidal-monad : Monoidal-monad-on Cáµ monad â Type (o â â)
is-symmetric-monoidal-monad m = is-symmetric-functor CË¢ CË¢


Then, we have that, over the above equivalence between monoidal monads and commutative strengths, the property of being a symmetric monoidal monad is equivalent to the property of being a symmetric strength.

Given a symmetric monoidal monad, we immediately see that the induced left and right strengths are related by the braiding.

    module _ (m : Monoidal-monad-on Cáµ monad) where

      symmetric-monoidalâsymmetric-strength
â is-symmetric-monad-strength Cáµ (monoidalâcommutative.to m .fst)
symmetric-monoidalâsymmetric-strength sy =
(Ï â (id ââ Î· _)) â Î²â  â¡âš pullr (sym (Î²â.is-natural _ _ _)) â©â¡
Ï â Î²â â (Î· _ ââ id)    â¡âš extendl sy â©â¡
Mâ Î²â â Ï â (Î· _ ââ id) â


Now, given a symmetric commutative strength, we can use the commutativity as follows to conclude that the induced monoidal functor is symmetric:

    module _ ((s , s-comm) : Î£ _ is-commutative-strength) where

      symmetric-strengthâsymmetric-monoidal
â is-symmetric-monoidal-monad (monoidalâcommutative.from (s , s-comm))
symmetric-strengthâsymmetric-monoidal sy =
(ÎŒ _ â Mâ Ï â Ï) â Î²â       â¡âš pullr (pullr sy) â©â¡
ÎŒ _ â Mâ Ï â Mâ Î²â â Ï      â¡Ëâš reflâ©ââš M.extendl (swizzle sy has-is-symmetric (M.annihilate has-is-symmetric)) â©â¡Ë
ÎŒ _ â Mâ (Mâ Î²â) â Mâ Ï â Ï â¡âš extendl (mult.is-natural _ _ _) â©â¡
Mâ Î²â â ÎŒ _ â Mâ Ï â Ï      â¡âš reflâ©ââš s-comm Î·â _ â©â¡
Mâ Î²â â ÎŒ _ â Mâ Ï â Ï      â


Packaging all of this together, we conclude with the desired equivalence between the structure of a symmetric monoidal monad and the structure of a symmetric commutative strength.

    symmetricâsymmetric
symmetricâsymmetric = prop-over-ext monoidalâcommutative (hlevel 1) (hlevel 1)
symmetric-monoidalâsymmetric-strength symmetric-strengthâsymmetric-monoidal

symmetric-monoidalâsymmetric-commutative