
\section{Compound Monads} \label{s-cm}

If $M$ and $N$, with associated functions, are monads,
we can sometimes, but not always,
combine these two monads to form a third.

Compound monads can arise naturally and be practically useful
(\cite{wadler-essence}, \cite{jones-composing}).
% For example, the type \textit{reader} in the SML Basis Library 
% For example, the following type, analogous to the error monad
% (\cite[\S 2.3]{wadler-essence}) is used to represent a the outcome of
% program which either terminates with a result or fails to terminate.
In this section we consider a construction for compound monads
and discuss the conditions under which it is possible.
When further conditions are satisfied,
% for both constructions to be applicable,
then we have the distributive law for monads described by 
Manes \cite{manes} and Barr \& Wells \cite{bwttt}: see \S \ref{s-dl}.
In this case the monads are ``compatible'' \cite[\S 9.2]{bwttt},
and our results show how some of the conditions given in \cite{bwttt}
for this are redundant.

\subsection{Compound Monads \textit{via} Partial Extension} 
\label{s-pext}

Let $M$ be a monad, and consider compound monads
where the compound monad type is $\alpha N M$, that is $(\alpha N) M$.
% which we will just write as $\alpha N M$.
We will call it the monad $MN$, 
in line with the usual notation for composition of functors.
To define a compound monad $MN$, we will need a function \extNM,
which ``extends'' a function $f$ 
from a ``smaller'' domain, $\alpha$, to a ``larger'' one, $\alpha N M$.
Consider, therefore, a ``partial extension'' function 
\pext\ which does part of this job:
\begin{align*}
\extNM & : (\alpha \leadsto \beta N M) \to (\alpha N M \leadsto \beta N M) \\
\pext & : (\alpha \leadsto \beta N M) \to (\alpha N \leadsto \beta N M) \\
\pext & : (\alpha \leadsto_M \beta N) \to (\alpha N \leadsto_M \beta N) 
\end{align*}
We will prove that 
rules (\ref{pextru}) to (\ref{pextfun}) are sufficient to define
a compound monad using such a function \pext.
We assume nothing about the functions \oNM\ or \unitNM,
except that they have the appropriate types,
or that $N$ is a monad. 
% We need not assume that $N$ is a monad. 
% although in many examples
% rules (\ref{pextru}) to (\ref{pextfun}) are proved to hold for any monad $M$,
% when setting $M$ to the identity monad gives a monad $N$.
%
\comment{
\begin{table}%[!hbt]
\caption{Monad rules for a compound monad using \pext} 
\label{tab-prules}
\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
pext f \oM\ \unitNM & = & f & (\pextru) \\
pext \unitNM & = & \unitM & (\pextlu) \\
pext (g \oNM\ f) & = & pext g \oM\ pext f & (\pextfun) \\[2ex]
\kjoin & = & \pext\ \unitM & (kjoin-pext) \\ 
\kmap\ f & = & \pext\ (\unitNM\ \oM\ f) & (kmap-pext)  
\end{tabular}
} \end{center} 
\end{table}
}
%
\setcounter{equation}{0}
\renewcommand\theequation{E\arabic{equation}K}
\begin{align} % \label{tab-prules} was (\ref{pextru}) to (\ref{pextfun})
\label{pextru} \pext\ f \oM \unitNM & = f \\[-0.5ex]
\label{pextlu} \pext\ \unitNM & = \unitM \\[-0.5ex]
\label{pextfun} \pext\ (g \oNM f) & = \pext\ g \oM \pext\ f \\[1ex]
% \stepcounter{equation} not when using (E3a)
\label{kjoin-pext} \kjoin & = \pext\ \unitM \\[-0.5ex]
\label{kmap-pext} \kmap\ f & = \pext\ (\unitNM \oM f) \\[1ex] 
\label{ompext} g \oNM f & = \pext\ g \oM f \\[-0.5ex]
\pext\ g & = g \oNM \unitM \tag{\ref{extom}K}
\end{align}

Observing how the second type expression for \pext\ above
looks like that for \ext\ in \S\ref{s-monads},
and by comparing (\ref{pextru}) to (\ref{pextfun}) with
(\ref{extru}) to (\ref{extfun})
we see that we have the three rules needed for a monad $N$
{in \KM, the Kleisli category of $M$}.
We will refer to this monad as \NKM.
Its \unit\ is \unitNM; recall that the identity and composition in the
category are \unitM\ and \om.
%
\begin{align*}
\unitM & : \alpha \leadsto_M \alpha \\[-0.5ex]
\unitNM & : \alpha \leadsto_M \alpha N \\[-0.5ex]
\oM & : (\beta \leadsto_M \gamma) \to (\alpha \leadsto_M \beta) \to
  (\alpha \leadsto_M \gamma) 
