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.Diagram.Monad
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

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 $\mathcal{C}$ is a monad on $\mathcal{C}$ 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 transformations¹; this requires a total of four conditions.

That $\eta$ 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 $\epsilon$ to be ${\eta }_1\text{.}$

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

The diagram on the left automatically commutes because of the monad laws, since $\epsilon$ is forced to be ${\eta }_1\text{,}$ 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 ) 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 ${\mathcal{C}}^{\mathrm{rev}}$ from a monoidal monad on $\mathcal{C}\text{.}$

  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!

The guiding intuition is that the monoidal structure on $M$ 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))

    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 $\phi \text{!}$

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 ${\eta }_1$ 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 $\tau \sigma \tau \sigma$ to $\tau \sigma \text{:}$ we first need to commute the two strengths in the middle to obtain $\tau \tau \sigma \sigma \text{,}$ and then use the fact that two consecutive applications of the strengths result in just one after commuting with $\mu \text{.}$ Concretely, this manifests as the following diagram, where the commutation of the strengths is highlighted.

The morphisms labelled $(M)\mu$ alternate between being $\mu$ and $M\mu \text{,}$ in a way that is allowed by the associativity law because they are followed by $\mu \text{.}$

      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 )
      (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 $\phi$ we started with; moreover, the monoidal unit $\epsilon$ becomes ${\eta }_1\text{,}$ 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

  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ˢ
      (_ , 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.

    module _ (m : Monoidal-monad-on Cᵐ monad) where
      open Monoidal-monad-on m

      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:

    module _ ((s , s-comm) : Σ _ is-commutative-strength) where
      open Monad-strength s

      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 ) (hlevel )
      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⁻¹