module Cat.Monoidal.Monad where

Monoidal monads🔗

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

Duality🔗

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!

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.

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

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 identification between monoidal monads and commutative strengths, the property of being a symmetric monoidal monad is identified with 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-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 =
      Σ-ap monoidal≃commutative (λ m → prop-ext!
        (symmetric-monoidal→symmetric-strength m)
        (λ sy → subst is-symmetric-monoidal-monad (monoidal≃commutative.η m)
          (symmetric-strength→symmetric-monoidal
            (monoidal≃commutative.to m) sy)))
      ∙e Σ-assoc e⁻¹

  1. With respect to the induced lax monoidal structures on and ↩︎


References