\section{Introduction} \label{s-intro}

\subsubsection{Monads and Adjoint Functors}
Monads have long been known in category theory, where a monad
consists of a endofunctor with two natural transformations
$\eta$ and $\mu$, satisfying three further identities.
%
An alternative presentation of a monad involves adjoint functors:
we consider some of the numerous ways of characterising the existence of a pair
of adjoint functors.

Moggi \cite{moggi} showed that useful notions of computations can be
represented by monads, and
Wadler, in \cite{wadler-essence} and subsequent papers,
expounded the idea for use in functional programming languages.  
Examples of monads are the exception monad 
(to model a computation which may fail),
the non-determinism monad (a computation which may produce multiple results).
% and the reader and writer monads (computations which, at each step, either
% read some input and act accordingly, or write some output).

\subsubsection{Distributive Laws for Monads}
Given two monads, these can sometimes, but not always,
be combined to form a monad
(for example, describing a computation which may fail,
but otherwise may produce multiple results).
Jones \& Duponcheel \cite{jones-composing} give a detailed account of various
ways to compose monads to form a compound monad.
It turns out that one of their constructions is equivalent to the
``distributive law'' of the category theory literature.
Barr \& Wells\cite[\S9.2]{bwttt} give five conditions for a compound monad to be
obtained from a distributive law, but we found that
two of these are redundant.
The approach of Barr \& Wells uses a monad in the Eilenberg-Moore category of
another monad ; our approach uses a monad in the Kleisli category of another
monad.
% Very recently Altenkirch et al \cite{alt-monads} have introduced the notion of
% a relative monad, which has a Kleisli category.  

\subsubsection{HOL and \HOLw}
There are potentially different ways to formalise category theory.
In a prover such as HOL, there is the limitation that
the logic is essentially based on sets.
If we overlook this we can model a category as a set of objects, and
a set of arrows each of which has a source and target object, and
a partial function for composition.
Here lies a difficulty: one is forever proving that the target of one arrow
is the source of another, before one can compose them.  
While this particular task is well suited to automation, 
it is a significant complication. %added difficulty.
In a dependently typed system, the type of arrows could be parameterised over
the source and target objects.
In \cite{huet-saibi}, Huet \& Saibi describe a formalisation in Coq which
addresses this problem essentially by creating a type for the set of arrows
between each pair of objects.

In \cite{kkr}, Kozen, Kreitz and Richter describe a formalisation of category
theory (in Nuprl), and briefly survey some other formalisations.
These explicitly state and prove requirements such as that composing arrows
require the target and source to match, and that a functor preserves source and
targets of an arrow.
Proofs in such formalisations tend to involve a vary large number of steps of
this nature, so that success requires a high degree of automation.

Another approach is to use the types of the HOL logic as the
objects of a category, as in \cite{homeier}.
This removes the difficulty mentioned above, since the type system 
can be used to 
avoid trying to compose arrows whose target and source do not match.
However it creates other difficulties, as discussed in more detail
by Homeier \cite{homeier}, which result from the fact that
the action of a functor on arrows,
and of a natural transformation, become polymorphic functions,
and the action of a functor on objects (types) is a type constructor.
% In the logic of the HOL and Isabelle theorem provers,
% type constructors (as distinct from types, which may be free variables) 
% in HOL and Isabelle can only be defined in advance,
% in a theory, as ``type constants''.
% Likewise polymorphic functions which are to be used differently 
% in a single term can only be defined in advance, in a theory,
% as a constant, as Homeier \cite[p.~245]{homeier} explains.

% Now, in the logic of the HOL or Isabelle provers, 
% we can define a type constructor in a theory.
% Further, if we define polymorphic functions as constants in a theory, 
% we can apply those functions to different types in a single term, 
% which we cannot do with polymorphic function variables,
% as Homeier \cite[p.~245]{homeier} explains.

