
\newpage
% APPENDIX --- FOR REFEREES' USE; NOT FOR PUBLICATION

\appendix

\section{\HOLw\ definitions and theorems}

\subsection{Basic Definitions and Theorems about Categories} \label{a-cat}

\begin{verbatim}
(in src/bool/boolScript.sml)
val _ = type_abbrev ("C", Type `: \('f:'l => 'k => 'm) 'a 'b. 'a ('b 'f)`);

val _ = type_abbrev ("o_arrow", Type `: \'A.
  (!'a 'b 'c. (('b,'c) 'A) -> (('a,'b) 'A) -> (('a,'c) 'A))`);

val _ = type_abbrev ("id", Type `: \'A. !'a. ('a ('a 'A))`);

val _ = type_abbrev ("category", Type `: \'A. 'A id # 'A o_arrow`) ;

val category_def = new_definition("category_def",
  ``category = \:'A. \ (id: 'A id, comp: 'A o_arrow).
    (* Left Identity *)
    (!:'a 'b. !(f:'b ('a 'A)). comp id f = f) /\
    (* Right Identity *)
    (!:'a 'b. !(f:'b ('a 'A)). comp f id = f) /\
    (* Composition *)
    (!:'a 'b 'c 'd. !(f:'b ('a 'A)) (g:'c ('b 'A)) (h:'d ('c 'A)).
      comp h (comp g f) = comp (comp h g) f)``) ;

val dual_comp_def = Define
  `dual_comp (comp : 'A o_arrow) : ('A C) o_arrow =
    (\:'c 'b 'a. \f g. comp [:'a,'b,'c:] g f)` ;

category_dual : |- category [:'A:] (id, comp) <=>
  category [:'A C:] (id, dual_comp comp)
\end{verbatim}

Note that functors $F$ and $G$ (that is, their action on arrows) are
given, in \HOLw, as \texttt{F'} and \texttt{G}.
We use a prime in \texttt{F'} is because \texttt{F}
is the defined constant ``false''.

\begin{verbatim}
val _ = type_abbrev ("g_functor",
  Type `: \'C 'D 'F. !'a 'b. ('a, 'b) 'C -> ('a 'F, 'b 'F) 'D`);

val g_functor_def = Define
  `g_functor = \:'C 'D 'F. \ ((idC, compC) : 'C category)
     ((idD, compD) : 'D category) (F': 'F (('C, 'D) g_functor)).
  (* Identity *) (!:'a. F' [:'a, 'a:] idC = idD) /\
  (* Composition *) (!:'a 'b 'c. !f g.
    F' (compC [:'a,'b,'c:] g f) = compD (F' g) (F' f)) ` ; 
\end{verbatim}

\begin{verbatim}
val g_dual_functor_def = Define
  `g_dual_functor (F': 'F (('C, 'D) g_functor)) =
    (\:'a 'b. F' [:'b, 'a:]) : 'F (('C C, 'D C) g_functor)` ;

g_functor_dual :
  |- g_functor [:'C, 'D, 'F:] (idC,compC) (idD,compD) F' <=>
    g_functor [:'C C, 'D C, 'F:] (idC,dual_comp compC) 
      (idD,dual_comp compD) (g_dual_functor F') 
\end{verbatim}

\subsection{Definitions and Theorems characterising Adjoint Pairs}
\label{a-adjf}

We first show the definition of the predicates \texttt{g\_adjf}$n$, which are
used later.  These predicates do not represent the entire conditions for
adjoint pairs --- they do not include that $F,G$ are functors, that
$\eta,\epsilon$ are natural transformations, etc.
\begin{verbatim}
  |- g_adjf1 (idC,compC) G eta sharp <=>
     !:'a 'b. !f g. (compC (G g) eta = f) <=> (sharp f = g)

  |- g_adjf2 (idD,compD) F' eps flatt <=>
     !:'b 'a. !g f. (compD eps (F' f) = g) <=> (flatt g = f)

  |- g_adjf3 (idC,compC) (idD,compD) F' G eta eps <=>
     !:'a 'b. !f g. (compC (G g) eta = f) <=> (compD eps (F' f) = g)

  |- g_adjf4 (idC,compC) (idD,compD) sharp flatt <=>
     (!:'a 'b. !f g. (flatt g = f) <=> (sharp f = g)) /\
     (!:'a 'c 'b. !h f. sharp (compC f h) =
	  compD (sharp f) (sharp (compC (flatt idD) h))) /\
     !:'a 'c 'b. !h g. flatt (compD h g) =
	 compC (flatt (compD h (sharp idC))) (flatt g)))

  |- g_adjf5 (idC,compC) (idD,compD) F' G eta eps <=>
     (!:'b. compC (G eps) eta = idC) /\ !:'a. compD eps (F' eta) = idD
\end{verbatim}

Here are some examples of some duality theorems, required to use the duality of 
Theorem~\ref{t-adjf}\ref{t-adjf1} and \ref{t-adjf2},
whereas Theorem~\ref{t-adjf}\ref{t-adjf3} is self-dual.

\begin{verbatim}
g_adjf3_dual : |- g_adjf3 [:'C, 'D:] (idC,compC) (idD,compD) F' G eta eps =
    g_adjf3 [:'D C, 'C C:] (idD, dual_comp compD) (idC, dual_comp compC)
	  (g_dual_functor G) (g_dual_functor F') eps eta

g_adjf12_dual : |- g_adjf2 [:'D,'C:] (idD,compD) F' eps flatt =
    g_adjf1 [:'D C,'C C:] (idD, dual_comp compD) (g_dual_functor F') eps flatt

SHARP_FLATT_dual : |- SHARP (idD,compD) F' eps =
     FLATT (idD,dual_comp compD) (g_dual_functor F') eps

ETA_EPS_dual : |- ETA (idD,compD) flatt = EPS (idD,dual_comp compD) flatt
\end{verbatim}

Here are the theorems justifying Theorem~\ref{t-adjf}.
The actual text of all the theorems is rather long, and is omitted,
but it is clear from the way we construct the terms to be proved.
Note how we use the alternative versions, \texttt{cats'} and \texttt{taf3'},
to facilitate proving \texttt{adjf\_thm\_2\_eq\_3} by duality from 
\texttt{adjf\_thm\_1\_eq\_3}.  
Note also how we express the common definition in category theory texts, 
``\ldots there exists a unique arrow $g$ such that $G g \oo \eta = f$ \ldots''
as ``there exists a function $\cdot^\sharp$ such that $G g \oo \eta = f$ iff
$g = f^\sharp$''.
The final theorem, \texttt{g\_adjf4\_eqv}, expresses that the second and third
parts of Theorem~\ref{t-adjf}\ref{t-adjf4} are equivalent.

\begin{verbatim}
val gatm = ``category [:'C:] (idC, compC) ==> category [:'D:] (idD, compD) ==>
  g_adjf1 [:'C, 'D, 'F, 'G:] (idC,compC) G eta sharp ==>
  g_adjf2 [:'D, 'C, 'G, 'F:] (idD,compD) F' eps flatt ==>
  g_adjf3 [:'C, 'D, 'F, 'G:] (idC,compC) (idD,compD) F' G eta eps ==>
  g_adjf4 [:'C, 'D, 'F, 'G:] (idC,compC) (idD,compD) sharp flatt ==>
  (!:'a 'b. !f g. (flatt [:'b,'a:] g = f) <=> (sharp [:'a,'b:] f = g)) ==>
  (!:'a 'c 'b. !h f. sharp [:'a,'b:] (compC f h) =
    compD (sharp [:'c,'b:] f) (sharp (compC (flatt idD) h))) ==>
  (!:'a 'c 'b. !h g. flatt [:'c,'a:] (compD h g) =
    compC (flatt (compD h (sharp idC))) (flatt [:'b,'a:] g)) ==>
  g_adjf5 [:'C, 'D, 'F, 'G:] (idC,compC) (idD,compD) F' G eta eps ==>
  g_functor [:'D,'C,'G:] (idD,compD) (idC,compC) G ==>
  g_functor [:'C,'D,'F:] (idC,compC) (idD,compD) F' ==>
  g_nattransf [:'C:] (idC, compC) eta (g_I [:'C:]) (G g_oo F') ==>
  g_nattransf (idD,compD) eps (F' g_oo G) (g_I [:'D:]) ==>
  (eps = EPS (idC,compC) sharp) ==> (flatt = FLATT (idC,compC) G eta) ==>
  (eta = ETA (idD,compD) flatt) ==> (sharp = SHARP (idD,compD) F' eps) ==>
  (G = \:'a 'b. \g. flatt (compD g eps)) ==>
  (F' = \:'a 'b. \f. sharp (compC eta f)) ==> T `` ;

val ([catC, catD, adjf1, adjf2, adjf3, adjf4,
  adjf4a, adjf4b, adjf4c, adjf5, funG, funF,
  nteta, nteps, eps, flatt, eta, sharp, Geq, Feq], _) = strip_imp gatm ;

(* now to set out our adjoint functor results in the form in the paper *)
val cats = mk_conj (catC, catD) ;
val cats' = mk_conj (catD, catC) ;
val taf1 = list_mk_conj [funG, nteta, adjf1, eps, flatt, Feq] ;
val taf2 = list_mk_conj [funF, nteps, adjf2, eta, sharp, Geq] ;
val taf3 = list_mk_conj [funF, funG, adjf3, flatt, sharp] ;
val taf3' = list_mk_conj [funG, funF, adjf3, sharp, flatt] ;
val taf4 = list_mk_conj [adjf4, eta, eps, Feq, Geq] ;
val taf5 = list_mk_conj [funF, funG, nteta, nteps, adjf5, flatt, sharp] ;

val adjf_thm_1_eq_3 = store_thm ("adjf_thm_1_eq_3",
  mk_imp (cats, mk_eq (taf1, taf3)), ...) ;

val adjf_thm_2_eq_3 = store_thm ("adjf_thm_2_eq_3",
  mk_imp (cats', mk_eq (taf2, taf3')), ...) ;

val adjf_thm_3_eq_4 = store_thm ("adjf_thm_3_eq_4",
  mk_imp (cats, mk_eq (taf3, taf4)), ...) ;

val adjf_thm_3_eq_5 = store_thm ("adjf_thm_3_eq_5",
  mk_imp (cats, mk_eq (taf3, taf5)), ...) ;

(* to show the second and third parts of (iv) are equivalent *)
val g_adjf4_eqv = store_thm ("g_adjf4_eqv",
  list_mk_imp ([cats, adjf4a], mk_eq (adjf4b, adjf4c)), ...) ;
\end{verbatim}

\subsection{Definitions and Theorems about Monads} \label{a-monads}

Here is the definition of the Kleisli arrow type abbreviation. 
\begin{verbatim}
val _ = type_abbrev ("Kleisli", Type `: \'A 'M 'a 'b. ('a, 'b 'M) 'A`) ;
\end{verbatim}

The combination of postfix type constructors, and the fact that the
conventional notation $(\alpha, \beta) C$ is not syntactic sugar for a curried 
application of a higer order type constructor $C$ has led to the situation
where the following are all equivalent:
\begin{verbatim}
 ('A, 'M, 'a, 'b) Kleisli
 ('a, 'b) (('A, 'M) Kleisli) 
 'b ('a ('M ('A Kleisli)))
\end{verbatim}

We have several predicates defining, in various ways, a monad.
\begin{description}
\item[\texttt{Komonad}:] rules (\ref{extru}) to (\ref{extfun})
\item[\texttt{Kmonad}:] rules (\ref{extru}), (\ref{extlu}) and a variant of 
(\ref{extfun}) obtained by substituting (\ref{omext})
\item[\texttt{Kdomonad}:] rules (\ref{extru}) to (\ref{mapext})
\item[\texttt{Kdmonad}:] as for \texttt{Kmonad}, plus rules 
  (\ref{joinext}) and (\ref{mapext})
\item[\texttt{g\_umj\_monad}:] 
  the \emph{definition} of this is explained in Appendix~\ref{a-dmap},
  but it is \emph{proved} equivalent to rules (\ref{MJ1}) to
  (\ref{MJ7}) (in \texttt{g\_umj\_monad\_exp})
\end{description}

As noted in the main text, rules (\ref{extru}) to (\ref{extfun}) imply 
rule (\ref{omext}), and so we have the theorem \texttt{Komonad\_iff}.

\begin{verbatim}
Kcomp_def : |- !id comp ext.
  Kcomp (id,comp) ext = (\:'a 'b 'c. (\h k. comp (ext h) k))

Komonad_iff : |- category (id,comp) ==>
    (Komonad (id,comp) (unit,ext,kcomp) <=>
    Kmonad (id,comp) (unit,ext) /\ (kcomp = Kcomp (id,comp) ext)) 
\end{verbatim}

The pair of adjoint functors to and from the Kleisli category of a monad:
the adjoint functors are \ext\ and
the functor which is the identity on objects,
and takes arrow $f$ to $\unit \oo f$.
\begin{verbatim}
Komonad_IMP_uof :
    |- category (id,comp) /\ Komonad (id,comp) (unit,ext,kcomp) ==>
           g_functor (id,comp) (unit,kcomp) (\:'a 'b. comp unit)

Komonad_IMP_ext_f :
    |- Komonad (id,comp) (unit,ext,kcomp) ==>
           g_functor (unit,kcomp) (id,comp) ext
\end{verbatim}

The following theorems show that these functors form an adjoint pair:
they show respectively that \ext\ is a right adjoint, and that
\unit\ is a natural transformation.

\begin{verbatim}
Kmonad_IMP_adjf;
    |- Kmonad (id,comp) (unit,ext) ==> g_adjf1 (id,comp) ext unit (\:'a 'b. I)
     
Kmonad_IMP_unit_nt;
    |- Kmonad (id,comp) (unit,ext) ==>
       g_nattransf (id,comp) unit g_I (\:'a 'b. (\f. ext (comp unit f)))
\end{verbatim}

Finally,
every pair of adjoint functors $F$ and $G$ gives a monad, whose action on
objects is $G \oo F$, whose \unit\ ($\eta$) is just $\eta$ (!), 
% and whose \join\ is $G \epsilon F$
and where $\ext\ f$ is $G (f^\sharp)$
\begin{verbatim}
g_adjf1_IMP_Kmonad :
  |- category (idC,compC) /\ g_functor (idD,compD) (idC,compC) G /\
           g_adjf1 (idC,compC) G eta sharp ==>
	Kmonad (idC,compC) (eta,(\:'a 'b. G o sharp))
\end{verbatim}

\subsection{Definitions and Theorems about Compound Monads} \label{a-cm}

Here are the rules (\ref{KMJ1}) to (\ref{Kextjm}), 
which are the counterparts, for the monad \NKM\ in \KM, the Kleisli category
for $M$, of rules (\ref{MJ1}) to (\ref{extjm}).

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


Theorems \ref{thm-pext-k} and \ref{thm-when-pext} are combined in the 
single HOL theorem \texttt{cm\_Ko\_J1S}.

\begin{verbatim}
J1S_def : |- !id comp extM extNM.
   J1S (id,comp) extM extNM <=>
   !:'a 'b. !f. extM (extNM f) = comp (extNM f) (extM id)

cm_Ko_J1S : 
  |- category (id,comp) /\ Komonad (id,comp) (unitM,extM,kcomp) ==>
     (Komonad (id,comp) (unitNM,extNM,oNM) /\ J1S (id,comp) extM extNM /\
       (pext = (\:'a 'b. (\f. comp (extNM f) unitM))) <=>
     Komonad (unitM,kcomp) (unitNM,pext,oNM) /\
       (extNM = (\:'a 'b. (\f. extM (pext f)))))
\end{verbatim}

\subsection{Theorems about the Compatibility Conditions} \label{a-cc}

(C2) $\Rightarrow$ (C5):
holds even if $\mapM \joinN$ is replaced by an arbitrary term
\texttt{djoin}

\begin{verbatim}
BW_C2_C5: |- category (id,comp) /\ Kmonad (id,comp) (unitNM,extNM) ==>
       (extNM unitM = djoin) ==> (comp djoin (extNM id) = extNM djoin) 
\end{verbatim}

(C5) $\Rightarrow$ (C2):

\begin{verbatim}
BW_C5_C2 : |- category (id,comp) ==> Kmonad (id,comp) (unitNM,extNM) ==>
  Kdmonad (id,comp) (unitN,extN,mapN,joinN) ==>
  Kdmonad (id,comp) (unitM,extM,mapM,joinM) ==>
  (unitNM = (\:'b. comp unitM unitN)) ==>
  (comp (mapM joinN) (extNM id) = extNM (mapM joinN)) ==>
  (extNM unitM = mapM joinN)
\end{verbatim} 

(C3) $\Leftrightarrow$ (C4):
For these, we first showed that each of (C3) and (C4) are equivalent to their
more general versions (recall that (C4) is just J(1)).

\begin{verbatim}
C3_IFF_C3S:
  |- category (id,comp) /\ Kdmonad (id,comp) (unitM,extM,mapM,joinM) /\
       Kdmonad (id,comp) (unitN,extN,mapN,joinN) /\
       Kdmonad (id,comp) (unitNM,extNM,mapNM,joinNM) /\
       (mapNM = (\:'a 'b. (\f. mapM (mapN f)))) ==>
     ((!:'a. comp joinNM (mapM unitN) = joinM) <=>
     !:'a 'b. !f. comp (extNM f) (mapM unitN) = extM f)

C4_IFF_J1S:
  |- category (id,comp) /\ Kdmonad (id,comp) (unitM,extM,mapM,joinM) /\
       Kdmonad (id,comp) (unitNM,extNM,mapNM,joinNM) /\
       (!:'a 'b. !f. extM (mapNM f) = comp (mapNM f) joinM) ==>
     ((!:'a. extM joinNM = comp joinNM joinM) <=>
     J1S (id,comp) extM extNM)
\end{verbatim}

Then we show that the more general versions are equivalent.
\begin{verbatim}
J1S_IFF_C3S :
  |- category (id,comp) /\ Kdmonad (id,comp) (unitM,extM,mapM,joinM) /\
       Kmonad (id,comp) (unitNM,extNM) /\
       (unitNM = (\:'a. comp unitM unitN)) ==>
     (J1S (id,comp) extM extNM <=>
     !:'a 'b. !f. comp (extNM f) (mapM unitN) = extM f)
\end{verbatim}

\subsection{Duality of proofs:  
  (C2) $\Leftrightarrow$ (C5) and (C3) $\Leftrightarrow$ (C4)}
  \label{a-duality}
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_N, \mu_M &  & \joinNM, \joinN, \joinM \\
& \eta, \eta_N, \eta_M & & \unitNM, \unitN, \unitM \\
& T, N, M & & \mapNM, \mapN, \mapM \\
T & = M N &
\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 = M \eta_N \oo \eta_M & = \eta_M N \oo \eta_N \tag{C1} \\
\mu \oo M N \eta_M N & = M \mu_N \tag{C2} \\
\mu \oo M \eta_N M N & = \mu_M N  \tag{C3} \\
\mu_M N \oo M \mu & = \mu \oo \mu_M N M N \tag{C4} \\
M \mu_N \oo \mu N & = \mu \oo M N M \mu_N \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 $M$ or $N$ 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_N$ and of $\mu$.
% \newpage 
\begin{description}
\mditem[(C4) $\Rightarrow$ (C3):] \\[-4ex]
\begin{align*} \qquad
\mu \oo M \eta_N M N 
  & = \mu \oo \:(\mu_M \oo M \eta_M)\: N M N \oo M \eta_N M N
    \tag{\ref{MJ6} for $M$} \\[-0.5ex]
  & = \mu \oo \mu_M N M N \oo M \eta_M N M N \oo M \eta_N M N \\[-0.5ex]
  & = \mu \oo \mu_M N M N \oo M \:(\eta_M N \oo \eta_N)\: M N \\[-0.5ex]
  & = \mu \oo \mu_M N M N \oo M \eta M N \tag{C1} \\[-0.5ex]
  & = \mu_M N \oo M \mu \oo M \eta M N \tag{C4} \\[-0.5ex]
  & = \mu_M N \oo M \:(\mu \oo \eta M N)\: = \mu_M N \tag{\ref{MJ5} for $M N$}
\end{align*}
\mditem[(C3) $\Rightarrow$ (C4):] \\[-4ex]
\begin{align*}
\mu_M N \oo M \mu 
  & = \mu \oo M \eta_N M N \oo M \mu \tag{C3} \\[-0.5ex]
  & = \mu \oo M \:(\eta_N M N \oo \mu)\: \\[-0.5ex]
  & = \mu \oo M \:(N \mu \oo \eta_N M N M N)\: \tag{$\eta_N$ natural} \\[-0.5ex]
  & = \mu \oo M N \mu \oo M \eta_N M N M N \\[-0.5ex]
  & = \mu \oo \mu M N \oo M \eta_N M N M N \tag{\ref{MJ7} for $M N$} \\[-0.5ex]
  & = \mu \oo \mu_M N M N \tag{C3}
\end{align*}
\mditem[(C5) $\Rightarrow$ (C2):] \\[-4ex]
\begin{align*} \qquad
\mu \oo M N \eta_M N 
  & = \mu \oo M N M \:(\mu_N \oo \eta_N N)\: \oo M N \eta_M N
    \tag{\ref{MJ5} for $N$} \\[-0.5ex]
  & = \mu \oo M N M \mu_N \oo M N M \eta_N N \oo M N \eta_M N \\[-0.5ex]
  & = \mu \oo M N M \mu_N \oo M N \:(M \eta_N \oo \eta_M)\: N \\[-0.5ex]
  & = \mu \oo M N M \mu_N \oo M N \eta N \tag{C1} \\[-0.5ex]
  & = M \mu_N \oo \mu N \oo M N \eta N \tag{C5} \\[-0.5ex]
  & = M \mu_N \oo \:(\mu \oo M N \eta)\: N = M \mu_N \tag{\ref{MJ6} for $M N$}
\end{align*}
\mditem[(C2) $\Rightarrow$ (C5):] \\[-4ex]
\begin{align*}
M \mu_N \oo \mu N 
  & = \mu \oo M N \eta_M N \oo \mu N \tag{C2} \\[-0.5ex]
  & = \mu \oo \:(M N \eta_M \oo \mu)\: N \\[-0.5ex]
  & = \mu \oo \:(\mu M \oo M N M N \eta_M)\: N \tag{$\mu$ natural} \\[-0.5ex]
  & = \mu \oo \mu M N \oo M N M N \eta_M N \\[-0.5ex]
  & = \mu \oo M N \mu \oo M N M N \eta_M N \tag{\ref{MJ7} for $M N$} \\[-0.5ex]
  & = \mu \oo M N M \mu_N \tag{C2} 
\end{align*}
\end{description}

\subsection{Barr \& Wells (D3) and (D4) versus Jones \& Duponcheel S(4)} 
  \label{a-bw-jd}

Recall that 
\begin{itemize}
\item Barr \& Wells defined a distributive law to be a
natural transformation $\lambda$ saisfying their (D1) to (D4) 
\item
Barr \& Wells defined a compound monad satisfying (\ref{MC}) to satisfy the
compatibility condition if their (C1) to (C5) are satisfied
\item Barr \& Wells showed that compatibility and the existence of a
distributive law to be equivalent
\item
Jones \& Duponcheel assumed (\ref{MC}) and (\ref{UC}) throughout,
and showed that the existence of a function \swap\
(ie, $\lambda$) 
satisfying their conditions S(1) to S(4)
is equivalent to a compound monad satisfying J(1) and J(2)
\item S(1) is that \swap\ is natural, (C1) is (\ref{UC}),
(C4) and (C5) are J(1) and J(2), and 
(D1) and (D2) are S(3) and S(2)
\item We showed that 
(C3) and (C2) are equivalent to (C4) and (C5) respectively,
and so to J(1) and J(2)
\end{itemize}
Therefore we should be able to prove (D3) and (D4) from S(4),
and vice versa.
%
\begin{align*}
\swap \oo \mapN\ \unitM & = \unitM \\[-0.5ex]
  \lambda \oo N \eta_M & = \eta_M N 
  \tag{D1} \\
\swap \oo \unitN & = \mapM\ \unitN \\[-0.5ex]
  \lambda \oo \eta_N M & = M \eta_N 
  \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
  \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
  \tag{D4}
  \end{align*}
% 
\begin{gather*}
\prd  = \mapM\ \joinN \oo \swap \qquad \dorp  = \extM\ \swap \\
\prd \oo \mapN\ \dorp  = \dorp \oo \prd \tag*{S(4)}
\end{gather*}

To prove (D4) from S(4), do $\ldots \oo \mapN\ \unitM$ to both sides.
Then lhs gives 
$\prd \oo \mapN\ (\dorp \oo \unitM) = 
\prd \oo \mapN\ \swap$,
ie, the rhs of (D4).
Using (D1), $\prd \oo \mapN\ \unitM = \mapM\ \joinN \oo \unitM = \unitM \oo
\joinN$,
so $\dorp \oo \prd \oo \mapN\ \unitM = \extM\ \swap \oo \unitM \oo \joinN = 
  \swap \oo \joinN$, is, the lhs of (D4).

An argument which is actually dual in the sense described earlier gives 
(D3): it involves doing $\ldots \oo \mapN\ (\mapM\ \unitN)$.
(It uses (D2)).
From rhs of S(4), we get the rhs of (D3).
\begin{align*}
\dorp & \oo \prd \oo \mapN\ (\mapM\ \unitN) \\[-0.3ex]
& = \dorp \oo \mapM\ \joinN \oo \swap \oo \mapN\ (\mapM\ \unitN) \\[-0.3ex]
& = \dorp \oo \mapM\ \joinN \oo \mapM\ (\mapN\ \unitN) \oo \swap \\[-0.3ex]
& = \dorp \oo \mapM\ (\joinN \oo \mapN\ \unitN) \oo \swap \\[-0.3ex]
& = \extM\ \swap \oo \swap 
\end{align*}
From lhs of S(4), we get the lhs of (D3).
\begin{align*}
\prd & \oo \mapN\ \dorp \oo \mapN\ (\mapM\ \unitN) \\[-0.3ex]
  & = \prd \oo \mapN\ (\extM\ \swap \oo \mapM\ \unitN) \\[-0.3ex]
  & = \prd \oo \mapN\ (\extM\ (\swap \oo \unitN)) \\[-0.3ex]
  & = \prd \oo \mapN\ (\extM\ (\mapM\ \unitN)) \\[-0.3ex]
  & = \prd \oo \mapN\ (\mapM\ \unitN \oo \joinM) \\[-0.3ex]
  & = \prd \oo \mapN\ (\mapM\ \unitN) \oo \mapN\ \joinM 
\end{align*}
which is the lhs of (D3) because
\begin{align*}
\prd \oo \mapN\ (\mapM\ \unitN) 
  & = \mapM\ \joinN \oo \swap \oo \mapN\ (\mapM\ \unitN) \\[-0.3ex]
  & = \mapM\ \joinN \oo \mapM\ (\mapN\ \unitN) \oo \swap \\[-0.3ex]
  & = \mapM\ (\joinN \oo \mapN\ \unitN) \oo \swap = \swap
\end{align*}

For the converse, using (D3) and (D4) to prove S(4), we have
\begin{align*}
& \prd \oo \mapN\ \dorp \\[-0.3ex]
  & = \mapM\ \joinN \oo \swap \oo \mapN\ (\joinM \oo \mapM\ \swap) \\[-0.3ex]
  & = \mapM\ \joinN \oo \swap \oo \mapN\ \joinM \oo \mapN\ (\mapM\ \swap)
  \\[-0.3ex]
  & = \mapM\ \joinN \oo \joinM \oo \mapM\ \swap \oo 
    \swap \oo \mapN\ (\mapM\ \swap) \\[-0.3ex]
  & = \mapM\ \joinN \oo \joinM \oo \mapM\ \swap \oo 
     \mapM\ (\mapN\ \swap) \oo \swap \\[-0.3ex]
  & = \joinM  \oo \mapM\ (\mapM\ \joinN) \oo \mapM\ \swap \oo 
     \mapM\ (\mapN\ \swap) \oo \swap \\[-0.3ex]
  & = \joinM  \oo \mapM\ (\mapM\ \joinN \oo \swap \oo \mapN\ \swap)
    \oo \swap \\[-0.3ex]
  & = \joinM  \oo \mapM\ (\swap \oo \joinN) \oo \swap \\[-0.3ex]
  & = \extM\ \swap \oo \prd = \dorp \oo \prd 
\end{align*}

The proofs above were done in \HOLw.
The predicate \texttt{dist\_law} says that \swap\ is a natural transformation
and that (D1) to (D4) hold.
\begin{verbatim}
S_IFF_DL : |- category (id,comp) ==>
   Kdmonad (id,comp) (unitM,extM,mapM,joinM) ==>
   g_umj_monad (id,comp) (unitN,mapN,joinN) ==>
   (S1to4 (id,comp) (unitM,extM,mapM,joinM) (unitN,mapN,joinN) swap <=>
   dist_law (id,comp) (unitM,extM,mapM,joinM) (unitN,mapN,joinN) swap)
\end{verbatim}

\subsection{Proof that a \KM\ gives a natural transformation \swap} 
\label{a-swap-nt}
Note that it follows easily from (\ref{omext})
that $h \om (g \oo f) = (h \om g) \oo f$, 
so we omit the parentheses in such an expression.
%
\begin{align*}
& \swap \oo \mapN\ (\mapM\ f) \\[-0.3ex]
& = \kmap\ (\extM\ (\unitM \oo f)) \\[-0.3ex]
& = \kmap\ ((\unitM \oo f) \oM \id) \\[-0.3ex]
& = \kmap\ (\unitM \oo f) \oM \kmap\ \id \\[-0.3ex]
& = \pext\ (\unitNM \oM \unitM \oo f) \oM \swap \\[-0.3ex]
& = \pext\ (\unitNM \oo f) \oM \swap \\[-0.3ex]
& = \extM (\pext\ (\unitNM \oo f)) \oo \swap \\[-0.3ex]
& = \extNM (\unitNM \oo f) \oo \swap = \mapNM\ f \oo \swap 
\end{align*}

\subsection{Compatibility conditions imply a distributive law: further details} 
\label{a-cc-dl}

Assuming the compatibility condition (C4), ie (\ref{J1}),
we have the monad \NKM\ in \KM.
Next, 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$.
$$
\kjoin = \pext\ \unitM = \extNM\ \unitM \oo \unitM = 
  \mapM\ \joinN \oo \unitM = \unitM \oo \joinN 
  $$

We use the definition of the distributive law $\lambda$
\cite[\S 9.2]{bwttt}, ie, \swap\ \cite[\S 4.3]{jones-composing},
namely $\swap = \pext\ (\mapM\ \unitN)$.
We show this is equal to $\kmap\ \id$.
\begin{align*}
\swap = \pext\ (\mapM\ \unitN) & = \pext\ (\extM (\unitM \oo \unitN)) \\
  & = \pext\ (\unitNM \oM \id) = \kmap\ \id
\end{align*}


\subsection{Proof that a distributive law gives a monad in \KM} 
\label{a-DL-to-K}

Here we are {given} \swap\ satisfying (D1) to (D4), and we
\emph{define} 
\begin{align*}
\kjoin & = \unitM \oo \joinN \\
\kmap\ f & = \swap \oo \mapN\ f \\
\pext\ f & = \kjoin \oM \kmap\ f \\ % = \mapM\ \joinN \oo \kmap\ f \\
\unitNM & = \unitM \oo \unitN \\
\mapNM\ f & = \mapM\ (\mapN\ f) 
\end{align*}

We show (\ref{MJ1}K) to (\ref{MJ7}K), and also J(2).
Note that $\kjoin \oM f = \mapM\ \joinN \oo f$,
and 
$\kjoin \oM \unitM \oo g = \unitM \oo \joinN \oo g$.

(\ref{MJ1}K) is just (D1),
and $\kmap\ (\unitM \oo f) = \unitM \oo \mapN\ f$.
Thus
$\kmap\ \unitNM = \unitM \oo \mapN\ \unitN$ and
$\kmap\ \kjoin = \unitM \oo \mapN\ \joinN$.

Now (\ref{MJ5}K) to (\ref{MJ7}K) use 
(\ref{MJ5}N) to (\ref{MJ7}N) respectively. 

So for (\ref{MJ5}K), 
$\kjoin \oM \unitNM = = \unitM \oo \joinN \oo \unitN = \unitM$

For (\ref{MJ6}K), 
$\kjoin \oM \kmap\ \unitNM = = \unitM \oo \joinN \oo \mapN\ \unitN = \unitM$

For (\ref{MJ7}K), 
$\kjoin \oM \kjoin = \unitM \oo \joinN \oo \joinN$ 
and 
$\kjoin \oM \kmap\ \kjoin = \kjoin \oM (\unitM \oo \mapN\ \joinN) 
= \unitM \oo \joinN \oo \mapN\ \joinN$.

For (\ref{MJ3}K),
$\kmap\ f \oM \unitNM = \kmap\ f \oo \unitN
= \swap \oo \mapN\ f \oo \unitN
= \swap \oo \unitN \oo f
= \mapM\ \unitN \oo f
= \unitNM \oM f$

For (\ref{MJ4}K), using (D4) and (\ref{MJ4}N),
\begin{align*}
\kjoin \oM \kmap\ (\kmap\ f) 
& = \mapN\ \joinN \oo \swap \oo \mapN\ (\swap \oo \mapN\ f) \\[-0.3ex]
& = \mapN\ \joinN \oo \swap \oo \mapN\ (\swap \oo \mapN\ f) \\[-0.3ex]
& = \swap \oo \joinN \oo \mapN\ (\mapN\ f) \\[-0.3ex]
& = \swap \oo \mapN\ f \oo \joinN \\[-0.3ex]
& = \kmap\ f \oM \unitM \oo \joinN = \kmap\ f \oM \kjoin 
\end{align*}

For (\ref{MJ2}K), using (D3) and naturality of \swap:
\begin{align*} \kmap\ g \oM \kmap\ f 
& = \extM\ (\swap \oo \mapN\ g) \oo \swap \oo \mapN\ f \\[-0.3ex]
& = \extM\ \swap \oo \mapM (\mapN\ g) \oo \swap \oo \mapN\ f \\[-0.3ex]
& = \extM\ \swap \oo \swap \oo \mapN (\mapM\ g) \oo \mapN\ f \\[-0.3ex]
& = \swap \oo \mapN\ \joinM \oo \mapN (\mapM\ g) \oo \mapN\ f \\[-0.3ex]
& = \swap \oo \mapN\ (\extM\ g \oo f) = \kmap\ (g \oM f) 
\end{align*}

We have proved this result \HOLw.
Recall that 
the predicate \texttt{dist\_law} says that \swap\ is a natural transformation
and that (D1) to (D4) hold.

\begin{verbatim}
BWD_cm : |- category (id,comp) ==>
   Kdomonad (id,comp) (unitM,extM,kcomp,mapM,joinM) ==>
   g_umj_monad (id,comp) (unitN,mapN,joinN) ==>
   dist_law (id,comp) (unitM,extM,mapM,joinM) (unitN,mapN,joinN) swap ==>
   (kjoin = (\:'a. comp unitM joinN)) ==>
   (kmap = (\:'a 'b. (\f. comp swap (mapN f)))) ==>
   (unitNM = (\:'a. comp unitM unitN)) ==>
   g_umj_monad (unitM,kcomp) (unitNM,kmap,kjoin)
\end{verbatim}

We now have proved (\ref{MJ1}K) to (\ref{MJ7}K),
and our definition of \pext\ is (\ref{extjm}K)
so we can now use (\ref{joinext}K), ie $\pext\ \unitM = \kjoin$.
Then we can prove (C2), ie (J2),
assuming that $\extNM$ is defined by (\ref{PE}):
%
$$\extNM\ \unitM =  \extM\ (\pext\ \unitM) 
= \extM\ (\unitM \oo \joinN) = \mapM\ \joinN$$

Now we also want to show that when we define the monad $MN$ by
\extNM\ and \oNM, as in Theorem~\ref{thm-when-pext}, 
then the definition of \mapNM\ that results is equivalent to (\ref{MC}).
To show this, note that 
$\kmap\ (g \oo f) = \kmap\ g \oo \mapN\ f$ by definition, 
and that $\pext\ (g \oo f) = \pext\ g \oo \mapN\ f$ can be proved from it.
Then 
\begin{align*}
\extM\ (\pext\ (\unitNM \oo f)) & = \extM\ (\pext\ \unitNM \oo \mapN\ f) \\
& = \extM\ (\unitM \oo \mapN\ f) = \mapM\ (\mapN\ f) 
\end{align*}

So, from the premises of \texttt{BWD\_cm} we also get, 
in theorems \texttt{BWD\_cmK} and \texttt{BWD\_cmKJM}:
(premises as in \texttt{BWD\_cm} shown as \texttt{\dots})
\begin{verbatim}
BWD_cmK : |- ... ==>
   Kdmonad (unitM,kcomp) (unitNM,pext,kmap,kjoin)

BWD_cmKJM : |- ... ==>
  Kdmonad (unitM,kcomp) (unitNM,pext,kmap,kjoin) ==>
  (extM (pext unitM) = mapM joinN) /\
  (extM (pext (comp unitNM f)) = mapM (mapN f))
\end{verbatim}

\subsection{Generalising the 7-rule axiom system to Compound Monads}
\label{a-dmap}
We now present a generalisation of the system of axioms
(\ref{MJ1}) to (\ref{extjm}), and their equivalence to
(\ref{extru}) to (\ref{mapext}).
This was motivated by the construction by Jones \& Duponcheel
\cite[\S 3.3]{jones-composing}
using their function \dorp. % (see \S \ref{s-jddorp}).

We found that the rules (\ref{G1}) to (\ref{G8}),
which are analogous to rules (\ref{MJ1}) to (\ref{extjm}),
% shown in Table~\ref{tab-drules}
are sufficient to establish that $NM$ is a monad,
without assuming that either $N$ or $M$ is even a premonad.
In these rules, we make no assumptions about the functions
we call \extNM, \joinNM, \mapNM, \unitNM\ or \unitM. 

These rules also use three more functions of the following types:
\begin{align*}
\dunit & \ :\ \alpha M \to \alpha N M \\[-0.3ex]
\dmap & \ :\ (\alpha \to \beta M) \to (\alpha N M \to \beta N M) \\[-0.3ex]
\djoin & \ :\ \alpha N N M \to \alpha N M 
\end{align*}%
%
\setcounter{equation}{0}%
\renewcommand\theequation{G\arabic{equation}}%
\begin{align} % \label{tab-drules} was (\ref{G1}) to (\ref{G8})
\dmap\ \unitM &= \id \label{G1} \\[-0.3ex]
\dmap\ (f \oo h) &= \dmap\ f \oo \mapNM\ h \label{G2} \\[-0.3ex]
\dmap\ f \oo \unitNM &= \dunit \oo f \label{G3} \\[-0.3ex]
\djoin \oo \dmap\ (\dmap\ f) &= \dmap\ f \oo \joinNM 
  \label{G4} \\[-0.3ex]
\djoin \oo \dunit &= \id \label{G5} \\[-0.3ex]
\djoin \oo \dmap\ \unitNM &= \id \label{G6} \\[-0.3ex]
\djoin \oo \dmap\ \djoin &= 
  \djoin \oo \joinNM \label{G7} \\[1ex]
\extNM\ f &= \djoin \oo \dmap\ f \label{G8}
\end{align}
%
Now we can prove analogues of the equivalence of the various monad
presentations in \S\ref{s-monads}.  
In fact, the proofs are very similar to the proofs for a single monad.

\begin{theorem} \label{thm-G}
Assume rules (\ref{G1}) to (\ref{G8}).
Then \extNM, \joinNM, \mapNM\ and \unitNM\ give a monad $NM$,
where also
\begin{eqnarray}
\djoin & = & \extNM\ \unitM \label{G9} \\[-0.3ex]
\dmap\ f & = & \extNM\ (\dunit \oo f) \label{G10} \\[-0.3ex]
\unitNM & = & \dunit \oo \unitM \label{G11} \\[-0.3ex]
\mapNM\ f & = & \dmap\ (\unitM \oo f) \label{G12} 
\end{eqnarray}
\end{theorem}

The following converse result tells us when a monad $NM$ can be defined in this
way.  Note that we are still not assuming that $M$ or $N$ is a monad.

\begin{theorem} \label{thm-Grev}
Assume that $NM$ is a monad.
Also assume that rules (\ref{G5}) and (\ref{G9}) to (\ref{G11}) hold.
Then the remaining rules among (\ref{G1}) to (\ref{G8}) hold.
\end{theorem}

In the \HOLw\ implementation, \texttt{Gmonad} refers to rules 
(\ref{G1}) to (\ref{G7}).
Thus in \HOLw\ the equivalence \texttt{Gmonad\_iff\_Kmonad}
represents Theorems~\ref{thm-G} and \ref{thm-Grev}.

\begin{verbatim}
EXTD_def : |- !id comp dmap djoin.
   EXTD (id,comp) (dmap,djoin) = (\:'a 'b. (\f. comp djoin (dmap f)))
\end{verbatim}

\begin{verbatim}
Gmonad_iff_Kmonad : |- category (id,comp) ==>
  (Gmonad (id,comp) (dunit,dmap,djoin) (unitNM,mapNM,joinNM) unitM /\
  (extNM = EXTD (id,comp) (dmap,djoin)) <=>
  Kdmonad (id,comp) (unitNM,extNM,mapNM,joinNM) /\
  (djoin = (\:'a. extNM unitM)) /\
  (dmap = (\:'a 'b. (\f. extNM (comp dunit f)))) /\
  (unitNM = (\:'a. comp dunit unitM)) /\ !:'a. comp djoin dunit = id)
\end{verbatim}

Given a monad $NM$, we consider when it can be constructed using
Theorem~\ref{thm-G}, now assuming that $M$ and $N$ are monads.
Now, (\ref{G9}) and (\ref{G10}) are just definitions,
and we define $\dunit = \mapM\ \unitN$ to satisfy (\ref{G11}).
So the only condition is that (\ref{G5}) holds,
which is now $\extNM\ \unitM \oo \mapM\ \unitN = \id$.
As we noted earlier, \emph{either} J(1) \emph{or} J(2) implies this identity.

% \begin{gather*}
% \dunit = \mapM\ \unitN \tag{\ref{DU}}  \\
% \extNM\ \unitM \oo \mapM\ \unitN = \id \label{G5'} \tag{\ref{G5}$'$}
% \end{gather*}

The function \dorp\ of Jones \& Duponcheel \cite{jones-composing} 
is just $\dorp  = \dmap\ \id$.

\comment{
Now if we set $N$ to be the identity monad, 
then \dmap\ becomes \extM, \dunit\ and \djoin\ become the identity,
and \unitNM, \mapNM, \joinNM\ and \extNM\ become
\unitM, \mapM, \joinM\ and \extM.
}

Now if we set $M$ to be the identity monad, 
then \unitM\ becomes the identity,
\dunit, \dmap\ and \djoin\ become \unitN, \mapN\ and \joinN, 
and \unitNM, \mapNM, \joinNM\ and \extNM\ become
\unitN, \mapN, \joinN\ and \extN.

In fact in the \HOLw\ development, we \emph{defined} 
\texttt{g\_umj\_monad} in terms of \texttt{Gmonad} 
(\texttt{g\_umj\_monad\_def}), and then \emph{proved} that it corresponds 
to the usual statement of the 7 rules, in \texttt{g\_umj\_monad\_exp}.

\begin{verbatim}
g_umj_monad_exp : |- g_umj_monad (id,comp) (unit,map,join) <=>
   (!:'a. map id = id) /\
   (!:'a 'b 'c. !f g. map (comp g f) = comp (map g) (map f)) /\
   (!:'a 'b. !f. comp (map f) unit = comp unit f) /\
   (!:'a 'b. !f. comp (map f) join = comp join (map (map f))) /\
   (!:'a. comp join unit = id) /\ 
   (!:'a. comp join (map unit) = id) /\
   !:'a. comp join (map join) = comp join join
\end{verbatim}

\begin{verbatim}
g_umj_monad_def :
  |- g_umj_monad = (\:'A 'N. (\(id,comp) (unitN,mapN,joinN).
     Gmonad (id,comp) (unitN,mapN,joinN) (unitN,mapN,joinN) id))
\end{verbatim}

Then Theorem~\ref{thm-G} gives that rules (\ref{MJ1}) to (\ref{MJ7}),
with (\ref{extjm}) and (\ref{omext}) as definitions, imply rules
(\ref{extru}) to (\ref{extfun}) and the converse definitions
(\ref{joinext}) and (\ref{mapext}).

To use the converse Theorem~\ref{thm-Grev} in proving
the converse direction of Theorem~\ref{t-e3-umj7},
we would need to first prove (\ref{G5}), ie, $\joinN \oo \unitN = \id$,
which is easy --- it is just (\ref{extlu}), and also (\ref{omext}),
and then Theorem~\ref{thm-Grev} gives the rest.

\begin{verbatim}
EXT_def : |- !id comp map join.
   EXT (id,comp) (map,join) = (\:'a 'b. (\f. comp join (map f)))
\end{verbatim}

\begin{verbatim}
g_umj_iff_Kdomonad : |- category (id,comp) ==>
  (g_umj_monad (id,comp) (unit,map,join) /\
    (ext = EXT (id,comp) (map,join)) /\
    (kcomp = Kcomp (id,comp) ext) <=> 
  Kdomonad (id,comp) (unit,ext,kcomp,map,join))
\end{verbatim}

