%%
%%
\documentclass[envcountsame]{llncs}
% \documentclass{acm_proc_article-sp}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{amssymb}
% \usepackage{exptrees}
\usepackage{url}

%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2
\newcounter{saveeqn} 
\newcommand\mditem[1][]{\item{\textmd{#1}}}

\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\title{Categories and Monads in HOL-Omega}
\author{Jeremy E. Dawson 
  \thanks{Supported by an Australian Research Council Large Grant}}

\institute{
Logic and Computation Group,
\\ College of Engineering and Computer Science,
\\ Australian National University,
   Canberra, ACT 0200, Australia
\\ \url{http://cecs.anu.edu.au/~jeremy/} 
}

\newcommand\cfile{}
%\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}

\newcommand\comment[1]{} 

% automatically defined in LLNCS style
% \newtheorem{theorem}{Theorem}%[chapter]
% \newtheorem{thm}{Theorem}%[chapter]
% \newtheorem{lemma}[thm]{Lemma}
% \newtheorem{defn}[thm]{Definition}
% \newtheorem{cor}{Corollary}[thm]
% \newtheorem{corollary}{Corollary}[thm]
% \renewcommand\thecor{\thethm(\arabic{cor})}

\pagestyle{myheadings}
\pagestyle{plain}

%% Title 
\maketitle

\date{\today}

\begin{abstract}
\comment{
We describe some proofs in category theory,
about adjoint functors and monads, 
using HOL-Omega, a recent extension of the HOL theorem prover.
We describe proofs giving various characterisations of a pair of adjoint
functors, of monads, and the relation between them.
A distributive law enables the composition of two monads;
we have found that a distributive law arises from one monad in the 
Kleisli category of another monad,
which simplifies the proofs of many relevant results in this area.
A distributive law, and conditions for it, have been described by
Barr \& Wells;
we found that a construction of Jones \& Duponcheel is also in fact a
distributive law, which has enabled us to simplify the conditions for
compatibility of monads of Barr \& Wells.
 
We discuss the value of HOL-Omega, and its type system,
for category theory proofs,
and the limitations of HOL-Omega for such proofs.
In our formalisation, objects are represented by types, and
we note how some category theory constructions cannot,
it seems, be formalised in this way.

and its use in proving results of category theory.
---------------------------------- NEW ATTEMPT FOLLOWS ------------------
}
We consider HOL-Omega, a recent extension by Homeier
to the type system of the HOL theorem prover.
We describe how it permits an implementation of categories,
where we model the objects of a category as the types of HOL-Omega.
This gives a ``light-weight'' implementation of categories 
into a theorem prover:
we explore how this is sufficient for easily proving some non-trivial results 
of category theory,
although some other results cannot be expressed in HOL-Omega in this way.
%
We illustrate the use of HOL-Omega by first proving the multiple
characterisations of an adjoint pair of functors.
Then we consider compound monads, where we consider distributive laws
and the conditions for compatibility of monads. 
We show how in HOL-Omega we can express the concept of a monad in the Kleisli
category of another monad, and use this to obtain easy proof of
some results about distributive laws,
including a new result simplifying the conditions of Barr \& Wells
for compatibility of monads. 
%
\\[1ex]
Keywords: formal verification, distributive law for monads, Kleisli category
\end{abstract}

\sloppy 

%\newpage

%% Here begins the main text

\newcommand\file{}

\newcommand\hinput[1]{\renewcommand\file{#1.tex}
  \markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
  \input{#1}}

\input{defs}
\input{intro}
\input{adjf}
\input{monads}
\input{cm}
\input{cfw}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

% \newpage
\input{bib}
\newpage
\appendix
\input{app}

\end{document}