\end{align*}

Thus the treatment of a single monad described in 
\S\ref{s-monads} applies to this monad.
We define the counterparts of \map\ and \join, calling them \kmap\ and \kjoin:
note how rules (\ref{kjoin-pext}) and (\ref{kmap-pext}) 
correspond to (\ref{joinext}) and (\ref{mapext}).
As in \S\ref{s-monads}, we deduce (\ref{ompext}), giving 
\oNM\ in tems of \pext.
We will refer to rule ($r$) for this monad as ($r$K);
likewise we may refer to rules ($r$M), ($r$N) or ($r$MN)
where necessary.
\comment{ TABLE OMITTED 
The various functions and theorems involved have counterparts 
of which examples are tabulated below, % Table~\ref{tab-corresp},
where the left-hand side shows the standard
treatment (set out as for a monad $N$),
and the right-hand side shows the monad \NKM\ in \KM.
% 
\begin{align*}
id &: \alpha \to \alpha  & \unitM &: \alpha \to \alpha M  \\[-0.5ex]
\unitN &: \alpha \to \alpha N  & \unitNM &: \alpha \to \alpha N M  \\[-0.5ex]
\mapN &: (\alpha \to \beta) \to \alpha N \to \beta N  &
\kmap &: (\alpha \to \beta M) \to \alpha N \to \beta N M  \\[-0.5ex]
\joinN &: \alpha N N \to \alpha N  & 
\kjoin &: \alpha N N \to \alpha N M  \\[-0.5ex]
\extN &: (\alpha \to \beta N) \to \alpha N \to \beta N  &  
\pext &: (\alpha \to \beta N M) \to \alpha N \to \beta N M  \\[-0.5ex]
\extN\ g &= g \oN \id & \pext\ g &= g \oNM \unitM \\[-0.5ex]
g \oN f &= \extN\ g \oo f & g \oNM f &= \pext\ g \oM f \\[-0.5ex]
\joinN &= \extN\ id & 
\kjoin &= \pext\ \unitM \\[-0.5ex] 
\mapN\ f &= \extN\ (\unitN \oo f) & 
\kmap\ f &= \pext\ (\unitNM \oM f) \\[-0.5ex] 
\extN\ f &= \joinN \oo \mapN\ f & 
\pext\ f &= \kjoin \oM \kmap\ f \\[-0.5ex] 
h \oN f &= (h \oN id) \oo f &
h \oNM f &= (h \oNM \unitM) \oM f % \\[-0.5ex] 
\end{align*}
END TABLE OMITTED }

% Where necessary to avoid ambiguity, we will refer to rule $(r)$ for monad
% $M,N$ or $MN$ as ($r$M), ($r$N) or ($r$MN). 

We also obtain rules (\ref{KMJ1}) to (\ref{Kextjm})
which are the counterparts of (\ref{MJ1}) to (\ref{extjm}),
and these hold by Theorem~\ref{t-e3-umj7} for this monad \NKM.
These are set out in Appendix~\ref{a-cm}.
Likewise % (\ref{Kexto}) and 
Theorem~\ref{thm-ext-join-iff} holds for \NKM.
% Then, just as in \S\ref{s-monads}, these seven rules,
% with \pext\ and \oNM\ defined from \kjoin\ and \kmap\
% by (\ref{extjm}K) and (\ref{omext}K),
% are sufficient to show rules (\ref{pextru}) to (\ref{pextfun})
% and the converse definitions of \kjoin\ and \kmap\ in terms of \pext,
% (\ref{kjoin-pext}) and (\ref{kmap-pext}).
%
% following now in Appendix
% \setcounter{equation}{0}%
% \renewcommand\theequation{\arabic{equation}K}%
% \begin{eqnarray} % \label{tab-kmjrules} was (\ref{KMJ1}) to (\ref{Kextjm})
% \kmap\ \unitM & = &  \unitM \label{KMJ1} \\[-0.5ex]
% \kmap\ f \oM \kmap\ g & = &  \kmap\ (f \oM g) \label{KMJ2} \\[-0.5ex]
% \unitNM \oM f & = &  \kmap\ f \oM \unitNM \label{KMJ3} \\[-0.5ex]
% \kjoin \oM \kmap\ (\kmap\ f) & = &  \kmap\ f \oM \kjoin
  % \label{KMJ4} \\[-0.5ex]
