
\section{Categorical Results ; Adjoint Functors} \label{s-adjf}

\subsection{Preliminary Results}
Our first illustration of using \HOLw\ relates to adjoint functors
between two categories.
Here our work also makes the assumption that the two categories have the same
objects (since we use, for objects, HOL types),
but we assert this does not affect the proof steps we need to perform.
% However we assert that, in performing the proof in \HOLw, 
% we go through substantially the same steps as one would do in a paper proof.
% The benefit of this is that the type system deals with some requirements,
% as mentioned above, 
% which are trivial in practice but add to the size of proofs in other
% formalisations.

% DEFINITION OF CATEGORIES, FUNCTORS, NTs
We assume a basic knowledge of categories, functors and natural
transformations.
See, eg, \cite{maclane-categories}, \cite{bwttt}, \cite{cockett}, \cite{turi}.
% , or many others, or Wikipedia.
We will write composition of arrows (morphisms)
right-to-left, thus $g \oo f$ where the source object of $g$ is the target
object of $f$.

Here we must put in a word about notation.
In HOL (as in its implementation and user interface language, Standard ML),
type constructors are written postfix, so $\alpha$ \texttt{list set}
is the type of sets of lists of things of type $\alpha$.
There are no higher-order type constructors, but type constructors 
can have multiple arguments, so $(\alpha, \beta)$ \texttt{prod}
is the type of pairs with components of type $\alpha$ and $\beta$.
In \HOLw\ this becomes a curried higher-order (type) function, 
so $(\alpha, \beta)$ \texttt{prod} equates to $\beta\ (\alpha\
\texttt{prod})$.
This means that while the action of a functor on arrows is
written on the left, the action of a functor on objects (types) is written on
the right.

