Cocommutative bimonads: Why does this diagram commute?

Question

1. Definitions
Let $(C, \otimes,I, a, l,r,c)$ be a monoidal category with braiding $c:\otimes \rightarrow\otimes ^{op}$. Let $(S,\mu,\eta,\tau,\theta)$ be a bimonad on $C$. Following Turaev and Virelizier in Monoidal Categories and Topological Field Theory we define a bimonad as follows:

• $(S,\mu,\eta)$ is a monad on $C$ with multiplication $\mu$ and unit $\eta$.
• $(S, \tau,\theta)$ is an oplax monoidal functor with natural transformation $\tau: S \circ \otimes \Longrightarrow \otimes \circ (S,S)$ and morphism $\theta: S(I) \rightarrow I$.
• The multiplication $\mu$ and the unit $\eta$ are comonoidal natural transformations (that is monoidal natural transformations of the respective lax monoidal functors $C^{op} \rightarrow C^{op}$). Here we consider the oplax monoidal functor $(S^2, \tau \circ S(\tau), \theta \circ S(\theta))$ where $S(\tau)$ and $S(\theta)$ denote whiskered natural transformations.

Let $S$ be cocommutative, i.e. $c \circ \tau = \tau \circ S(c)$ holds.

2. Problem
I am trying to show that in the above setting the following diagram in $C$ commutes for all $X,Y \in Obj(C)$:

$$\require{AMScd} \begin{CD} S(X \otimes X \otimes Y \otimes Y) @>{\tau_{X \otimes X, Y \otimes Y}}>> S(X \otimes X) \otimes S(Y \otimes Y)\\ @V{S(id_X \otimes c_{X,Y} \otimes id_Y)}VV @V{\tau_{X, X} \otimes \tau_{Y,Y}}VV \\ S(X \otimes Y \otimes X \otimes Y) @. S(X) \otimes S(X) \otimes S(Y) \otimes S(Y)\\ @V{\tau_{X \otimes Y, X \otimes Y}}VV @V{id_{S(X)}\otimes c_{S(X), S(Y)}\otimes id_{S(Y)}}VV \\ S(X \otimes Y) \otimes S(X \otimes Y) @>{\tau_{X, Y} \otimes \tau_{X, Y}}>> S(X) \otimes S(Y) \otimes S(X) \otimes S(Y) \end{CD}$$

The commutativity of this diagram seems similar to the cocommutativity of $S$. Informally: "Pulling tensor products out of $S$ and then braiding on the outside is the same as braiding on the inside and then pulling tensor factors out of $S$." I tried using the cocommutativity to write the above diagram as a composite of commuting diagrams (diagram chasing), however I keep getting more and more diagrams inside the one above without being able to connect all nodes.

3. Questions
Any ideas? Is there a type of graphical calculus I could use to tackle the problem?

Answer 1

Can't you just say that this diagram

commutes because

1. is just two different ways to "completely unpack" $S(XXYY)$
2. commutes because $S$ is natural at $c$
3. is your cocommutativity assumption
4. same as 1.