% \kjoin \oM \unitNM & = &  \unitM \label{KMJ5} \\[-0.5ex]
% \kjoin \oM \kmap\ \unitNM & = &  \unitM \label{KMJ6} \\[-0.5ex]
% \kjoin \oM \kmap\ \kjoin & = &  \kjoin \oM \kjoin\  \label{KMJ7} \\[1ex]
% pext\ f & = & kjoin \oM \kmap\ f \label{pext-kjm} \label{Kextjm} \\[1ex]
% pext\ (g \oM f) & = & pext\ g \oM \kmap\ f  \label{Kexto} 
% \end{eqnarray}%
%
This monad \NKM\ in \KM, the Kleisli category for $M$,
gives rise to a further Kleisli category,
which we may describe as the Kleisli category for \NKM\ in \KM.
%the Kleisli category for $M$.
Its identity is \unitNM\ and its composition function is \oNM.
It turns out that this is also the Kleisli category of a monad $MN$ in 
$\mathcal C$.  
% Where necessary to avoid ambiguity, we will refer to rule $(r)$ for monad
% $M,N$ or $MN$ as ($r$M), ($r$N) or ($r$MN). 
% Note also that the two rules (\ref{pextlu}) and (\ref{pextfun})
% express the fact that \pext\ is (the action on arrows of) a functor,
% from this compound Kleisli category to \KM. %the Kleisli category for $M$.
%
\comment{ TREATMENT VIA A RULES OMITTED 
This monad can also be characterised by four rules analogous to 
(\ref{krid}) to (\ref{omoass}):
that is, the rules (\ref{krid}K) to (\ref{omoass}K).
We also show (\ref{extom}K). % and (\ref{omoass}K).
%
\setcounter{saveeqn}{\value{equation}}
\setcounter{equation}{0}
\renewcommand\theequation{A\arabic{equation}K}
\begin{align} 
% \label{tab-assNMrules} was (\ref{kridK}) to (\ref{oNMoMouass})
f \oNM \unitNM & = f \label{kridK} \\[-0.5ex]
\unitNM \oNM f & = f \label{klidK} \\[-0.5ex]
h \oNM (g \oNM f) & = (h \oNM g) \oNM f \label{kassK} \\[-0.5ex]
% (h \oNM \unitM) \oM f & = h \oNM f \label{oNMoMouass} \\[1ex] 
(h \oNM g) \oM f & = h \oNM (g \oM f) \\
\pext\ g & = g \oNM \unitM 
\end{align}
%
Now, to show that $MN$ is a compound monad, we also need to show 
four rules analogous to (\ref{krid}) to (\ref{omoass}),
namely (\ref{krid}MN) to (\ref{omoass}MN).
Of these, the first three, (\ref{krid}MN) to (\ref{kass}MN),  
are the same as (\ref{krid}K) to (\ref{kass}K);
only (\ref{omoass}MN) is different.
So to show that $MN$ (defined by \unitNM\ and \oNM) is a monad, 
we need only show (\ref{omoass}MN), and to do this we have available
both (\ref{omoass}K) and (\ref{omoass}M).
\begin{align}
(h \oNM g) \oo f & = h \oNM (g \oo f) \tag{\ref{omoass}MN} \\[-0.5ex]
(h \oM g) \oo f & = h \oM (g \oo f) \tag{\ref{omoass}M}
\end{align}
END TREATMENT VIA A RULES OMITTED }

\begin{theorem}[\texttt{Ko\_pext\_cm}] \label{thm-pext-k}
% need HOL thms for (PE) and (J1S) 
Assume that $M$ is a monad and that functions \pext, \oNM and \unitNM\ 
of the appropriate types are given,
satisfying rules (\ref{pextru}) to (\ref{pextfun}).
Then, using (\ref{EC}) to define \extNM, 
\unitNM, \extNM\ and \oNM\  define a monad, and
(\ref{PE}) and (\ref{J1S}) hold.
\begin{align}
% \label{ompext} g \oNM\ f & = \pext\ g \oM\ f \\
\label{EC} \extNM\ f & = \extM\ (\pext\ f) \tag{EC} \\
\label{PE} \pext\ f & = \extNM\ f \oo \unitM \tag{PE} \\
\label{J1S} \extM\ (\extNM\ f) & = \extNM\ f \oo \joinM \tag{J1S} % \\
% \label{E1D} \extNM\ f \oo \mapM\ \unitN & = \extM\ f \tag{\ref{extru}D} 
% \label{pextcong} \pext\ f = \pext\ g & \Rightarrow f = g \\
\end{align}
\end{theorem}