In \cite{homeier} Homeier proved many results about categories,
functors and natural transformations, in the setting where objects are types
and arrows are functions between them
(in the \HOLw\ theory \texttt{functor}).
% We proved some results about adjoint functors in the same way,
% in the theory \texttt{adjoint}.
However, to be able to deal with the dual of a category 
we need a more general setting where arrows are of variable type 
$(\alpha, \beta)\ A$, or \texttt{('a,'b)\ 'A}, 
% where $\alpha$ and $\beta$ are the source and target types.
for source and target types $\alpha$ and $\beta$.
(In HOL a type \emph{variable} is preceded by a prime).
% This is actually syntactic sugar for $\beta (\alpha C)$. MENTIONED ABOVE
We proved general results in this setting in theory 
\texttt{category}, and our results about
adjoint functors in theory \texttt{g\_adjoint}.

Since our initial purpose of this generalisation was to allow for dual,
or opposite, 
categories, our first examples of type issues in \HOLw\ are in this setting.

\texttt{dual\_comp} takes an arrow composition function \texttt{comp} and
returns the appropriate function for composition of the arrows in the reverse
direction.  Note that it reverses not only the order of the two arrow arguments
but also the order of the three type (object) arguments involved.
If the types of arrows, originally, are $(\alpha, \beta)\ A$, then, when we are
using arrows backwards, the type of an arrow with source $\alpha$ and target
$\beta$ is $(\alpha, \beta)\ A\ C$, 
which is defined to be $(\beta, \alpha)\ A$, 
using the pre-defined (higher-order) type operator $C$.
Likewise, \texttt{o\_arrow} is defined as a type constructor to express the
type of an arrow composition function.
Note that \texttt{o\_arrow} is parameterised over the arrow type constructor
$A$; since, given $A$, 
an arrow composition function must apply to \emph{all} objects,
% and universally quantified over the three objects (types) involved:
it is universally quantified over the three types (objects) involved.  
We defined a predicate \texttt{category} (see Appendix~\ref{a-cat}),
asserting that the composition function $\circ$ is associative, and
that the identity arrow for each type (object) is the identity of $\circ$.
We show part of it below: the arguments are the arrow type constructor $A$,
the identity arrow function, of type $A\ \id$, 
which is, for each object (type) $\alpha$,
an arrow of type $(\alpha, \alpha) A$
and the arrow composition function, of type $A\ \oarrow$.
Then we could prove (\texttt{category\_dual})
that the dual of a category is a category.
%
\begin{gather*}
(\alpha, \beta)\ A\ C = (\beta, \alpha)\ A \qquad \qquad 
A\ \id = \forall \alpha.\ (\alpha, \alpha) A \\
A\ \oarrow = \forall \alpha \beta \gamma.\ 
  (\beta, \gamma) A \to (\alpha, \beta) A \to (\alpha, \gamma) A \\
\textit{category}\ [:A:]\ (\id: A\ \id, \comp: A\ \oarrow) = \ldots \\
\dualcomp\ \comp\ [:\gamma,\beta,\alpha:]\ f\ g =
  comp\ [:\alpha,\beta,\gamma:]\ g\ f 
\end{gather*}

Getting the statement of the theorem \texttt{category\_dual} to typecheck 
was difficult.  
Initally we had defined the \texttt{category} predicate without the explicit
type argument \texttt{'A}.  
In earlier examples this had caused no problems.
Although in this system type-checking involves higher-order unification of
type expressions, which doesn't give most general unifiers and therefore
principal types, the algorithm would manage when the types of arrows
consistently used the same type constructor.  
In this case we found that the only solution seemed to be a type parameter
(as putting more type annotations in did not succeed).
This required us to redefine the predicate \texttt{category} to have a type
parameter.
This would normally require every use of it to be changed to include the type
argument, but in fact since the inclusion of type arguments is optional in
\HOLw, changing the definition to include type arguments did not require
changing the other previous uses of \texttt{category} in the sources.

Recall that a functor (between categories with arrow
type constructors $C$ and $D$, say) comprises a mapping of objects
(in our \HOLw\ model this is a type constructor, say $F$),
and a mapping of arrows.
The arrow map must satisfy 
\begin{itemize}
\item preservation of sources and targets of objects:
the type of the arrow map, 
$\forall \alpha \beta.\ (\alpha, \beta) C \to (\alpha\ F, \beta\ F) D$
  (\emph{type abbreviation} \texttt{g\_functor}) ensures this
\item preservation of identity and composition of arrows:
the \emph{predicate} \texttt{g\_functor} (Appendix~\ref{a-cat}) specifies this
\end{itemize}
% The type abbreviation \gfunctor\ below represents the type of the arrow map
% part of a functor; the object map part is just the type constructor $F$.
% The type constructors $C$ and $D$ are the arrow type constructors for the
% source and target categories.

\comment{ SUPERSEDED BY THE ABOVE
In the above we distinguish the \emph{type} \texttt{('C, 'D, 'F) g\_functor}
which is the type of the arrow function, implying that its action on arrows
results in arrows in the category \texttt{'D} with the correct sources and
targets, from the predicate \texttt{g\_functor}, which asserts the 
equalities (preservation of identity and composition).
The object function is simply the type constructor \texttt{'F}.
END SUPERSEDED }

% g_functor and g_functor_def was here
% \begin{gather*}
% \gfunctor\ C\ D\ F = \forall \alpha \beta.\ 
  % (\alpha, \beta) C \to (\alpha\ F, \beta\ F) D 
% \end{gather*}

Stating duality theorems provided unexpected difficulties.  
Given the definition of a functor, ie, so far as types are concerned,
a function on objects (a type constructor) and a function on arrows, 
this should be unchanged for dual categories.
This is not so!  The type of the arrow map
% as above is
% $\forall \alpha \beta.\ (\alpha, \beta) C \to (\alpha\ F, \beta\ F) D$,
% but for the ``same'' functor between the dual categories, the required type is
% $\forall \beta \alpha.\ (\alpha, \beta) C \to (\alpha\ F, \beta\ F) D$,
% with the quantification order reversed.
is quantified over the 
source and target types, so % considering the functor for dual categories 
dualising the functor
requires changing the order of these two quantifications.
Function \texttt{g\_dual\_functor} (Appendix~\ref{a-cat})
dualises a functor in this way.
Once the statement was formalised correctly, 
it was trivial to prove (as \texttt{g\_functor\_dual}) 
that the ``dual'' of a functor is also a functor.

% g_dual_functor_def and g_functor_dual was here

%
\subsection{Adjoint Functors}

A pair of adjoint functors can be defined in several ways.
We first give two equivalent common definitions.

\begin{definition} \label{d-adjf}
For categories $\mathcal C$ and $\mathcal D$,
functors $F : \mathcal C \to \mathcal D$ and 
$G : \mathcal D \to \mathcal C$, form an \emph{adjunction}
(written $F \dashv G$) if 
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item \label{d-adjf1}
there is a natural transformation $\eta : I_{\mathcal C} \to G \oo F$, 
and for each arrow $f : A \to G B$ in $\mathcal C$,
there is a unique arrow $g : F A \to B$ in $\mathcal D$
(call it $g = f^\sharp$) such that $G g \oo \eta = f$, or
\item \label{d-adjf2}
there is a natural transformation $\epsilon : F \oo G \to I_{\mathcal D}$
and for each arrow $g : F A \to B$ in $\mathcal D$,
there is a unique arrow $f : A \to G B$ in $\mathcal C$
(call it $f = g^\flat$) such that $\epsilon \oo F f = g$
\end{enumerate}
\end{definition}

These definitions are dual and equivalent, and 
the functions $\cdot^\sharp$ and $\cdot\flat$ are mutually inverse.
Then these give $\epsilon = I_{\mathcal C}^\sharp$ and 
$\eta = I_{\mathcal D}^\flat$.
% and, further, that the action of $F$ and $G$ on
% arrows can be expressed in terms of $\epsilon, \eta, \cdot^\sharp$ and
% $\cdot\flat$, since
% \begin{align}
% (g \oo \epsilon)^\flat & = G(g \oo \epsilon) \oo \eta =
% G g \oo G \epsilon \oo \eta = G g \oo \epsilon^\flat =
% G g \oo I_{\mathcal C} = G g \tag{G} \\
% (\eta \oo f)^\sharp & = \epsilon \oo F(\eta \oo f) =
% \epsilon \oo F \eta \oo F f = \eta^\sharp \oo F f =
% I_{\mathcal D} \oo F f = F f \tag{F}
% \end{align}

So our first significant exercise in the use of \HOLw\ was to prove the
equivalence of these two definitions.
Since they are dual, we found an intermediate formulation which is self-dual,
which is Theorem~\ref{t-adjf}\ref{t-adjf3},
so having proved that \ref{t-adjf1} and \ref{t-adjf3} are equivalent,
we could use duality to prove that
\ref{t-adjf2} and \ref{t-adjf3} are equivalent.
This was actually not as easy as it sounds --- we had to formulate,
prove and use many lemmas expressing the duality between each component
of \ref{t-adjf2} and the corresponding component of \ref{t-adjf1}.
Cutting, modifying and pasting proofs might have been easier!

Performing these proofs had a surprising outcome: having formulated the
definitions above and done the proofs, we found that not all the assumptions
were necessary.  
While adjoint pairs are usually defined assuming $F$ and $G$ are
functors, we found that, for $F$ in Definition~\ref{d-adjf}\ref{d-adjf1},
and for $G$ in Definition~\ref{d-adjf}\ref{d-adjf2}, it is not necessary.  
This is found in Cockett \cite[Proposition~2.2.2]{cockett}
(though he says it was known earlier).
He then provided, essentially, Theorem~\ref{t-adjf}\ref{t-adjf4},
a criterion for an adjoint pair not assuming either $F$ or $G$ to satisfy the
functor equalities.
He then discovered a similar criterion and discussion in 
\cite[Definitions 109,110]{levy-thesis}, and the result
that the two parts of Theorem~\ref{t-adjf}\ref{t-adjf4} are equivalent,
in \cite[\S3.1]{dosen-bsl}.
% in \cite[\S3.1, p.258]{dosen-bsl}.

In the following theorem, $F,G, \eta,\epsilon, \cdot^\sharp$ and $\cdot^\flat$
are assumed to be of the appropriate ``types'' without necessarily satisfying 
the equalities for a functor, natural transformation, etc.
But it \emph{is} assumed that they return arrows in the correct categories,
with the correct source and target objects.
Note how the last few conditions in each criterion
are definitional: so, for example, 
when starting with \ref{t-adjf1}, with $G$, $\eta$ and $\cdot^\sharp$,
you can define $F$, $\epsilon$ and $\cdot^\flat$ to make the 
last three conditions true.
The \HOLw\ theorems underlying this result are described in
Appendix~\ref{a-adjf}.

\begin{theorem} \label{t-adjf}
Let $\mathcal C$ and $\mathcal D$ be categories.
Then the following are equivalent.
(Where relevant, conditions are for \emph{all} $f$, $g$ and $h$).
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item \label{t-adjf1}
$G$ is a functor, $\eta$ is natural,
$G g \oo \eta = f$ iff $g = f^\sharp$,
$\epsilon = I_{\mathcal C}^\sharp$, $g^\flat = G g \oo \eta$ and
$F f = (\eta \oo f)^\sharp$ 

\item \label{t-adjf2}
$F$ is a functor, $\epsilon$ is natural,
$\epsilon \oo F f = g$ iff $f = g^\flat$,
$\eta = I_{\mathcal D}^\flat$, $f^\sharp = \epsilon \oo F f$ and
$G g = (g \oo \epsilon)^\flat$

\item \label{t-adjf3}
$F$ and $G$ are functors, 
$G g \oo \eta = f$ iff $\epsilon \oo F f = g$,
$g^\flat = G g \oo \eta$ and $f^\sharp = \epsilon \oo F f$

\item \label{t-adjf4}
$\cdot^\sharp$ and $\cdot^\flat$ are mutually inverse,
$(f \oo h)^\sharp = f^\sharp \oo (\eta \oo h)^\sharp$ and/or
$(h \oo g)^\flat = (h \oo \epsilon)^\flat \oo g^\flat$ 
(which are equivalent),
$\eta = I_{\mathcal D}^\flat$, $\epsilon = I_{\mathcal C}^\sharp$,
$F f = (\eta \oo f)^\sharp$ and 
$G g = (g \oo \epsilon)^\flat$ 

\item \label{t-adjf5} \cite[Proposition 7.6]{turi}
$F$ and $G$ are functors, 
$\eta$ and $\epsilon$ are natural,
$G \epsilon \oo \eta G = I_{\mathcal C}G$,
$\epsilon F \oo F \eta = I_{\mathcal D}F$,
$g^\flat = G g \oo \eta$ and $f^\sharp = \epsilon \oo F f$
\end{enumerate}
\end{theorem}

