% APPENDIX

\renewcommand\theenumi{\roman{enumi}}
\renewcommand\labelenumi{(\theenumi)}


\section{Relation between our constructions and others previously described}
\label{app-jd}

In this section we compare our constructions with
those of Jones \& Duponcheel \cite{jones-composing},
and also with the distributive law for monads of Manes \cite{manes}.
and Barr \& Wells \cite[\S 9.2]{bwttt}.

Throughout this section we 
assume at least that $M$ and $N$ are premonads,
and that we have functions \unitNM\ and \mapNM\ for which
(\ref{UC}) and (\ref{MC}) hold.
We note that when $N$ and $M$ are premonads, 
then (\ref{UC}) and (\ref{MC}) give that $NM$ is a premonad
\cite[\S 3]{jones-composing}.

\subsection{Relation between the \textit{pext} construction and 
  the \textit{prod} construction of Jones \& Duponcheel} \label{app-pp}

In this subsection we further assume that $M$ is a monad.  
Under these assumptions 
Jones \& Duponcheel \cite[\S 3.2,\S 4.1]{jones-composing} 
show that the compound monads $NM$ which can be
defined using \prd\ and the four rules P(1) to P(4)
are precisely those satisfying (\ref{J1}).
%
\begin{align*} 
\prd \oo \mapN\ (\mapNM\ f) & = \mapNM\ f \oo \prd\ 
  \tag*{P(1)}  \\[-0.5ex]
\prd \oo \unitN\ & = id \tag*{P(2)}  \\[-0.5ex]
\prd \oo \mapN\ \unitNM\ & = \unitM \tag*{P(3)}  \\[-0.5ex]
\prd \oo \mapN\ \joinNM\ & = \joinNM \oo \prd \tag*{P(4)} 
\end{align*}