\begin{proof}
By rules (\ref{pextru}) to (\ref{pextfun}), \pext, \oNM\ and \unitNM\
give a monad in \KM.
% and so rules (\ref{krid}K) to (\ref{omoass}K) are satisfied. 
\comment{ PROOF VIA A RULES OMITTED 
Since $M$ is a monad, (\ref{omoass}M) holds, and so we use (\ref{omoass}M)
and (\ref{omoass}K) to show (\ref{omoass}MN) 
by setting either $h$ or $g$ to be \unitM\ 
(and using (\ref{krid}) or (\ref{klid})) in the following:
%
% \begin{align*}
% (h \oNM id) \oo f &= ((h \oNM \unitM) \oM id) \oo f 
    % \tag{\ref{omoIass}K} \\[-0.5ex]
  % &= (h \oNM \unitM) \oM f = h \oNM f
    % \tag{\ref{omoIass}M, \ref{omoIass}K}
% \end{align*}
% 
% To get (\ref{omoass}MN) from (\ref{omoass}M) and (\ref{omoass}K),
\begin{align*}
 (k \oNM (h \oM g)) \oo f &= ((k \oNM h) \oM g) \oo f 
    \tag{\ref{omoass}K} \\[-0.5ex]
= (k \oNM h) \oM (g \oo f) &= k \oNM (h \oM (g \oo f)) 
    \tag{\ref{omoass}M,\ref{omoass}K} \\[-0.5ex]
% &= (k \oNM h) \oM (g \oo f) 
    % \tag{\ref{omoass}M} \\[-0.5ex]
% &= k \oNM (h \oM (g \oo f)) 
    % \tag{\ref{omoass}K} \\[-0.5ex]
= k \oNM ((h \oM g) \oo f) 
    \tag{\ref{omoass}M} 
\end{align*}
END PROOF VIA A RULES OMITTED }

% \begin{description}
% 
% % \mditem[(\ref{EC}):]
% % By (\ref{extom}M) and (\ref{extom}MN) this is (\ref{omext}K). 
% 
% \mditem[(\ref{PE}):] % By (\ref{omext}MN) this is (\ref{extom}K). 
% This follows from (\ref{EC}) and (\ref{extru}M).
% 
% \mditem[(\ref{J1S}):] 
% By Theorem~\ref{thm-ext-join-iff} for $M$, \ref{ej3} $\Rightarrow$ \ref{ej1}, 
% this follows from (\ref{EC}).
% 
% \mditem[(\ref{E1D}):] 
% By (\ref{PE}) and (\ref{extru}MN), $\pext\ f \oo \unitN = f$.
% Thus, by (\ref{EC}) and (\ref{exto}M),
% $\extNM\ f \oo \mapM\ \unitN = \extM\ (\pext\ f \oo \unitN) = \extM\ f$.
% \end{description}
(\ref{PE}) follows from (\ref{EC}) and (\ref{extru}M).

By Theorem~\ref{thm-ext-join-iff} for $M$, \ref{ej3} $\Rightarrow$ \ref{ej1}, 
(\ref{J1S}) follows from (\ref{EC}).

It is now trivial to use (\ref{EC}) to prove rules 
(\ref{extru}MN) to (\ref{extfun}MN).
Rules (\ref{extlu}MN) and (\ref{extfun}MN)
each follows directly 
from (\ref{EC}) and the same rule for $M$ and for \NKM.
% and the corresponding rule from among (\ref{pextru}) to (\ref{pextfun}).
Rule (\ref{extru}MN) is proved by (\ref{EC}), (\ref{omext}M) and
(\ref{extru}K).
\qed
\end{proof}

% In Theorem~\ref{thm-pext-k} we proved
% rules (\ref{krid}) to (\ref{omoass}) for $MN$,
% so proving that $MN$ is a monad.
% However, we note that it is also trivial to prove rules 
% (\ref{extru}) to (\ref{extfun}) for $MN$.
% In fact, using (\ref{EC}),
% each rule for $MN$ follows from the same rule for $M$ 
% and the corresponding rule from among (\ref{pextru}) to (\ref{pextfun}).

\comment{
At this point we have, by (\UC) and (\extcomp), that
\begin{quote} \textit{
map\NM\ f = ext\NM\ (unit\NM\ \oo\ f) = \\ 
  \mbox{} \qquad ext\M\ (pext (unit\M\ \oo\ (unit\N\ \oo\ f))) =
  (ext\M\ \oo\ pext \oo\ kl\M\ \oo\ kl\N) f
} \end{quote} 
that is, \map\NM\ is the composition of four functors.
}

