\newpage
For monads $N$, $M$ and $NM$, where (\ref{MC}) is assumed,
Barr \& Wells \cite[\S 9.2]{bwttt} give five conditions, (C1) to (C5),
for the existence of a distributive law,
but in fact 
(C2) $\Leftrightarrow$ (C5) and (C3) $\Leftrightarrow$ (C4),
as noted in \S \ref{sec-dl}.
These conditions are given below, as are the proofs of these
equivalences, in the category theory notation.

Michael Barr has observed that there is a duality between (C2,C5) and (C3,C4),
when these are written in category theory notation,
and so the same duality should hold between the proofs 
of implications between these conditions.
The proof (C3) $\Rightarrow$ (C4) is due to this observation.
Interestingly, while the proofs are dual in a notational sense,
the reasons for each step of the proofs are not so.

We indicate the correspondence between the category theory notation and
the notation of this paper.
\begin{align*}
& \mu & \joinNM &: \alpha N M N M \to \alpha N M \\
& \mu F & \joinNM &: \alpha F N M N M \to \alpha F N M \\
& \mu, \mu_1, \mu_2 &  & \joinNM, \joinN, \joinM \\
& \eta, \eta_1, \eta_2 & & \unitNM, \unitN, \unitM \\
& T, T_1, T_2 & & \mapNM, \mapN, \mapM \\
T & = T_2 T_1 &
\mapNM\ & = \mapM \oo \mapN \tag{MC} \\
\mu \oo \eta T &= \id & 
\join \oo \unit & =  \id\ \tag{\ref{MJ5}} \\
\mu \oo T \eta &= \id & 
\join \oo \map\ \unit & =  \id\ \tag{\ref{MJ6}} \\
\mu \oo T \mu & = \mu \oo \mu T & 
\join \oo \map\ \join & = \join \oo \join\  \tag{\ref{MJ7}} 
\end{align*}

We first list the conditions (C1) to (C5).
\begin{align*}
\eta = T_2 \eta_1 \oo \eta_2 & = \eta_2 T_1 \oo \eta_1 \tag{C1} \\
\mu \oo T \eta_2 T_1 & = T_2 \mu_1 \tag{C2} \\
\mu \oo T_2 \eta_1 T & = \mu_2 T_1  \tag{C3} \\
\mu_2 T_1 \oo T_2 \mu & = \mu \oo \mu_2 T_1 T \tag{C4} \\
T_2 \mu_1 \oo \mu T_1 & = \mu \oo T T_2 \mu_1 \tag{C5}
\end{align*}

Finally we show the proofs of equivalence.
Note the duality between the notations of the proofs.
Steps with no reasons given rely on either $T$ or $T_i$ being functors
($T (\phi \oo \psi) = T \phi \oo T \psi$)
or on the definition of composition of natural transformations
($(\phi \oo \psi) T = \phi T \oo \psi T$).
Observe how the duality between the proofs also uses the duality 
between rules (\ref{MJ5}) and (\ref{MJ6}), and the self-duality of
rule (\ref{MJ7}) (see the table above).
But also note the duality between the specific uses made of the 
naturality of $\eta_1$ and of $\mu$.
\newpage 
\begin{description}
\mditem[(C4) $\Rightarrow$ (C3):] \\[-7ex]
\begin{align*} \qquad
\mu \oo T_2 \eta_1 T 
  & = \mu \oo \:(\mu_2 \oo T_2 \eta_2)\: T_1 T \oo T_2 \eta_1 T
    \tag{\ref{MJ6} for $T_2$} \\[-0.5ex]
  & = \mu \oo \mu_2 T_1 T \oo T_2 \eta_2 T_1 T \oo T_2 \eta_1 T \\[-0.5ex]
  & = \mu \oo \mu_2 T_1 T \oo T_2 \:(\eta_2 T_1 \oo \eta_1)\: T \\[-0.5ex]
  & = \mu \oo \mu_2 T_1 T \oo T_2 \eta T \tag{C1} \\[-0.5ex]
  & = \mu_2 T_1 \oo T_2 \mu \oo T_2 \eta T \tag{C4} \\[-0.5ex]
  & = \mu_2 T_1 \oo T_2 \:(\mu \oo \eta T)\: = \mu_2 T_1 \tag{\ref{MJ5} for $T$}
\end{align*}
\mditem[(C3) $\Rightarrow$ (C4):] \\[-7ex]
\begin{align*}
\mu_2 T_1 \oo T_2 \mu 
  & = \mu \oo T_2 \eta_1 T \oo T_2 \mu \tag{C3} \\[-0.5ex]
  & = \mu \oo T_2 \:(\eta_1 T \oo \mu)\: \\[-0.5ex]
  & = \mu \oo T_2 \:(T_1 \mu \oo \eta_1 T^2)\: \tag{$\eta_1$ natural} \\[-0.5ex]
  & = \mu \oo T \mu \oo T_2 \eta_1 T^2 \\[-0.5ex]
  & = \mu \oo \mu T \oo T_2 \eta_1 T^2 \tag{\ref{MJ7} for $T$} \\[-0.5ex]
  & = \mu \oo \mu_2 T_1 T \tag{C3}
\end{align*}
\mditem[(C5) $\Rightarrow$ (C2):] \\[-7ex]
\begin{align*} \qquad
\mu \oo T \eta_2 T_1 
  & = \mu \oo T T_2 \:(\mu_1 \oo \eta_1 T_1)\: \oo T \eta_2 T_1
    \tag{\ref{MJ5} for $T_1$} \\[-0.5ex]
  & = \mu \oo T T_2 \mu_1 \oo T T_2 \eta_1 T_1 \oo T \eta_2 T_1 \\[-0.5ex]
  & = \mu \oo T T_2 \mu_1 \oo T \:(T_2 \eta_1 \oo \eta_2)\: T_1 \\[-0.5ex]
  & = \mu \oo T T_2 \mu_1 \oo T \eta T_1 \tag{C1} \\[-0.5ex]
  & = T_2 \mu_1 \oo \mu T_1 \oo T \eta T_1 \tag{C5} \\[-0.5ex]
  & = T_2 \mu_1 \oo \:(\mu \oo T \eta)\: T_1 = T_2 \mu_1 \tag{\ref{MJ6} for $T$}
\end{align*}
\mditem[(C2) $\Rightarrow$ (C5):] \\[-7ex]
\begin{align*}
T_2 \mu_1 \oo \mu T_1 
  & = \mu \oo T \eta_2 T_1 \oo \mu T_1 \tag{C2} \\[-0.5ex]
  & = \mu \oo \:(T \eta_2 \oo \mu)\: T_1 \\[-0.5ex]
  & = \mu \oo \:(\mu T_2 \oo T^2 \eta_2)\: T_1 \tag{$\mu$ natural} \\[-0.5ex]
  & = \mu \oo \mu T \oo T^2 \eta_2 T_1 \\[-0.5ex]
  & = \mu \oo T \mu \oo T^2 \eta_2 T_1 \tag{\ref{MJ7} for $T$} \\[-0.5ex]
  & = \mu \oo T T_2 \mu_1 \tag{C2} 
\end{align*}
\end{description}

\newpage