We relate \prd\ to \pext, and list other relevant equalities,
with an easy lemma relating them.
%
\setcounter{equation}{0}
\renewcommand\theequation{PP\arabic{equation}}
\begin{align}
\prd & = \pext\ \id \label{prdpext} \\[-0.5ex]
\pext\ f & = \prd \oo \mapN\ f \label{pextpm} \\[-0.5ex]
\pext\ (g \oo f) & = \pext\ g \oo \mapN\ f \tag{\ref{pexto}} \\
\pext\ f \oo \unitN & = f \tag{\ref{pextru'}}
\end{align}

\begin{lemma} \label{lem-pp}
\begin{enumerate}
\item \label{ppo}
  (\ref{pextpm}) holds iff (\ref{prdpext}) and (\ref{pexto}) hold.
\item (\ref{pextru'}) holds iff (\ref{pextru}) holds.
\item assuming (\ref{pextpm}), P(2) holds iff (\ref{pextru'}) holds.
\item assuming (\ref{pextpm}), P(3) is just (\ref{pextlu}).
\end{enumerate}
\end{lemma}

\begin{theorem} \label{thm-prod}
Assume that $NM$ is a compound monad, for which (\ref{J1}) holds.
Use (\ref{PE}) to define \pext, and (\ref{prdpext}) to define \prd.
Then (\ref{J1S}) holds, and (\ref{pextpm}), (\ref{pexto}) and
P(1) to P(4) hold.
\comment{
\begin{quote}
\begin{tabular}{l@{\qquad}r@{\ \ }c@{\ \ }l}
\textbf{(\Jos)} & \ext\M\ (\ext\NM\ f) & = & \ext\NM\ f \oo \join\M \\
\textbf{(\pext)} & \multicolumn{3}{l}
  {(\ref{pextru}) to (\ref{pextfun}) %the rules of Table~\ref{tab-prules} 
  and the results of Theorem~\ref{thm-pext-k} hold} \\
\textbf{(\pextru-N)} & \pext\ f \oo \unitN & = & f \\
\textbf{(\pexto)} & \pext\ (g \oo f) & = & \pext\ g \oo \map\N\ f \\
\textbf{(\pextpm)} & \pext\ f & = & \prd \oo \map\N\ f \\
\textbf{(\P14)} & \pext\ (\ext\NM\ g) & = & \ext\NM\ g \oo \prd
\end{tabular}
\end{quote}
}
\end{theorem} 

\begin{proof}
% \begin{description}
% \mditem[(\ref{J1S}):] 
By Lemma~\ref{lem-J1}\ref{lem-J1-S}, (\ref{J1S}) holds. 
%
We now have that Theorems \ref{thm-when-pext} and \ref{thm-pext-k} hold, and
% Using (\ref{PE}), the following gives (\ref{pexto}),
Lemma~\ref{lem-pko} gives (\ref{pexto}), from which (\ref{pextpm}) follows.
\comment{
\begin{align*}
\extNM\ (g \oo f) \oo \unitM 
  & = \extNM\ g \oo \mapNM\ f \oo \unitM \tag{\ref{exto}NM} \\[-0.5ex]
  & = \extNM\ g \oo \unitM \oo \mapN\ f \tag{\ref{MC}, \ref{MJ3}M} 
\end{align*}
}%
To prove P(1) and P(4), we use the following result.
\begin{align*}
\pext\ (\extNM\ g) & = \pext\ (g \oNM \id) \tag{\ref{extom}NM} \\[-0.5ex]
  & = g \oNM \pext\ \id \tag{\ref{extfun}K, \ref{omext}K} \\[-0.5ex]
  & = \extNM\ g \oo \prd \tag{\ref{omext}NM, \ref{prdpext}} 
\end{align*}
%
From this we use (\ref{pextpm}), and (\ref{mapext}NM) and (\ref{joinext}NM)
respectively, to get P(1) and P(4).
% Using (\ref{pextpm}), P(3) is (\ref{pextlu}),
% and using (\ref{prdpext}), P(2) is a case of (\ref{pextru'}).
% By (\ref{prdpext}), P(2) is a special case of (\ref{pextru'}), and 
% by (\ref{pextpm}), P(3) is (\ref{pextlu}).
Finally, Lemma~\ref{lem-pp} gives P(2) and P(3). \qed
\end{proof}

We note that our definition of \prd\ gives
$\prd\ = \pext\ \id\ = \extNM\ \id \oo \unitM\ = \joinNM \oo \unitM$
which is the definition used in \cite[\S4.1]{jones-composing}.
% This shows that the \prd\ and \pext\ constructions 
% give the same compound monad.

The following converse theorem is \cite[\S3.2]{jones-composing}.

\begin{theorem}
Let function \prd\ be given, and
define \joinNM\ by $\joinNM = \extM\ \prd$.
Let P(1) to P(4) be satisfied.
Then $NM$ is a monad, satisfying (\ref{J1}).
\end{theorem}

\begin{proof}
Define \pext\ using (\ref{pextpm}).
Then Lemma~\ref{lem-pp} gives (\ref{pexto}),
(\ref{pextru}) and (\ref{pextlu}).

To define \extNM,  
we first show the equivalence of two likely definitions.
\begin{align*}
\joinNM \oo \mapNM\ f &= \extM\ \prd \oo \mapM\ (\mapN\ f)
  \tag{\ref{MC}} \\[-0.5ex] 
  &= \extM\ (\prd \oo \mapN\ f) = \extM\ (\pext\ f)
  \tag{\ref{exto}M, \ref{pextpm}} 
\end{align*}
So we define \extNM\ so that (\ref{MJ8}NM) and (\ref{EC}) hold,
and define \oNM\ using (\ref{omext}NM), from which (\ref{extom}NM) follows.
% Now if we define $\extNM\ f = \joinNM \oo \mapNM\ f$ 
%
\begin{align*}
\mbox{(\ref{pextfun}):} \qquad
\pext\ & (g \oNM f) = \pext\ (\extNM\ g \oo f) \tag{\ref{omext}NM} \\[-0.5ex]
  & = \prd \oo \mapN\ (\joinNM \oo \mapNM\ g \oo f)
    \tag{\ref{pextpm}, \ref{MJ8}NM} \\[-0.5ex]
  & = \joinNM \oo \prd \oo \mapN\ (\mapNM\ g \oo f)
    \tag{\ref{MJ2}N, P(4)} \\[-0.5ex]
  & = \joinNM \oo \mapNM\ g \oo \prd \oo \mapN\ f
    \tag{\ref{MJ2}N, P(1)} \\[-0.5ex]
  & = \extNM\ g \oo \pext\ f \tag{\ref{MJ8}NM, \ref{pextpm}} \\[-0.5ex]
  & = \extM\ (\pext\ g) \oo \pext\ f = \pext\ g \oM \pext\ f
    \tag{\ref{EC}, \ref{omext}M} 
\end{align*}

\comment{ 
(\ref{pextfun}): Then, using (\ref{MJ8}NM), from P(1) and P(4) we easily get
$\prd \oo \mapN\ (\extNM\ f) = \extNM\ f \oo \prd$.
Using (\ref{pexto}) then gives 
$\pext\ (\extNM\ f \oo g) = \extNM\ f \oo \pext\ g$.
Then (\ref{PE}), (\ref{omext}NM) and (\ref{omext}M) give (\ref{pextfun}).
}

Thus Theorem~\ref{thm-pext-k} applies and so 
\extNM, \oNM\ and \unitNM\ are functions of a monad $NM$.
To show that \joinNM\ and \mapNM\ are the \join\ and \map\ functions of this
monad, we need (\ref{joinext}) and (\ref{mapext}) for $NM$.

Since (\ref{joinext}NM) is clear from (\ref{MJ8}NM),
it remains to show (\ref{mapext}NM).
\begin{align*}
\extNM\ (\unitNM \oo f) & = \extM\ (\pext\ \unitNM \oo \mapN\ f) 
    \tag{\ref{EC}, \ref{pexto}} \\[-0.5ex] 
  & = \extM\ (\unitM \oo \mapN\ f)  \tag{\ref{pextlu}} \\[-0.5ex] 
  & = \mapM\ (\mapN\ f) = \mapNM\ f \tag{\ref{mapext}M, \ref{MC}} 
\end{align*}

% Since we have shown (\ref{extru}) to (\ref{mapext}) for $NM$, $NM$ is a monad.
Finally, (\ref{J1}), and also (\ref{J1S}), follow from
Theorem~\ref{thm-ext-join-iff} for $M$, \ref{ej3} $\Rightarrow$ \ref{ej1}. 
\qed 
\end{proof}

\subsection{Relation between the \textit{dmap} construction and 
  the \textit{dorp} construction of Jones \& Duponcheel} \label{app-dd}

In this subsection, as well as assuming that
$M$ and $N$ are premonads and that (\ref{UC}) and (\ref{MC}) hold,
we further assume that $M$ is a monad.  
Under these assumptions 
Jones \& Duponcheel \cite[\S 3.3,\S 4.2]{jones-composing} 
show that the compound monads $NM$ which can be
defined using \dorp\ and the four rules D(1) to D(4)
are precisely those satisfying (\ref{J2}).
We relate \dorp\ to \dmap\ as shown.
%
\begin{align} 
\dorp \oo \mapNM\ (\mapM\ f) & = \mapNM\ f \oo \dorp\ \tag*{D(1)} \\[-0.5ex]
\dorp \oo \unitNM & = \mapM\ \unitN \tag*{D(2)} \\[-0.5ex]
\dorp \oo \mapNM\ \unitM & = \id \tag*{D(3)} \\[-0.5ex]
\dorp \oo \joinNM & = \joinNM \oo \mapNM\ \dorp\ \tag*{D(4)} \\[1ex]
\dorp & = \dmap\ \id \tag{DD1} \label{DD1} \\[-0.5ex]
\dmap\ f & = \dorp \oo \mapNM\ f \tag{DD2} \label{DD2} 
\end{align}
%
Note that, analogously to Lemma~\ref{lem-pp}(\ref{ppo}), 
(\ref{DD2}) holds iff (\ref{DD1}) and (\ref{G2}) hold.

\begin{theorem}
Assume that $NM$ is a compound monad for which (\ref{J2'}) holds.
Define \djoin\ by (\ref{G9}) or (\ref{DJ}),
and \dmap\ and \dunit\ by (\ref{G10}) and (\ref{DU}).
Then (\ref{DJ}) and (\ref{G1}) to (\ref{G12}) hold.
Further, if \dorp\ is defined by (\ref{DD1}), then 
(\ref{DD2}) and D(1) to D(4) hold.
\end{theorem}

\begin{proof}
(\ref{G11}) holds, using (\ref{MJ3}M).
The equivalence of (\ref{DJ}), that is,
$\djoin\ = \mapM\ \joinN$,
and (\ref{G9}) follows from Lemma~\ref{lem-J2}.
Then $\djoin \oo \dunit\ = \mapM\ \joinN \oo \mapM\ \unitN\ = \id$,
by (\ref{MJ2}M), (\ref{MJ5}N) and (\ref{MJ1}M),
that is, (\ref{G5}) holds.
  % \mapM\ (\joinN \oo \unitN) = \mapM\ \id\ = \id$
Thus the conditions of Theorem~\ref{thm-Grev} are satisfied,
so (\ref{G1}) to (\ref{G8}) also hold, 
as does, by Theorem~\ref{thm-G}, (\ref{G12}).

Now, using (\ref{DD1}), we get (\ref{DD2}) from (\ref{G2}).
Then D(3) is just (\ref{G1}), and D(4) follows from (\ref{G4}),
by (\ref{G8}) and (\ref{extjm}NM).
Using (\ref{DU}), (\ref{G3}) gives D(2).

We prove D(1) by
\begin{align*}
\dorp \oo \mapNM\ (\mapM\ f) & = \dmap\ (\mapM\ f) \tag{\ref{DD2}} \\[-0.5ex]
  & = \extNM\ (\dunit \oo \mapM\ f) \tag{\ref{G10}} \\[-0.5ex]
  & = \extNM\ (\mapNM\ f \oo \dunit) 
    \tag{\ref{MC}, \ref{MJ2}M, \ref{MJ3}N, \ref{DU}} \\[-0.5ex]
  & = \mapNM\ f \oo \extNM\ \dunit 
    \tag{\ref{mapext}NM, \ref{extass}NM} \\[-0.5ex]
  & = \mapNM\ f \oo \dorp \tag*{(\ref{G10}, \ref{DD1}) $\square$}
\end{align*}
\end{proof}

Note that our definition of \dorp\ gives
$\dorp\ = \dmap\ \id\ = \extNM\ \dunit$, which corresponds to 
the definition used in \cite[\S 4.2]{jones-composing}.

Jones \& Duponcheel \cite[\S 3.3]{jones-composing} 
also show how to define a compound monad from a function \dorp,
satifying four rules D(1) to D(4),
assuming that $M$ is a premonad and $N$ is a monad.
They use (\ref{UC}) and (\ref{MC}) as definitions, 
and defining \joinNM\ by
\begin{equation*}
\joinNM = \mapM\ \joinN \oo \dorp \tag{JD} \label{JD}
\end{equation*}
They show that in such a compound monad, (\ref{J2}) holds.
We can prove this theorem via rules (\ref{G1}) to (\ref{G8}) and 
Theorem~\ref{thm-G}.
However in doing so, we have to prove (\ref{MJ4}NM) on the way to 
proving (\ref{G4}) which is rather unsatisfying.

\begin{theorem} \cite[\S 3.3]{jones-composing} 
Let $N$ be a monad and $M$ a premonad. 
Define \unitNM\ and \mapNM\ by (\ref{UC}) and (\ref{MC}).
Define \djoin\ and \dunit\ by (\ref{DJ}) and (\ref{DU}).
Let the function \dorp\ satisfy D(1) to D(4),
and define \dmap\ by (\ref{DD2}).
Define \joinNM\ by (\ref{JD}).
Then $NM$ is a monad satisfying (\ref{G1}) to (\ref{G12}) and (\ref{J2}).
\end{theorem}

\begin{proof} (sketched: also proved in Isabelle).  
Firstly, note that $NM$ is a premonad.
From that fact, using (\ref{DD2}), we can get 
(\ref{DD1}) from (\ref{MJ1}NM),
(\ref{G2}) from (\ref{MJ2}NM),
(\ref{G3}) from (\ref{MJ3}NM) and D(2),
while (\ref{G1}) is just D(3).

(\ref{G5}): Use (\ref{DJ}), (\ref{DU}),
(\ref{MJ2}M), (\ref{MJ5}N) and (\ref{MJ1}M).

(\ref{G6}): Use
(\ref{DJ}), (\ref{UC}), (\ref{G2}), (\ref{G1}), (\ref{MC}),
(\ref{MJ2}M), (\ref{MJ6}N) and (\ref{MJ1}M).

We use (\ref{G8}) as a definition,
noting also that (\ref{MJ8}NM) holds, as
\begin{align*}
\joinNM \oo \mapNM\ f & = \mapM\ \joinN \oo \dorp \oo \mapNM\ f
    \tag{{JD}} \\[-0.5ex]
  & = \djoin \oo \dmap\ f
    \tag{\ref{DJ}, \ref{DD2}} 
\end{align*}

From (\ref{G8}) and (\ref{G1}) we get (\ref{G9}). 

\comment{
(\ref{G7}):
\begin{align}
\djoin \oo \dmap\ \djoin &= \mapM\ \joinN \oo \dmap\ (\mapM\ \joinN) 
    \tag{\ref{DJ}} \\[-0.5ex]
  &= \mapM\ \joinN \oo \mapNM\ \joinN \oo \dorp 
    \tag{\ref{DD2},D1} \\[-0.5ex]
  &= \mapM\ (\joinN \oo \joinN) \oo \dorp 
    \tag{\ref{MC}, \ref{MJ2}M, \ref{MJ7}N} \\[-0.5ex]
  &= \djoin \oo \joinNM\ 
    \tag{\ref{MJ2}M,{JD}} 
\end{align}
TO COMPLETE ie DO G4 
}

To prove (\ref{G4}) and (\ref{G7}) we derive initially
\begin{align*}
\djoin \oo \dmap\ \mapM\ g &= \mapM\ \joinN \oo \mapNM\ g \oo \dorp
    \tag{\ref{DJ}, \ref{DD2}, D(1)} \\[-0.5ex]
  &= \mapM\ (\joinN \oo \mapN\ g) \oo \dorp
    \tag{\ref{MC}, \ref{MJ2}M} \\[-0.5ex]
  &= \mapM\ (\extN\ g) \oo \dorp
    \tag{\ref{MJ8}N} 
\end{align*}

Then, to get (\ref{G7}), we set $g = \joinN$ in this to get,
on the right-hand side,
\begin{align*}
\mapM\ & (\extN\ \joinN) \oo \dorp = \mapM\ (\joinN \oo \joinN) \oo \dorp
    \tag{\ref{MJ7}N, \ref{MJ8}N} \\[-0.5ex]
  &= \djoin \oo \mapM\ \joinN \oo \dorp = \djoin \oo \joinNM\
    \tag{\ref{MJ2}M, \ref{DJ}, {JD}} 
\end{align*}
%
and we set $g = \mapN\ f$ in it to get, by a very similar argument, 
using (\ref{MJ4}N) instead of (\ref{MJ7}N),
$\djoin \oo \dmap\ \mapNM\ f = \mapNM\ f \oo \joinNM$.
Rewriting using (\ref{G8}) and (\ref{MJ8}NM), we have (\ref{MJ4}NM).
Thus the property of $h$ that 
$\joinNM \oo \mapNM\ h = h \oo \joinNM$
holds for $h = \dorp$, by D(4), and for $h = \mapNM\ f$, above.
So it is easy to see that this property holds for their composition,
$h = \dorp \oo \mapNM\ f$, which, again using (\ref{G8}) and (\ref{MJ8}NM),
gives us (\ref{G4}).

Thus Theorem~\ref{thm-G} applies.
As we now have both (\ref{G9}) and (\ref{DJ}), Lemma~\ref{lem-J2}
shows that (\ref{J2}) holds.
\qed
\end{proof}

\subsection{Relation between the \textit{kmap} construction and 
  the \textit{swap} construction of Jones \& Duponcheel} \label{app-ks}

Throughout this section we make the assumptions of \S \ref{app-pp}
and of \S \ref{app-dd}.
That is, we assume that $M$ and $N$ are monads, 
and that (\ref{UC}) and (\ref{MC}) hold.
Under these assumptions 
Jones \& Duponcheel \cite[\S 3.4,\S 4.3]{jones-composing} 
show that the compound monads $NM$ which can be
defined using \swap\ and the four rules S(1) to S(4)
(where \prd\ and \dorp\ are defined in terms of \swap\ as shown)
are precisely those satisfying (\ref{J1}) and (\ref{J2}).
%
\begin{align*} 
\swap \oo \mapN\ (\mapM\ f) & = \mapNM\ f \oo \swap\ \tag*{S(1)} \\[-0.5ex]
\swap \oo \unitN & = \mapM\ \unitN \tag*{S(2)} \\[-0.5ex]
\swap \oo \mapN\ \unitM & = \unitM \tag*{S(3)} \\[-0.5ex]
\prd \oo \mapN\ \dorp & = \dorp \oo \prd \tag*{S(4)} 
\end{align*}%
%
\begin{align*}
\prd & = \mapM\ \joinN \oo \swap &
\dorp & = \extM\ \swap
\end{align*}%
%
\setcounter{equation}{0}%
\renewcommand\theequation{KS\arabic{equation}}%
\begin{align} 
\label{SK} \swap & = \kmap\ \id \\[-0.5ex]
\label{kmapsm} \kmap\ f & = \swap \oo \mapN\ f \\[-0.5ex]
\tag{\ref{kmapo}} \kmap\ (g \oo f) & = \kmap\ g \oo \mapN\ f 
\end{align} 

Note that, analogously to Lemma~\ref{lem-pp}(\ref{ppo}), 
(\ref{kmapsm}) holds iff (\ref{SK}) and (\ref{kmapo}) hold.
%
\begin{theorem} \label{thm-swap}
With the assumptions and definitions of Theorem~\ref{thm-both},
further define \swap\ from \kmap\ by (\ref{SK}).
Then S(1) to S(4) hold.
\comment{
Then (\ref{kmapo}), (\ref{kmapsm}), and xx hold.
\begin{quote}
\begin{tabular}{l@{\qquad}r@{\ \ }c@{\ \ }l}
\textbf{(\kmapo)} & \kmap\ (g \oo f) & = & \kmap\ g \oo \mapN\ f \\
\textbf{(\kmapsm)} & \kmap\ f & = & \swap \oo \mapN\ f \\
\textbf{(\Jts)} & \extNM\ \unitM & = & \mapM\ \joinN \\
\textbf{(\kjoinuj)} & \kjoin & = & \unitM \oo \joinN \\
\textbf{(\extkmap)} & \extNM\ f & = & \extM\ (\mapM\ \joinN \oo \kmap\ f) \\
\textbf{(xx)} & \kmap\ f & = & \pext\ (\mapM\ \unitN \oo f) 
\end{tabular}
\end{quote}
}
\end{theorem} 

\begin{proof}
By Lemma~\ref{lem-J1}\ref{lem-J1-S}, Theorem~\ref{thm-when-pext} applies.
So by Lemma~\ref{lem-pko}, (\ref{kmapo}) and so (\ref{kmapsm}) hold.
So S(3) is just (\ref{KMJ1}).
Now by (\ref{mapext}K), (\ref{omext}M) and (\ref{DUK}),
$\kmap\ f = \pext\ (\unitNM \oM f) = \pext\ (\dunit \oo f)$,
so $\swap\ = \pext\ \dunit$ and, by (\ref{pextru'}),
$\swap \oo \unitN\ = \dunit$ and S(2) follows.

We show S(1), after simplifying it using (\ref{kmapsm}), as follows:
%
\begin{align*}
% \text{for S(1):} \quad
\kmap\ (\mapM\ f) &= \kmap\ ((\unitM \oo f) \oM id) 
    \tag{\ref{mapext}M, \ref{extom}M} \\[-0.5ex] 
  &= \kmap\ (\unitM \oo f) \oM \kmap\ \id \tag{\ref{KMJ2}} \\[-0.5ex] 
  &= (\kmap\ \unitM \oo \mapN\ f) \oM \swap\ 
    \tag{\ref{kmapo}, \ref{SK}} \\[-0.5ex] 
  &= \extM\ (\unitM \oo \mapN\ f) \oo \swap\ 
    \tag{\ref{MJ1}K, \ref{omext}M} \\[-0.5ex] 
  % &= \mapM\ (\mapN\ f) \oo \swap\ 
    % \tag{\ref{MJ1}K, \ref{omext}M, \ref{mapext}M} \\[-0.5ex] 
  &= \mapNM\ f \oo \swap \tag{\ref{mapext}M, \ref{MC}} 
\end{align*}
% S(1) follows from this by (\ref{kmapsm}).
%
Now, for S(4) we first use our definitions of \dorp\ and \prd.
By \eqref{DD1} and \eqref{DMK}, $\dorp\ = \extM\ (\kmap\ \id)$,
and by (\ref{mapext}K) let $\kmap\ \id$ be $\pext\ g$, so we have
% show $\pext\ \dorp = \dorp \oo \prd$ by
%
\begin{align*}
\prd \oo \mapM\ \dorp & = \pext\ (\extM\ (\kmap\ \id)) 
    \tag{\ref{pextpm}} \\[-0.5ex] 
  & = \pext\ (\pext\ g \oM \id) \tag{\ref{extom}M} \\[-0.5ex] 
  & = \pext\ g \oM \pext\ \id \tag{\ref{extass}K} \\[-0.5ex] 
  % & = \kmap\ \id \oM \prd = \extM\ (\kmap\ \id) \oo \prd
  & = \extM\ (\kmap\ \id) \oo \prd
    \tag{\ref{prdpext}, \ref{omext}M} 
\end{align*}

Finally, to show S(4) precisely as it is stated,
we need to check that the various definitions of \prd\ and \dorp\
are consistent.
By our definitions, 
\begin{align*}
\prd & = \pext\ \id\ = \kjoin \oM \kmap\ \id 
    \tag{\ref{prdpext}, \ref{MJ8}K} \\[-0.5ex] 
  & = \extM\ \kjoin \oo \swap = \mapM\ \joinN \oo \swap
    \tag{\ref{omext}M, \ref{SK}, \ref{DJK}, \ref{DJ}} \\[1ex]
\dorp & = \dmap\ \id\ = \extM\ (\kmap\ \id) = \extM\ \swap
    \tag{\ref{DD1}, \ref{DMK}, \ref{SK}} 
\end{align*}
so our definitions are consistent with those used above in stating S(4).
\qed
\comment{
\begin{description}
\mditem[(\kmapo)] By (\pexto) and (\omoass),
\textit{
\pext\ (\unitNM \oM (g \oo f)) = 
\pext\ (\unitNM \oM g) \oo \mapN\ f}.
That is, 
\textit{ \kmap\ (g \oo f) = \kmap\ g \oo \mapN\ f}.

\mditem[(\kmapsm)] By (\swapkmap), 
this is the special case $g = \id$ of (\kmapo).

\item[(\Jts)] 
By Theorem~\ref{thm-ext-join-iff}, \ref{ej1} $\Rightarrow$ \ref{ej2}, 
we need
\textit{\mapM\ \joinN \oo \unitNM\ = \unitM}: using (\ref{UC})
this is 

\textit{
\begin{tabular}{rcl@{\qquad}r}
\mapM\ \joinN \oo \unitM \oo \unitN & = & 
\unitM \oo \joinN \oo \unitN & (\textup{MJ3 for} M) \\
& = & \unitM & (\textup{MJ5 for} N) 
\end{tabular} }

\item[(\kjoinuj)] ~

\textit{
\begin{tabular}{rcl@{\qquad}r}
\kjoin &=& \pext\ \unitM\ = \extNM\ \unitM \oo \unitM & (\pextext) \\
  &=& \mapM\ \joinN \oo \unitM\ = \unitM \oo \joinN & (\Jts, 
  \textup{MJ3 for} M)
\end{tabular} }

\item[(\extkmap)] ~

\textit{
\begin{tabular}{rcl@{\qquad}r}
\extNM\ f &=& \extM\ (\pext\ f) = \extM\ (\kjoin \oM \kmap\ f) &
  (\extcomp, pext-kjm)\\
  &=& \extM\ (\mapM\ \joinN \oo \kmap\ f) & (\omext, \mapext)
\end{tabular} }


\end{description}
}
\end{proof}

We showed in the proof above that $\swap\ = \pext\ \dunit$ 
which is consistent with the definition of \swap\ used in 
\cite[\S4.3]{jones-composing}.

\comment{
We can set $f = id$ in (\extkmap) 
to get \textit{\joinNM\ = ext\M\ (\mapM\ \joinN \oo \swap)},
and also in (\kmappext), using (\ref{UC}), (\omext) and (\mapext), to get
\textit{\swap\ = \pext\ (\mapM\ \unitN)},
which are used/proved in \cite[\S3.4,\S4.3]{jones-composing}.
This shows that the \swap\ and \kmap\ constructions give the same compound
monad.

It is also straightforward to prove the results S(2) to S(4) of
\cite[\S3.4]{jones-composing}, and S(1) follows from (S1e) above.
Using \textit{\swap\ = \pext\ (\mapM\ \unitN)} (above), 
S(2) is just (\pextru-N), and by (\kmapsm), S(3) is (\ref{KMJ1}).
Tracing definitions of the function \dorp\ used in S(4) shows that 
S(4) is a special case of (\P14) above.
}

Conversely, from S(1) to S(4), (\ref{kmapsm}) and (\ref{KJ})
it is possible to prove the rules of (\ref{KMJ1}) to (\ref{KMJ7}) directly.
These proofs have been done in Isabelle, see \cite{prfs}, 
functor \verb|fromSwap|.
Alternatively, see Jones \& Duponcheel \cite[\S 3.4]{jones-composing} 
for proofs from S(1) to S(4) that $NM$ is a monad. 

Another interesting result is that both sides of S(4) equal 
$\swap \oNM \swap$. The key step to prove it is to modify the proof of S(4)
above, to give 
%
\begin{align*}
\prd \oo \mapM\ \dorp 
  & = \pext\ (\pext\ g \oM \id) \tag{as above} \\[-0.5ex] 
  & = \pext\ (\pext\ g) \oM \kmap\ \id \tag{\ref{exto}K} \\[-0.5ex] 
  & = \pext\ \swap \oM \swap = \swap \oNM \swap 
    \tag{\ref{SK}, \ref{omext}K} 
\end{align*}

\subsection{A distributive law for monads} \label{app-dl}
Manes \cite{manes} describes a ``distributive law'' for monads,
at Chapter~4, pages 311-2, Definition~3.6, and 
page~334, Exercise~6.
This is also described by Barr \& Wells in \cite{bwttt}, \S 9.2,
where rules (D1) to (D4) are given.
His natural transformation $\lambda$ is also the polymorphic function \swap. 
Translating these rules into our terminology, and calling (D1) to (D4)
(\ref{BWD1}) to (\ref{BWD4}), we have
%
\setcounter{equation}{0}
\renewcommand\theequation{DL\arabic{equation}}
\begin{align*}
\swap \oo \mapN\ \unitM & = \unitM \label{BWD1} \tag{BWD1} \\[-0.5ex]
\swap \oo \unitN & = \mapM\ \unitN \label{BWD2} \tag{BWD2} \\[-0.5ex]
\swap \oo \mapN\ \joinM & = \joinM \oo \mapM\ \swap \oo \swap 
  \label{BWD3} \tag{BWD3} \\[-0.5ex]
\swap \oo \joinN & = \mapM\ \joinN \oo \swap \oo \mapN\ \swap 
  \label{BWD4} \tag{BWD4} 
\end{align*}

Of these, (\ref{BWD2}) and (\ref{BWD4}) are the diagrams in 
\cite[Definition~3.16]{manes}, 
and (\ref{BWD1}) and (\ref{BWD3}) are the diagrams in 
Exercise~6 on page~334 of \cite{manes}. 
He additionally specifies that \swap\ is a natural transformation.

\begin{theorem} \label{thm-dl}
With the assumptions and definitions of Theorem~\ref{thm-swap},
(\ref{BWD1}) to (\ref{BWD4}) hold and \swap\ is a natural transformation.
\end{theorem} 

\begin{proof}
From Theorem~\ref{thm-swap} we have S(1) to S(4).
That \swap\ is a natural transformation is just S(1),
and (\ref{BWD2}) and (\ref{BWD1}) are just S(2) and S(3).
We can translate (\ref{BWD3}) to
$\kmap\ (\id \oM \id) = \kmap\ \id \oM \kmap\ \id$,
an instance of (\ref{MJ2}K).
To prove (\ref{BWD4}),
we have, by Theorem~\ref{thm-ext-join-iff} for \KM,
\ref{ej3} $\Rightarrow$ \ref{ej1}, and (\ref{mapext}K), 
\begin{align*}
\pext\ (\kmap\ \id) & = \kmap\ \id \oM \kjoin 
     \\[-0.5ex]
  & = \kmap\ \id \oM \unitM \oo \joinN 
    \tag{\ref{KJ}, \ref{omoass}M} \\[-0.5ex]
  & = \swap \oo \joinN \tag{\ref{SK}, \ref{krid}M} 
\end{align*}
Now $\pext\ (\kmap\ \id) = \prd \oo \mapN\ \swap$
which is, by the expression for \prd\ in \S \ref{app-ks} above,
equal to the right-hand side of (\ref{BWD4}).
\qed
\end{proof}

Conversely, from S(1) and (\ref{BWD1}) to (\ref{BWD4}), 
(\ref{kmapsm}) and (\ref{KJ})
it is possible to prove the rules of (\ref{KMJ1}) to (\ref{KMJ7}),
and the resulting compound monad satisfies (\ref{J1}) and (\ref{J2}) .
These proofs have been done in Isabelle, see \cite{prfs},
functors \verb|fromSextDL| and \verb|fromSextF|.

% \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

\section{Some examples using rules (\ref{krid}) to (\ref{omoIass})}
\label{app-ex}

In this section we give some examples of monads which are easily 
shown to be monads using rules (\ref{krid}) to (\ref{omoIass}).

The two examples in \S \ref{ex-comp-st} and \S \ref{ex-comp-rdr}
are (in different senses) compound monads.
In both cases $M$ is an arbitrary monad; 
we don't explicitly use the monad $N$,
but proceed directly to define the compound monad $N_M$.
The simple monad $N$ will be a special case of $N_M$,
which could be obtained by setting $M$ to be the identity monad 
(in which \unit, \ext, \map\ and \join\ are all the identity function).

\subsection{Example: the Continuation Monad} \label{ex-cont}

The continuation monad (eg, \cite[\S 3.1]{wadler-essence}) is given by 
$\alpha K = (\alpha \to \Ans) \to \Ans$,
where \Ans\ is a fixed type,
so $\alpha \to \beta K = \alpha \to (\beta \to \Ans) \to \Ans$.
We use the function \C, %(``switch arguments'')
of type $(\gamma \to \delta \to \Ans) \to (\delta \to \gamma \to \Ans)$,
defined by \mbox{\textit{C f x y = f y x}}.
Note that \textit{C (C f) = f}, so \C\ is 1-1, and
$\C\ x = \C\ y \Rightarrow x = y$.
Then we define \oK\ by
\textit{C (g \oK\ f) = C f \oo\ C g},
and \unitK\ by \textit{C \unitK\ = id}.

The \om\ rules are then easily proved.
For each rule \lhs\ = \rhs, as \C\ is 1-1,
it suffices to prove \C(\lhs) = \C(\rhs).
\textit{
\begin{description}
\item[] \textnormal{for (\ref{krid}):}
C (f \oK\ unit\K) = C unit\K\ \oo\ C f = id \oo\ C f = C f 
\item[] \textnormal{for (\ref{klid}):}
C (unit\K\ \oK\ f) = C f \oo\ C unit\K\ = C f \oo\ id = C f 
\item[] \textnormal{for (\ref{kass}):}
C (h \oK\ (g \oK\ f)) = (C f \oo\ C g) \oo\ C h = \\
\mbox{} \hfill C f \oo\ (C g \oo\ C h) = C ((h \oK\ g) \oK\ f)  
\end{description}
}

It is simple but tedious to confirm (\ref{omoIass}) directly.
We now check that this definition corresponds to the usual ones.
Using (\ref{extom}), we get 
\begin{itemize}
\item[] \textit{\unitK\ a c = C id a c = id c a = c a}\ , and
\item[] \textit{\extK\ g k c = (g \oK\ id) k c = C (C id \oo\ C g) k c = \\
 \mbox{} \qquad \qquad
 (C id \oo\ C g) c k = C id (C g c) k = id k (C g c) = 
 k ($\lambda$f. g f c)}
\end{itemize}
Both of these agree with the definitions in \cite[\S 3.1]{wadler-essence}.

\subsection{Example: the Compound State Monad} \label{ex-comp-st}
Let $M$ be a monad.
Let \State\ be a fixed type, representing, for example, a program state.
Then the state monad is given by the type 
$\alpha S = \State \to \alpha * \State$
(where $\alpha * \beta$ denotes a pair type).
This represents a computation which takes a program state and returns
a result of interest and a new state.
The ``compound'' state monad is given by the type 
$\alpha S_M = \State \to (\alpha * \State) M$.
(Note that because $\alpha S_M$ is neither 
$\alpha S M$ nor $\alpha M S$,
\S \ref{sec-pext} and following are 
\emph{not} relevant to this example, which perhaps should
not be called a ``compound monad'').
If, for example, $M$ is the list monad,
$S_M$ could be used to represent a non-deterministic program,
which may behave in any of a number of possible ways,
each way returning a result and new state.

To show that this is a monad, we use the functions \curry\ and \unc\
% (short for \textit{uncurry})
\begin{align*} 
\curry\ g\ x\ y & = g\ (x,y) &
\unc\ f\ (x,y) & = f\ x\ y
\end{align*} 
noting that these are mutually inverse (so, in particular, \unc\ is 1-1).
Consider a function $f : \alpha \to \beta S_M$.
Then $\unc\ f$ is of type $\alpha * \State \to (\beta * \State)\ M$.
Given that $M$ is a monad,
it is easy to see how to compose functions of such a type -- 
we define \oSM\ and \unitSM\ by
\begin{align*} 
\unc\ (g \oSM f) & = \unc\ g \oM \unc\ f \\[-0.5ex]
\unc\ \unitSM & = \unitM
\end{align*} 

The \om\ rules are then easily proved.
For each rule \lhs\ = \rhs, as \unc\ is 1-1,
it suffices to prove \unc\ (\lhs) = \unc\ (\rhs).
The proofs use the corresponding rules for the monad $M$.
\begin{description}
\mditem[for (\ref{krid}) and (\ref{klid}):] \\
$\unc\ (f \oSM \unitSM) =
  \unc\ f \oM \unc\ \unitSM = \unc\ f \oM \unitM = \unc\ f$
$\unc\ (\unitSM \oSM f) = 
  \unc\ \unitSM \oM \unc\ f = \unitM \oM \unc\ f = \unc\ f$ \\
\mditem[for (\ref{kass}):]
$\unc\ (h \oSM (g \oSM f)) = \unc\ h \oM (\unc\ g \oM \unc\ f) = $ \\
\mbox{} \hfill
  $ (\unc\ h \oM \unc\ g) \oM \unc\ f = \unc\ ((h \oSM g) \oSM f)$  
\end{description}

It is simple but tedious to confirm (\ref{omoIass}) directly.
We need only check that this definition corresponds to the usual ones.
Using (\ref{extom}), % we get 
\begin{itemize}
\item[] \textit{\unitSM\ a s = curry \unitM\ a s = \unitM\ (a,s)}\ , and
\item[] \textit{\extSM\ k m s = (k \oSM\ id) m s = 
  curry (\unc\ k \oM\ \unc\ id) m s = \\
 \mbox{} \qquad \qquad
  (\extM\ (\unc\ k) \oo\ \unc\ id) (m,s) = \extM\ ($\lambda(a,t)$. k a t) (m s)}
\end{itemize}
Both of these agree with the definitions in \cite[\S 7.1]{lhj} 
(modified to switch the members of pairs).

\subsection{Example: the Compound Reader Monad} \label{ex-comp-rdr}
Again, let $M$ be a monad.
Let \Env\ be a fixed type.
Then the environment, or reader, monad
is given by the type $\Env \to \alpha$
(evaluating any monadic value also involves reading the environment).
The reader monad is given by the type 
$\alpha R = \Env \to \alpha$, and
the compound reader monad (\cite[\S 7.2]{lhj}, \cite[\S 6.3]{jones-composing})
is given by $\alpha R_M = \Env \to \alpha M = (\alpha M) R$.

To show that this is a monad, we define a function 
\textit{ \ape\ f a = f a e} (for $e : \Env$), of type
$(\gamma \to \Env \to \delta) \to (\gamma \to \delta)$.
In similar proofs earlier, we had a function which was 1-1;
here we need to use the property
$$(\forall e. \mbox{\ape}\ f = \mbox{\ape}\ g) \Rightarrow f = g$$

We define \oRM\ and \unitRM\ by
\begin{center} \textit{
\begin{tabular}{rcl}
(g \oRM\ f) a e & = & (\ape\ g \oM\ \ape\ f) a \\
\unitRM\ a e & = & \unitM\ a
\end{tabular}
} \end{center} 
that is, 
\begin{center} \textit{
\begin{tabular}{rcl}
\ape\ (g \oRM\ f) & = & \ape\ g \oM\ \ape\ f \\
\ape\ \unitRM & = & \unitM
\end{tabular}
} \end{center} 

The \om\ rules are then easily proved.
For each rule \lhs\ = \rhs, it suffices to let $e$ be arbitrary,
and then to prove \textit{\ape}(\lhs) = \textit{\ape}(\rhs).
The proofs use the corresponding rules for the monad $M$.
\textit{
\begin{description}
\item[] \textnormal{for (\ref{krid}) and (\ref{klid}):} \\
\ape\ (f \oRM\ \unitRM) =
\ape\ f \oM\ \ape\ \unitRM\ = \ape\ f \oM\ \unitM\ = \ape\ f \\
\ape\ (\unitRM\ \oRM\ f) = 
\ape\ \unitRM\ \oM\ \ape\ f = \unitM\ \oM\ \ape\ f = \ape\ f \\
\item[] \textnormal{for (\ref{kass}):}
\ape\ (h \oRM\ (g \oRM\ f)) = \ape\ h \oM\ (\ape\ g \oM\ \ape\ f) = \\
\mbox{} \hfill 
  (\ape\ h \oM\ \ape\ g) \oM\ \ape\ f = \ape\ ((h \oRM\ g) \oRM\ f)  
\end{description}
}

It is straightforward to confirm (\ref{omoIass}) directly.
We need only check that this definition corresponds to the usual ones.
Using (\ref{extom}), % we get 
\begin{itemize}
\item[] \textit{\unitRM\ a e = \unitM\ a}\ , and
\item[] \textit{\extRM\ k m e = (k \oRM\ id) m e = 
  (\ape\ k \oM\ \ape\ id) m = \\
 \mbox{} \qquad \qquad
  (\extM\ (\ape\ k) \oo\ \ape\ id) m = \extM\ ($\lambda a$. k a e) (m e)}
\end{itemize}
Both of these agree with the definitions in \cite[\S 7.2]{lhj}.

\section{Examples of the Compound Monad Constructions}

\subsection{Example: the Compound Exception Monad}
The exception (or error) monad is given by 
\begin{center}
\texttt{ datatype $\alpha$ E = Ok of $\alpha$ | Err of string }
\end{center}
with \textit{unit\E\ a = Ok a}.
% and \ext\ defined similarly to \pext\ below.

With $M$ an arbitrary monad we define the compound monad $\alpha E M$ by

\begin{center} \textit{
\begin{tabular}{rcl@{\qquad\qquad}r}
pext f (Ok a) & = & f a & (\pextOk) \\ 
pext f (Err msg) & = & unit\M\ (Err msg) & (\pextErr)
\end{tabular} 
} \end{center}
(Letting $M$ be the identity monad gives us the definition of \ext\E,
for then \pext\ is \ext\E).
We also define \unit\EM\ and \oEM\ by
(\ref{UC}) and (\ref{ompext}).
Then we prove the \pext\ axioms (\ref{pextru}) to (\ref{pextfun}) as follows.
(\ref{pextru}) is just (\pextOk).
Using the definitions just mentioned, we get (\ref{pextlu}) from
\begin{center} \textit{
pext unit\EM\ (Ok a) = unit\EM\ a = unit\M\ (Ok a) \\
pext unit\EM\ (Err msg) = unit\M\ (Err msg)
} \end{center}
and using these definitions and also (\ref{omext}M) we get (\ref{pextfun}) from

\begin{center} \textit{
\begin{tabular}{rcl@{\qquad}r}
pext (g \oEM\ f) (Ok a) & = & (pext g \oM f) a & (\pextOk, \ref{ompext}) \\
  & = & ext\M\ (pext g) (f a) & (\ref{omext}M) \\
& = & ext\M\ (pext g) (pext f (Ok a)) & (\pextOk) \\
& = & (pext g \oM pext f) (Ok a) & (\ref{omext}M)
\end{tabular} 
} \end{center}

\begin{center} \textit{
\begin{tabular}{rcl@{\quad}r}
pext (g \oEM\ f) (Err msg) 
  & = & unit\M\ (Err msg) & (\pextErr) \\
  & = & pext g (Err msg) & (\pextErr) \\
& = & ext\M\ (pext g) (unit\M\ (Err msg)) & (\ref{extru}) \\
& = & ext\M\ (pext g) (pext f (Err msg)) & (\pextErr) \\
& = & (pext g \oM pext f) (Err msg) & (\ref{omext}M) 
\end{tabular} 
} \end{center}

\subsection{Other Examples; Isabelle Proofs}
\subsubsection{Example: the Compound Writer Monad}

Let \Monoid\ be a type representing a monoid, where we use
0 for the identity value and + for the associative binary operation.
Then let $\alpha W = (\Monoid * \alpha)$
and $\alpha W M = (\alpha W) M$.
A function $f : \alpha \to \beta W$ represents a function from $\alpha$ to
$\beta$ which also produces some output $m$ of type \Monoid; 
when \ext\W\ $f$ acts on \textit{(acc, a)}, where \acc\ represents output
already accumulated, the output $m$ is added to that in \acc.
That is, if $f\ a = (m,b)$, then 
\textit{\ext\W\ f (\acc,a) = (\acc\ $+$ m, b)}.
Naturally, $\unit_W\ a = (0,a)$. % \textit{unit\W\ a = (0,a)}.

The compound writer monad is given by 
\begin{center} \textit{
\pext\ f (\acc,a) = \map\M\ ($\lambda$(m,b). (\acc\ $+$ m, b)) (f a) 
} \end{center}

That is, the addition of the new output $m$ to the accumulated output
\acc\ is done ``under the hood'' of the monad $M$.
This makes the proof of the axioms for \pext\ more difficult,
and we omit them.  
(Jones \& Duponcheel \cite[\S 6.5.1]{jones-composing} also omit
proofs for this monad).

\subsubsection{Example: the Compound Reader Monad}

This was discussed in \S\ref{ex-comp-rdr}.
We write the monad type as $\alpha N R$, where $R$ takes the place of $M$ in 
our general results.
Note that, here, the monad $R$ is fixed, while $N$ is arbitrary.
The \pext\ construction applies to this compound monad,
but to use it, we need to show 
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item \label{rmon} that $R$ is a monad
\item \label{nmon} that $N$ is a monad
\item \label{pext} that the axioms for \pext,
  (\ref{pextru}) to (\ref{pextfun}), hold
\end{enumerate}
Our treatment of compound monads using the \pext\ axioms requires, as such,
only \ref{rmon} and \ref{pext}, but we need \ref{nmon} to prove \ref{pext}.
These proofs are, however, not difficult, and are omitted.

\subsubsection{Isabelle Proofs}

The proofs in this paper and the proofs for the compound reader and writer
monads were performed using the theorem prover Isabelle,
and are available at \cite{prfs}, or from the author's home page.

Jones \& Duponcheel, \cite[\S 6.4]{jones-composing},
discuss the compound list monad -- 
$\alpha$ \textit{list M} is a monad provided that
$M$ is a \emph{commutative} monad, and they give proofs of this.
We also have Isabelle proofs of the \pext\ axioms for the compound list monad.