We may next ask which compound monads can be constructed from such a
function \pext, satisfying rules (\ref{pextru}) to (\ref{pextfun}).
% Taking as read the requirement that the monadic type is $(\alpha N) M$,
% (which we will regard as implicit in the notation $MN$),
% the previous theorem provides two necessary conditions, 
% namely that (\ref{J1S}) and (\ref{E1D}) hold.
% In fact, these conditions, which are equivalent, are also sufficient.
% since (\extcomp) tells us
The previous theorem provides a necessary condition, 
namely that (\ref{J1S}) holds.
In fact, this condition is also sufficient.
The key step in the proof of this is to define \pext\ from \extNM\
by applying Theorem~\ref{thm-ext-join-iff} for $M$,
\ref{ej1} $\Rightarrow$ \ref{ej2}, to (\ref{J1S}).
%
We further note that the special case $f = id$ of (\ref{J1S})
(called (\ref{J1}), shown below) implies it in general.
% $\forall f. \exists g. \ext_{NM}\ f = \ext_M\ g$.
% By Theorem~\ref{thm-ext-join-iff} this is equivalent to 
% $\forall f. \ext_M\ (\ext_{NM}\ f) = \ext_{NM}\ f \circ \join_M$.

\begin{theorem}[\texttt{cm\_if\_J1o,J1\_IMP\_ext\_pext}] 
  \label{thm-when-pext}
Let $M$ and $MN$ be monads, such that 
(\ref{J1S}) (see Theorem~\ref{thm-pext-k}) holds.
% \textbf{(\UC)} & \unitNM\ & = & \unitM\ \oo\ \unitN \\
% \textbf{(\J1S)} & \ext\M\ (\ext\NM\ f) & = & \ext\NM\ f \oo\ \join\M
% either (\ref{J1S}) or (\ref{E1D}) (see Theorem~\ref{thm-pext-k}) hold.
Then 
% both (\ref{J1S}) and (\ref{E1D}) hold, and
\oNM\ and \unitNM\ also define a monad in the category \KM,
and, using (\ref{PE}) to define \pext, (\ref{EC}) holds.
\end{theorem}

This shows that, given a monad $M$, that the compound monads $MN$ 
obtainable using the construction via a monad $N$ in \KM\ are precisely
the monads $MN$ such that (\ref{J1S}) (or (\ref{J1})) is satisfied.
See theorem \texttt{cm\_Ko\_J1S} in Appendix~\ref{a-cm}. 

\subsection{Compound Monads via a Distributive Law} \label{s-dl}

Jones \& Duponcheel \cite{jones-composing} consider when a
compound monad may be obtained using various constructions.
They consider only compound monads which satisfy (\ref{UC}) and (\ref{MC}),
and we will assume these without further comment.
In \S3.2 they showed a construction using a function \prd,
satisfying certain properties P(1) to P(4), 
which can be related to (\ref{extru}K) to (\ref{extfun}K).
In \S4.1 they showed that this construction is applicable
if and only if their condition J(1) (which is our (\ref{J1})) holds.
In fact these are related:
% \prd\ and \pext\ are related:
$\prd = \pext\ \id$ and $\pext\ f = \prd \oo \mapN\ f$.

Similarly in \S3.3 and \S4.2 they showed a construction using a function \dorp,
satisfying certain properties (their D(1) to D(4)), 
which is applicable if and only if their condition J(2) (our (\ref{J2})) holds.
Then in \S3.4 and \S4.3 they showed a construction using a function \swap,
satisfying certain properties S(1) to S(4), 
which is applicable if and only if J(1) and J(2) hold.
%
\begin{align*}
\unitNM\ & = \unitM \oo \unitN \label{UC} \tag{UC} \\[-0.5ex]
\mapNM\ f & = \mapM\ (\mapN\ f) \label{MC} \tag{MC} \\
\extM\ \joinNM & = \joinNM \oo \joinM \label{J1} \tag{J1} \\
\extNM\ (\mapM\ \joinN) & = \mapM\ \joinN \oo \joinNM \label{J2} \tag{J2}
\end{align*}

