%% LyX 1.4.1 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[english]{article}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\IfFileExists{url.sty}{\usepackage{url}}
                      {\newcommand{\url}{\texttt}}

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Bold symbol macro for standard LaTeX users
\providecommand{\boldsymbol}[1]{\mbox{\boldmath $#1$}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
%include lhs2TeX.fmt

\usepackage{babel}
\makeatother
\begin{document}

\title{Category Theory in DTH}


\author{Robin Green \url{mailto:greenrd@@greenrd.org}}

\maketitle
\begin{code}
#include "Macros.h"


\end{code}

\section{Equality}

We need to define two equality relation metatypes: one for object
equality, and one for individual equality, since objects and individuals
have different kinds. Also, for convenience, we further define a universal
equality for objects and a universal equality for individuals, in
which the equality scopes over all appropriate values. The universal
equalities imply the ordinary equalities.

NOTE: Ordinary object equality has not been defined yet because I
don't need it yet.


\subsection{Object equality}

\begin{code}
data UnivObjectEquality (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
  = UnivObjectEquality
  { univObEqReflexive :: UnivObReflexive eqR
  , univObEqSymmetric :: UnivObSymmetric eqR
  , univObEqTransitive :: UnivObTransitive eqR
  }

type UnivObReflexive (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
  = forall (a :: K_OBJECT). eqR a a

type UnivObSymmetric (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
  = forall (a :: K_OBJECT) (b :: K_OBJECT). eqR a b -> eqR b a

type UnivObTransitive (eqR :: K_CLASS(K_OBJECT -> K_OBJECT))
  = forall (a :: K_OBJECT) (b :: K_OBJECT) (c :: K_OBJECT). eqR a b -> eqR b c -> eqR a c
\end{code}

\subsection{Individual equality}

\begin{code}
data Equality (eqR :: K_RELATION) (a :: K_OBJECT) = Equality
  { eqReflexive :: Reflexive eqR a
  , eqSymmetric :: Symmetric eqR a
  , eqTransitive :: Transitive eqR a
  }

type Reflexive (eqR :: K_RELATION) (a :: K_OBJECT)
   = forall a1. a a1 -> eqR a1 a1

type Symmetric (eqR :: K_RELATION) (a :: K_OBJECT)
   = forall a1 a2. a a1 -> a a2 -> eqR a1 a2 -> eqR a2 a1

type Transitive (eqR :: K_RELATION) (a :: K_OBJECT)
   = forall a1 a2 a3. a a1 -> a a2 -> a a3 -> eqR a1 a2 -> eqR a2 a3 -> eqR a1 a3

type UnivReflexive (eqR :: K_RELATION)
   = forall a1. eqR a1 a1

type UnivSymmetric (eqR :: K_RELATION)
   = forall a1 a2. eqR a1 a2 -> eqR a2 a1

type UnivTransitive (eqR :: K_RELATION)
   = forall a1 a2 a3. eqR a1 a2 -> eqR a2 a3 -> eqR a1 a3

newtype Identity a = Identity {runIdentity :: a}
\end{code}

\section{Types as Theorems}

{}``The type \texttt{x} is inhabited'' represents {}``\texttt{x}
is true''. (All Haskell types are technically inhabited by the special
value $\bot$, which kills the program if it tries to pattern-match
it to anything, but in DTH we don't consider $\bot$ to be a well-defined
inhabitant of any type.)

Consequently, if there is a well-defined function (in the mathematical
sense, i.e. a non-partial function) from x to y, then x implies y.
(Proof: If x is inhabited, then there exists an \texttt{x1 :: x},
so there exists a value of \texttt{y} which the function takes \texttt{x1}
to, so \texttt{y} is inhabited.) In DTH, we don't allow partial functions,
but this is not checked at compile-time and therefore it is up to
the programmer to abide by it.

\texttt{x} and \texttt{y} are logically-equivalent iff \texttt{x}
implies \texttt{y} and \texttt{y} implies \texttt{x}:

\begin{code}
data LogEq (x :: *) (y :: *) = LogEq (x -> y) (y -> x)

id :: UnivReflexive (->)
id x = x

comp :: UnivTransitive (->)
comp g f x = f (g x)

(.) = (flip comp) :: (b -> c) -> (a -> b) -> a -> c

flip f x y = f y x

logEqUnivReflexive :: UnivReflexive LogEq
logEqUnivReflexive = LogEq id id

logEqUnivSymmetric :: UnivSymmetric LogEq
logEqUnivSymmetric (LogEq xy yx) = LogEq yx xy

logEqUnivTransitive :: UnivTransitive LogEq
logEqUnivTransitive (LogEq xy yx) (LogEq yz zy) = LogEq (yz . xy) (yx . zy)
\end{code}

\section{Category Theory}

\texttt{Category} is not a class, because we don't always want to
refer to all the type parameters - which type constraints would require
us to do.

\begin{code}
data Category (ob :: K_CLASS(K_OBJECT))
              (objectEquality :: K_CLASS(K_OBJECT -> K_OBJECT))
              (hom :: K_MORPHISM_CLASS)
              (morphismEquality :: K_RELATION)
              (morphismComposition :: K_RELATION -> K_RELATION -> K_RELATION)
              (identityRelation :: K_RELATION)
  = Category
  { mtCategoryObjectEquality :: UnivObjectEquality objectEquality
  , mtCategoryMorphismEquality :: Equality morphismEquality (IsAnyRelInstance hom)
  , objectEqualityType :: forall a b. objectEquality a b -> Pair (ob a) (ob b)
  , morphismType :: forall a b pcf. hom a b pcf -> Pair (ob a) (ob b)
  , morphismEqualityType :: forall f g. morphismEquality f g -> MorphismEqualityRes hom f g
  , composeOp :: forall a b c pcf pcg. hom b c pcf -> hom a b pcg -> hom a c (morphismComposition pcf pcg)
  , identityMorphism :: forall a. ob a -> hom a a identityRelation
  , leftIdentityLaw :: forall a b pcf. ob a -> ob b -> morphismEquality
      (hom a b (morphismComposition identityRelation pcf))
      (hom a b pcf)
  , rightIdentityLaw :: forall a b pcf. ob a -> ob b -> morphismEquality
      (hom a b (morphismComposition pcf identityRelation))
      (hom a b pcf)
  }

data IsAnyRelInstance (fn :: K_MORPHISM_CLASS) (r :: *)
   = forall a b. IsAnyRelInstance (IsRelInstance (fn a b) r)

data Pair a b = Pair { fst_ :: a, snd_ :: b }

data IsRelInstance (rc :: K_CLASS(K_RELATION)) (r :: *) = forall pcf. IsRelInstance (IdR (rc pcf) r)

data MorphismEqualityRes hom f g = forall a b. MorphismEqualityRes (IsRelInstance (hom a b) f) (IsRelInstance (hom a b) g)
\end{code}
In this context, a category \textsf{C} - which, for the moment, we
will take to be the universal DTH category:

\begin{code}
type DthUniverse = Category StdObjects StdUnivObjectEquality Fn FnEq ComposeR IdR

dthUniverse :: DthUniverse
dthUniverse = Category
  { mtCategoryObjectEquality = stdUnivObjectEquality
  , mtCategoryMorphismEquality = fnEq
  , objectEqualityType = \_ -> Pair StdObjects StdObjects
  , morphismType = \_ -> Pair StdObjects StdObjects
  , morphismEqualityType = \(FnEq _) -> MorphismEqualityRes (IsRelInstance IdR) (IsRelInstance IdR)
  , composeOp = compose
  , identityMorphism = \_ -> idFn
  , leftIdentityLaw = \_ _ -> FnEq (\_ _ -> LogEq (\(ComposeR IdR pcf) -> pcf) (ComposeR IdR))
  , rightIdentityLaw = \_ _ -> FnEq (\_ _ -> LogEq (\(ComposeR pcf IdR) -> pcf) (\pcf -> ComposeR pcf IdR))
  }
\end{code}
- consists of:

\begin{itemize}
\item a class \textsf{ob(C)} of objects, which are metatypes (i.e. Haskell
types of kind \texttt{{*} -> {*}}), which metaclassify metaterms

\begin{itemize}
\item metaterms, in turn, type terms
\item Recall (see section \ref{sec:Types-as-Theorems}) that metaterms represent
logical variables, while metatypes represent logical predicates
\end{itemize}
\end{itemize}
\begin{code}
data StdObjects (o :: K_OBJECT) = StdObjects
\end{code}
\begin{itemize}
\item An equality \textsf{=} on objects. \texttt{a}\textsf{=}\texttt{b}
iff \texttt{a} and \texttt{b} are the same Haskell type (modulo type
synonym substitution)
\end{itemize}
\begin{code}
data StdUnivObjectEquality (a :: K_OBJECT) (b :: K_OBJECT) where
       StdUnivObjectEquality :: StdUnivObjectEquality a a

stdUnivObjectEquality :: UnivObjectEquality StdUnivObjectEquality
stdUnivObjectEquality = UnivObjectEquality
  { univObEqReflexive = StdUnivObjectEquality
  , univObEqSymmetric = \StdUnivObjectEquality -> StdUnivObjectEquality
  , univObEqTransitive = \StdUnivObjectEquality StdUnivObjectEquality -> StdUnivObjectEquality
  }
\end{code}
\begin{itemize}
\item a class \textsf{hom(C)} of morphisms, which are metarelations from
metaterms to metaterms

\begin{itemize}
\item \texttt{Fn a b} metaclassifies metarelations from \texttt{a} to \texttt{b}
\item metarelations, in turn, dependently type functions
\item Below, \texttt{pc} is the postcondition of the function, expressed
as a relation between the input and the output. It does not matter
whether or not the relation \texttt{pc} relates individuals that are
not in the domain of the function to anything. This is because it
would not make sense in general to make \texttt{pc} impose the precondition,
because that is the job of \texttt{Fn}.
\end{itemize}
\end{itemize}
\begin{code}
type FnImpl (a :: K_OBJECT) (b :: K_OBJECT) (pc :: K_RELATION) = PrImp a (FnRes b pc)

newtype Fn (a :: K_OBJECT) (b :: K_OBJECT) (pc :: K_RELATION) = Fn (FnImpl a b pc)

-- FnRes is short for function result
-- FnRes b pc a1 = exists b1. pc a1 b1 && b b1
data FnRes (b :: K_OBJECT) (pc :: K_RELATION) (a1 :: *) = forall (b1 :: *). FnRes (pc a1 b1) (b b1)

-- Predicate implication
type PrImp p q = forall (b1 :: *). p b1 -> q b1


\end{code}
\begin{itemize}
\item An equality \textsf{=} on morphisms. \texttt{Fn a b r} = \texttt{Fn
c d s} iff \texttt{a}=\texttt{c}, \texttt{b}=\texttt{d} and \texttt{forall
a1 b1. a a1 -> b b1 -> (r a1 b1 <-> s a1 b1)}. Note that this does
\textit{not} compare the implementations, but the postconditions -
so two functions where one function has a postcondition that is more
specific than the other's postcondition, but where they both have
an identical implementation, would be treated as unequal by \texttt{FnEq}.
\end{itemize}
\begin{code}
data FnEq (f :: *) (g :: *) where
       FnEq :: (forall a1 b1. a a1 -> b b1 -> LogEq (pc1 a1 b1) (pc2 a1 b1))
            -> FnEq (Fn a b pc1) (Fn a b pc2)

fnEq :: Equality FnEq (IsAnyRelInstance Fn)
fnEq = Equality
  { eqReflexive = \(IsAnyRelInstance (IsRelInstance IdR)) -> FnEq (\_ _ -> logEqUnivReflexive)
  , eqSymmetric = \(IsAnyRelInstance (IsRelInstance IdR)) (IsAnyRelInstance (IsRelInstance IdR)) (FnEq eqAt)
    -> FnEq (logEqUnivSymmetric |<<| eqAt)
  , eqTransitive = \(IsAnyRelInstance (IsRelInstance IdR)) (IsAnyRelInstance (IsRelInstance IdR))
                    (IsAnyRelInstance (IsRelInstance IdR)) (FnEq eq1At) (FnEq eq2At)
    -> FnEq (\a1 b1 -> logEqUnivTransitive (eq1At a1 b1) (eq2At a1 b1))
  }

(|<<|) = (.) . (.)
\end{code}
\begin{itemize}
\item a morphism composition operator, \texttt{Compose}R, which metacomposes
metarelations

\begin{itemize}
\item A metatype implication for \texttt{ComposeR} is given by the signature:

\begin{itemize}
\item \texttt{compose :: Fn b c pcf -> Fn a b pcg -> Fn a c (ComposeR pcf
pcg)}
\item which translates to \texttt{compose :: (pcf :: Fn b c) -> (pcg :: Fn
a b) -> (ComposeR pcf pcg :: Fn a c)}
\end{itemize}
\item \texttt{ComposeR pcf pcg} relates \texttt{a1} to \texttt{c1} iff there
exists \texttt{b1} such that \texttt{pcg a1 b1} and \texttt{pcf b1
c1}
\item \texttt{ComposeR} is associative
\end{itemize}
\end{itemize}
\begin{code}
data ComposeR (pcf :: * -> * -> *) (pcg :: * -> * -> *) (a1 :: *) (c1 :: *) where
        ComposeR :: pcf b1 c1 -> pcg a1 b1 -> ComposeR pcf pcg a1 c1

compose :: Fn b c pcf -> Fn a b pcg -> Fn a c (ComposeR pcf pcg)
compose (Fn f) (Fn g) = Fn (\a -> case g a of (FnRes gab b) -> case f b of (FnRes fbc c) -> FnRes (ComposeR fbc gab) c)
\end{code}
\begin{itemize}
\item and an identity morphism, \texttt{IdR}

\begin{itemize}
\item A metatype implication for IdR is given by:

\begin{itemize}
\item \texttt{idFn :: Fn a a IdR}
\item which translates to \texttt{IdR :: Fn a a}
\end{itemize}
\item This satisfies the \texttt{leftIdentityRule} and \texttt{rightIdentityRule},
as proven above.
\end{itemize}
\end{itemize}
\begin{code}
data IdR (a :: *) (b :: *) where
     IdR :: IdR a a

idFn :: Fn a a IdR
idFn = Fn (FnRes IdR)
\end{code}

\section{Functors}

\begin{code}
type Functor c d cHom dHom pcSub ret
  = forall a b. Fn (Hom cHom a b)
    (Hom dHom (ret a) (ret b))
    (FunctorPC c d cHom dHom a b pcSub ret)

data Hom hom a b h where
  Hom :: hom a b pc -> Hom hom a b (hom a b pc)

data FunctorPC c d cHom dHom a b pcSub ret g r where
\end{code}
\texttt{ret} must take each object in \texttt{c} to an object in \texttt{d}
- but this is implied by the inhabitance of \texttt{Hom dHom (ret
a) (ret b)}, so we don't need to restate it.

\texttt{c} is a category:

\begin{code}
  FunctorPC ::
     Category cOb cObEq cHom cHomEq cHomComp cId
\end{code}
d is a category:

\begin{code}
    -> Category dOb dObEq dHom dHomEq dHomComp dId
\end{code}
fmap maps the identity to the identity:

\begin{code}
    -> dHomEq (dHom (ret a) (ret a) dId) (dHom (ret a) (ret a) (pcSub a a cId))
\end{code}
The law \texttt{fmap g . fmap h = fmap g . h}

\begin{code}
    -> (cOb e
    -> dHomEq (dHom (ret a) (ret e) (dHomComp (pcSub a b pcg) (pcSub b e pch)))
              (dHom (ret a) (ret e) (pcSub a e (cHomComp pcg pch))))

    -> FunctorPC (Category cOb cObEq cHom cHomEq cHomComp cId) (Category dOb dObEq dHom dHomEq dHomComp dId) cHom dHom a b pcSub ret (cHom a b pcg) (dHom (ret a) (ret b) (pcSub a b pcg))
\end{code}

\subsection{Universal functors}

A universal functor is an endofunctor over \texttt{dthUniverse}.

\begin{code}
type UnivFunctor pcSub ret
  = forall a b. Fn (Hom Fn a b)
    (Hom Fn (ret a) (ret b))
    (UnivFunctorPC a b pcSub ret)

data UnivFunctorPC a b pcSub ret g r where
  UnivFunctorPC ::
\end{code}
fmap maps the identity to the identity:

\begin{code}
    FnEq (Fn (ret a) (ret a) IdR) (Fn (ret a) (ret a) (pcSub a a IdR))
\end{code}
The law \texttt{fmap g . fmap h = fmap g . h}

\begin{code}
    -> FnEq (Fn (ret a) (ret e) (ComposeR (pcSub a b pcg) (pcSub b e pch)))
              (dHom (ret a) (ret e) (pcSub a e (ComposeR pcg pch)))

    -> UnivFunctorPC a b pcSub ret (Fn a b pcg) (Fn (ret a) (ret b) (pcSub a b pcg))
\end{code}
Universal functors are functors:

\begin{code}
univFunctorToFunctor :: UnivFunctor pcSub ret -> Functor DthUniverse DthUniverse Fn Fn pcSub ret
univFunctorToFunctor uf = Fn (foo uf)

foo :: UnivFunctor pcSub ret
 -> FnImpl (Hom Fn a b)
    (Hom Fn (ret a) (ret b))
    (FunctorPC DthUniverse DthUniverse Fn Fn a b pcSub ret)
foo (Fn uf) gab = case uf gab of
      FnRes (UnivFunctorPC idLaw compLaw) r
        -> FnRes (FunctorPC dthUniverse dthUniverse idLaw compLaw) r
\end{code}

\end{document}