module Cat.Monoidal.Monad where
Monoidal monadsð
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 open Monad monad field monad-monoidal : Lax-monoidal-functor-on M open Lax-monoidal-functor-on monad-monoidal renaming (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 â â) Monoidal-monad = Σ (Monad C) Monoidal-monad-on
private unquoteDecl eqv = declare-record-iso eqv (quote Monoidal-monad-on) Monoidal-monad-on-path : â {M} {a b : Monoidal-monad-on M} â a .Monoidal-monad-on.monad-monoidal â¡ b .Monoidal-monad-on.monad-monoidal â 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} {monad : Monad C} where open Cat.Reasoning C open Cat.Monoidal.Functor Cáµ Cáµ open Monoidal-category Cáµ open Monad monad 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 monoidal-monad^rev m = record { monad-monoidal = record { ε = ε ; F-mult = NT (λ _ â Ï) λ _ _ _ â M-mult ._=>_.is-natural _ _ _ ; F-αâ = M-αâ ; F-λâ = M-Ïâ ; F-Ïâ = M-λâ } ; unit-ε = unit-ε ; unit-Ï = unit-Ï ; mult-Ï = mult-Ï } where open Monoidal-monad-on m
As commutative monadsð
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!
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.
Commutative monads from monoidal monadsð
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-monad-on Cáµ monad â Left-monad-strength Cáµ monad monoidalâleft-strength m = l where open Monoidal-monad-on m open Left-strength open Left-monad-strength l : Left-monad-strength Cáµ monad 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) (monad : Monad C) where open Cat.Reasoning C open Cat.Monoidal.Functor Cáµ Cáµ open Monoidal-category Cáµ open Monad monad 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-monad-on Cáµ monad â Σ (Monad-strength Cáµ monad) is-commutative-strength monoidalâcommutative = IsoâEquiv is where is : Iso _ _ is .fst m = s , s-comm module to-strength where open Monoidal-monad-on m open Monad-strength s : Monad-strength Cáµ monad s .strength-left = monoidalâleft-strength m s .strength-right = monad-strength^rev .fst (monoidalâleft-strength (monoidal-monad^rev 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â¡Ï
Monoidal monads from commutative monadsð
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 Monad-strength s open Monoidal-monad-on open Lax-monoidal-functor-on m : Monoidal-monad-on Cáµ monad m .monad-monoidal = strengthâmonoidal s
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) (Monad-strength-path Cáµ monad (Left-monad-strength-path Cáµ monad (Left-strength-path Cáµ M (sym l))) (Right-monad-strength-path Cáµ monad (Right-strength-path Cáµ M (sym r)))) where open Monad-strength s l : left-strength â¡ is .fst (is .snd .inv (s , s-comm)) .fst .Monad-strength.left-strength l = ext λ (A , B) â Ï â¡âš insertl right-ident â©â¡ ÎŒ _ â η _ â Ï â¡âš 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) â Ï â¡âš insertl left-ident â©â¡ ÎŒ _ â 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)) where open Monoidal-monad-on m
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.
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Ë¢ (_ , m .Monoidal-monad-on.monad-monoidal)
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.
symmetric-monoidalâsymmetric-strength : is-symmetric-monoidal-monad m â 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:
symmetric-strengthâsymmetric-monoidal : is-symmetric-monad-strength Cáµ s â 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 : is-symmetric-monoidal-monad â[ monoidalâcommutative ] (is-symmetric-monad-strength Cáµ â fst) symmetricâsymmetric = prop-over-ext monoidalâcommutative (hlevel 1) (hlevel 1) symmetric-monoidalâsymmetric-strength symmetric-strengthâsymmetric-monoidal symmetric-monoidalâsymmetric-commutative : Σ (Monoidal-monad-on Cáµ monad) is-symmetric-monoidal-monad â Σ (Monad-strength Cáµ monad) (λ s â is-commutative-strength s à is-symmetric-monad-strength Cáµ s) symmetric-monoidalâsymmetric-commutative = overâtotal monoidalâcommutative symmetricâsymmetric âe Σ-assoc eâ»Â¹
With respect to the induced lax monoidal structures on and â©ïž
References
- Kock, Anders Bredahl. 1972. âStrong Functors and Monoidal Monads.â Archiv Der Mathematik 23: 113â20. https://doi.org/10.1007/BF01304852.