They observe that both J(1) and J(2) are of a certain form, 
which is that of Theorem~\ref{thm-ext-join-iff}\ref{ej1}.
Therefore their conditions are, in effect, 
that \joinNM\ is of the form $\extM\ f$, and
that \mapM\ \joinN\ is of the form $\extNM\ g$.
% and $g = \mapM\ \joinN \oo \unitNM$, which is,
% by (\ref{UC}), (\ref{MJ3}M) and (\ref{MJ5}N), $g = \unitM$.
% 
% Thus it can be shown that either J(1) or J(2) implies that
% $\extNM\ \unitM \oo \mapM\ \unitN = \id$.

% \subsection{Relation to the distributive law for monads} 
% \label{sec-dl}
Barr \& Wells \cite[\S 9.2]{bwttt}
describe a construction of compound monads using
a ``distributive law'' $\lambda$.
% Manes \cite{manes} also describes a ``distributive law'' for monads,
% at Chapter~4, pages 311-2, Definition~3.6, and page~334, Exercise~6.
A distributive law for monads $M$ and $N$ is
a natural transformation $\lambda$ satisfying four rules shown below.
In fact $\lambda$ is the \swap\ of 
% In functional programming notation, we call it \swap, following
\cite{jones-composing}.
%
% \begin{figure}
\setcounter{equation}{0}
\renewcommand\theequation{DL\arabic{equation}}
\begin{align*}
\swap \oo \mapN\ \unitM & = \unitM \\[-0.5ex]
  \lambda \oo N \eta_M & = \eta_M N 
  \label{BWD1} \tag{D1} \\
\swap \oo \unitN & = \mapM\ \unitN \\[-0.5ex]
  \lambda \oo \eta_N M & = M \eta_N 
  \label{BWD2} \tag{D2} \\
\swap \oo \mapN\ \joinM & = \extM\ \swap \oo \swap \\[-0.5ex]
  \lambda \oo N \mu_M & = \mu_M N \oo M \lambda \oo \lambda M
  \label{BWD3} \tag{D3} \\
\swap \oo \joinN & = \mapM\ \joinN \oo \swap \oo \mapN\ \swap \\[-0.5ex]
  \lambda \oo \mu_N M & = M \mu_N \oo \lambda N \oo N \lambda
  \label{BWD4} \tag{D4}
  \end{align*}
% \caption{Conditions of Barr \& Wells for a distributive law $\lambda$ (\swap)}
% \label{f-dl}
% \end{figure}
 
Conversely, they define five conditions, (C1) to (C5),
for monads $M$, $N$ and $MN$ to be ``compatible''. 
(C1) is (\ref{UC}), and their treatment presupposes (\ref{MC}). 
In fact (C4) and (C5) are precisely (\ref{J1}) and
(\ref{J2}).
They show that $MN$ is compatible with $M$ and $N$ if and only if
it can be constructed using a distributive law.
%
% \begin{figure}
\begin{align*}
% \eta = M \eta_1 \oo \eta_M & = \eta_M N \oo \eta_N \tag{C1} \\
\extNM\ \unitM & = \mapM\ \joinN 
\\[-0.5ex] 
\mu \oo MN \eta_M N & = M \mu_N 
\tag{C2} \\
\joinNM \oo \mapM\ \unitN & = \joinM 
\\[-0.5ex] 
\mu \oo M \eta_N MN & = \mu_M N  
\tag{C3} \\
\extM\ \joinNM & = \joinNM \oo \joinM 
\\[-0.5ex] 
\mu_M N \oo M \mu & = \mu \oo \mu_M N MN 
\tag{C4} \\
\mapM\ \joinN \oo \joinNM & = \extNM\ (\mapM\ \joinN) 
\\[-0.5ex] 
M \mu_N \oo \mu N & = \mu \oo MN M \mu_N 
\tag{C5}
\end{align*}
% \caption{Conditions of Barr \& Wells for monads to be compatible}
% \label{f-cc}
% \end{figure}

In fact the definition of compatibility can be simplified,
since two of the five conditions given by 
Barr \& Wells in \cite[\S 9.2]{bwttt} are redundant.
See Appendix~\ref{a-cc} for the \HOLw\ theorems.
\begin{theorem} \label{t-C2534}
(C2) $\Leftrightarrow$ (C5) and (C3) $\Leftrightarrow$ (C4)
\end{theorem}
\begin{proof}
(C2) $\Rightarrow$ (C5): this is just Theorem~\ref{thm-ext-join-iff} for $MN$,
\ref{ej3} $\Rightarrow$ \ref{ej1} 