% Thus we have in the past defined \emph{in a theory}
% a type constructor $M$ (as the action of a functor on objects)
% and polymorphic functions \unit, \map, \join\ and \ext,
% of the types shown in \S\ref{s-monads}.
% But to prove that some properties of these functions 
% (such as rules (\ref{MJ1}) to (\ref{MJ7}), in \S\ref{s-monads}) 
% imply others (such as rules (\ref{extru}) to (\ref{extfun})) 
% we have to \emph{assert}) rules (\ref{MJ1}) to (\ref{MJ7}) 
% \emph{in the theory},
% and prove (\ref{extru}) to (\ref{extfun}).
% Then to prove the converse we have to assert rules 
% (\ref{extru}) to (\ref{extfun}) in another theory,
% and prove (\ref{MJ1}) to (\ref{MJ7}).

Homeier \cite{homeier} developed \HOLw\ on top of HOL to 
solve these difficulties.  
Whereas HOL is based on a simply-typed lambda calculus (with first-order type
constructor constants and a distinguished boolean type), 
\HOLw\ also has universal types ($\forall \alpha. \sigma$),
and terms may be abstracted over types and applied to types, as in System F.
Types are of arbitrary kind, so there are type constructor variables, 
including higher-order type constructors,
and the language of types includes abstraction and application
as well as universal quantification.
In addition, a boolean term can be universally or existentially
quantified over a type.
% ($\forall: \alpha. P$ or $\exists: \alpha. P$).
% Terms may be abstracted over types and applied to types, 
% as well as other terms, 
Full details are in \cite{homeier}.
\HOLw\ is compatible with HOL,
that is, definitions and proof texts which use only
the features of HOL are accepted unchanged in \HOLw.

In \cite{homeier} Homeier used \HOLw\ to prove results on categories 
and monads, using a formalisation where arrows are functions.
We found it easy to generalise this, so the type of arrows between objects
(types) $\alpha$ and $\beta$ is not the function type $\alpha \to \beta$ but,
using a variable arrow type constructor $A$, is $(\alpha, \beta)\ A$.
This lets us define dual categories, and, importantly,
the Kleisli category of a monad (\S\ref{s-monads}).

In using this system to perform proofs in category theory, therefore, we
have made the simplifying assumptions that the objects of a category can be
equated to the types of \HOLw.  
As we discuss later, this limits the results we can express and prove.
It also means that in a logical sense, our results do not apply to all 
categories, since the logical model underlying HOL is based on sets,
but we assert that our proofs go through all the same steps as
one would in a pen-and-paper proof, and, as always, the advantage of
mechanisation is that none of these steps are overlooked.
The value of proceeding in this way is that the proofs can be more succinct,
since the type system guarantees certain things which would otherwise have to
be checked explicitly.
Essentially we have a ``light-weight'' implementation of categories
which enables simple proofs of certain results.
We go on to show that this implementation is sufficient to prove 
new results on a distributive law for monads: 
our result simplifies the definition of compatibility for monads,
and we also give some elegant proofs of existing results.

In \S \ref{s-adjf}, we introduce the representation of categories in \HOLw,
and focus on type issues by discussing definitions and theorems about 
the dual of a category.  
We then give several equivalent characterisations of pairs of adjoint functors.
In \S \ref{s-monads} we discuss monads, their characterisations,
and the Kleisli category of a monad. 
In \S \ref{s-cm} we discuss composition of monads, and where this arises
from a distributive law, and 
% how we applied results from \S \ref{s-monads} to 
from a monad in the Kleisli category of another monad.

At present \HOLw\ is a branch in the \texttt{subversion} HOL repository,
and the proofs referred to in the text are contained among the \HOLw\ examples,
located at 
\url{https://hol.svn.sf.net/svnroot/hol/branches/HOL-Omega/examples/HolOmega},
with some files in the subdirectory \texttt{interim}.
Where results are mentioned in the text,
the HOL code of relevant definitions and theorems are given in the Appendix,
which is available in 
\url{http://users.rsise.anu.edu.au/~jeremy/pubs/holw-cm/}.
% which the text of selected definitions and theorems.
A name appearing in the text, as (\texttt{thm\_name}) is the name of 
a theorem or defined constant; % in \HOLw;
these are shown in the Appendix.