(C5) $\Rightarrow$ (C2): by Theorem~\ref{thm-ext-join-iff},
\ref{ej1} $\Rightarrow$ \ref{ej2},
$\mapM\ \joinN = \extNM\ f$ where $f = \mapM\ \joinN \oo \unitNM = 
 % \mapM\ \joinN \oo \unitM \oo \unitN = 
 \unitM \oo \joinN \oo \unitN = \unitM$,
by (\ref{UC}), (\ref{MJ3}M) and (\ref{MJ5}N)

(C4) $\Rightarrow$ (C3): by Theorem~\ref{thm-ext-join-iff} for $M$,
\ref{ej1} $\Rightarrow$ \ref{ej2},
we get 
\begin{align*} 
\joinNM \oo \mapM\ \unitN & =
  \extM\ (\joinNM \oo \unitM) \oo \mapM\ \unitN  \\
 & = \extM\ (\joinNM \oo \unitM \oo \unitN) \tag{\ref{extjm}M,\ref{MJ2}M} \\
 & = \extM\ \id = \joinM \tag{\ref{UC},\ref{MJ5}MN} 
\end{align*} 

(C3) $\Rightarrow$ (C4): 
from (C3) we prove the stronger (C3S) 
% which can be proved from (C3)
using (\ref{extjm}MN), (\ref{extjm}M), (\ref{MC}),
(\ref{MJ2}M) and (\ref{MJ3}N). 
Substituting the right-hand sides of this and (C3)
into the statement of (C4) gives (*), which holds by (\ref{MJ7}MN). 
\begin{gather*}
\extNM\ f \oo \mapM\ \unitN = \extM\ f \tag{C3S} \\
\extNM\ \joinNM \oo \mapM\ \unitN
 = \joinNM \oo \joinNM \oo \mapM\ \unitN \tag{*}
\end{gather*}
\end{proof}%

There are some intriguing aspects to Theorem~\ref{t-C2534}.
%
As Michael Barr pointed out,
there is a duality between (C2,C5) and (C3,C4),
when these are written in category theory notation
(for $X_1 \oo X_2 \oo \ldots$, 
you reverse the order of the symbols \emph{within} each $X_i$,
and interchange $M$ and $N$).
In the same way, (D2) and (D4) are dual to (D1) and (D3).
% Note the same sort of duality in the single monad rules: 
% (\ref{MJ5}) and (\ref{MJ6}) are dual, and (\ref{MJ7}) is self-dual.
Further, it seems to be possible to dualise the relevant proofs.  
Often the reasons for proof steps change.
For example, $M (f \oo g) = M f \oo M g$ when $M$ is a functor, whereas 
$(f \oo g) M = f M \oo g M$ (for natural transformations $f,g$) by definition.
And when the proofs are written out in this notation 
(see Appendix~\ref{a-duality})
a step depending on the naturality of $\mu$ becomes a step depending on the
naturality of $\eta_N$.

These observations by Michael Barr enabled us to find the proof of
(C3) $\Rightarrow$ (C4).
At first we had conjectured (C3) $\Rightarrow$ (C4) but were unable to prove it.
On the other hand its dual, the proof (C2) $\Rightarrow$ (C5),
was an instance of the rather trivial Theorem~\ref{thm-ext-join-iff}.
% which follows trivially from the rules
% (\ref{extru}) to (\ref{extfun}) defining a monad. 
So to find the proof of (C3) $\Rightarrow$ (C4),
we translated our simple proof of (C2) $\Rightarrow$ (C5) into the 
steps shown in Appendix~\ref{a-duality}, and dualised them.  

Note further that although (C4) and (C5) have this duality as they stand;
however their similarity that they are both of the form of 
Theorem~\ref{thm-ext-join-iff}\ref{ej1} applies to the symmetric equivalent of 
(C5).
% 
Another curious point is that the identity
$\extNM\ \unitM \oo \mapM\ \unitN = \id$
follows from \emph{either} (C2) \emph{or} (C3).

We have now shown that the compatibility conditions (C2) to (C5) are
just J(1) and J(2) of Jones \& Duponcheel \cite[\S 4]{jones-composing}.
Since their S(1) is just the requirement that \swap\ is a natural
transformation, 
it follows that their conditions S(2) to S(4) on \swap\ must be equivalent to 
(D1) to (D4). In fact S(2) and S(3) are just (D2) and (D1)
respectively.
For S(4), define \prd\ and \dorp\ from \swap, then S(4) is as shown.
We indicate in Appendix~\ref{a-bw-jd} how to prove S(4) directly from
(D3) and (D4), and vice versa. 
\begin{gather*}
\prd  = \mapM\ \joinN \oo \swap \qquad \dorp  = \extM\ \swap \\
\prd \oo \mapN\ \dorp  = \dorp \oo \prd \tag*{S(4)}
\end{gather*}

% We now indicate how we proved that a compound monad satisfying the
We now indicate how we used the properties of the monad \NKM\
to obtain easy proofs that a compound monad satisfying the
compatibility conditions provides a distributive law.
By Theorem~\ref{thm-when-pext}, compatibility conditions (C3/C4),
ie (\ref{J1}), imply that the monad NM
is derived from a monad \NKM\ in the Kleisli category \KM.
%
This gives us functions \pext, \kjoin\ and \kmap.

\begin{lemma} \label{lem-pko}
Assume $MN$ is constructed as in \S \ref{s-pext}. Then 
\begin{align*}
\pext\ (g \oo f) & = \pext\ g \oo \mapN\ f \label{pexto} \tag{PO} \\[-0.5ex]
\kmap\ (g \oo f) & = \kmap\ g \oo \mapN\ f \label{kmapo} \tag{KO}
\end{align*}
\end{lemma}

\begin{proof}
(\ref{pexto}): Uses
  (\ref{PE}), (\ref{extjm}MN), (\ref{MJ2}MN), 
    (\ref{MC}), (\ref{MJ3}M) and (\ref{PE}) again.

(\ref{kmapo}): Uses 
  (\ref{mapext}K), (\ref{omext}M), (\ref{pexto}) and
  (\ref{omext}M) and (\ref{mapext}K) again.  
\qed \end{proof}

If we assume also the compatibility condition (C2), ie (\ref{J2}),
then, using (\ref{PE}), (C2) and (\ref{MJ3}M), we can
show $\kjoin = \unitM \oo \joinN$.
% the expression for \kjoin\ shown below.
We define the distributive law $\lambda$, ie, \swap,
as in \cite[\S 9.2]{bwttt} (and in \cite[\S 4.3]{jones-composing}),
namely \mbox{$\swap = \pext\ (\mapM\ \unitN)$,} which is equal to 
$\kmap\ \id$ (see Appendix~\ref{a-cc-dl} for these).
With these results we can translate the conditions (D1) to (D4),
% the requirement that \swap\ be a natural transformation, 
and S(4) of Jones \& Duponcheel \cite{jones-composing}, 
into the following, which are all immediate results about the monad \NKM\
in the Kleisli category \KM.
%
\setcounter{equation}{0}
\renewcommand\theequation{DL\arabic{equation}}
\begin{align*}
\kmap\ \unitM & = \unitM \label{BWD1'} \tag{D1$'$} \\
\kmap\ \id \oM \unitNM & = \unitNM \oM \id
  \label{BWD2'} \tag{D2$'$} \\
\kmap\ (\id \oM \id) & = \kmap\ \id \oM \kmap\ \id 
  \label{BWD3'} \tag{D3$'$} \\
\kmap\ \id \oM \kjoin & = \kjoin \oM \kmap\ (\kmap\ \id)
  \label{BWD4'} \tag{D4$'$} \\
% \kmap\ ((\unitM \oo f) \oM \id) & = \kmap\ (\unitM \oo f) \oM \kmap\ \id 
  % \label{S1'} \tag{$\lambda$ natural} \\
\pext\ (\kmap\ \id \oM \id) & = \kmap\ \id \oM \pext\ \id
  \label{S4'} \tag{S4$'$} 
  \end{align*}

(\ref{BWD1'}) to (\ref{BWD4'}) are just instances of 
(\ref{MJ1}K), (\ref{MJ3}K), (\ref{MJ2}K) and (\ref{MJ4}K),
and (\ref{S4'}) follows from 
Theorem~\ref{thm-ext-join-iff} for \NKM, 
\ref{ej3} $\Rightarrow$ \ref{ej4}. 
That \swap\ is a natural transformation is more easily proved using its
definition from $M$ and $N$ and natural transformations 
$\joinNM, \unitM$ and $\unitN$, 
but a proof using the conditions for the monad \NKM\ in \KM\ 
is in Appendix~\ref{a-swap-nt}.

To prove the converse, that if the conditions 
(\ref{BWD1}) to (\ref{BWD4}) hold, then 
we can construct a compound monad $MN$ which satisfies the compatibility
conditions, is not quite so easy, but for this proof also we
have found the easiest
way is again to use the conditions for a monad \NKM\ in \KM.
We prove the seven rules (\ref{MJ1}K) to (\ref{MJ7}K).
Details are in Appendix~\ref{a-DL-to-K}. 


