bsc-leon-vatthauer/thesis/src/02_agda-categories.tex

\chapter{Category Theory in Agda}

There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits of such a formalization are clear: having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
Ideally such a development will bring researchers together and enable them to work in a unified setting that enables efficient communication of ideas and concepts.
In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library that serves as an extensive foundation of categorical definitions.
This chapter shall serve as a quick introduction to the library and the formalization of this thesis.

\section{Setoid Enriched Categories}
The usual textbook definition of a category glosses over some design decisions that have to be made when implementing it in type theory. One would usually see something like this:
\begin{definition}[Category]
A category consists of
\begin{itemize}
  \item A collection of objects
  \item A collection of morphisms between objects
  \item For every two morphisms $f : X \rightarrow Y, g : Y \rightarrow Z$ another morphism $g \circ f : X \rightarrow Z$ called the composition
  \item For every object $X$ a morphism $id_X : X \rightarrow X$ called the identity
\end{itemize}
where the composition is associative and the identity morphisms are identities with respect to the composition.
\end{definition}

Here \textit{collection} refers to something that behaves set-like, which is not a set and is needed to prevent size issues (there is no set of all sets, otherwise we would obtain Russel's paradox, but there is a collection of all sets), it is not immediately clear how to translate this to type theory.
Furthermore in mathematical textbooks equality between morphisms is usually taken for granted, i.e. there is some global notion of equality that is clear to everyone. In type theory we need to be more thorough as there is no global notion of equality, eligible for all purposes, e.g. the standard notion of propositional equality has issues when dealing with functions in that it requires extra axioms like functional extensionality.

The definition of category that we will work with can be seen in listing~\ref{lst:category} (unnecessary information has been stripped). 
The key differences to the definition above are firstly that instead of talking about collections, Agda's infinite \Verb{Set} hierarchy is utilized to prevent size issues. 
The notion of category is thus parametrized by 3 universe levels, one for objects, one for morphisms and one for equalities. 
The consequence is that the category does not contain a type of all morphisms, instead it contains a type of morphisms for any pair of objects. 
Furthermore the types of morphisms are equipped with an equivalence relation \Verb{_≈_}, making them setoids. 
This addresses the aforementioned issue of how to implement equality between morphisms: the notion of equality is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}.
Because of using a custom equality relation, proofs like \Verb{∘-resp-≈} are needed throughout the library to make sure that operations on morphisms respect the equivalence relation.
Lastly, the authors also include symmetric proofs like \Verb{sym-assoc} to definitions, in this case to guarantee that the opposite category of the opposite category is equal to the original category, and a similar reason for requiring \Verb{identity²}, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis.

\begin{listing}[H]
  \begin{minted}{agda}
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    Obj : Set o
    _⇒_ : Obj → Obj → Set ℓ
    _≈_ : ∀ {A B : Obj } → (A ⇒ B) → (A ⇒ B) → Set e

    id  : ∀ {A : Obj} → (A ⇒ A)
    _∘_ : ∀ {A B C : Obj} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} 
      → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    sym-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} 
      → h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    identity² : ∀ {A} → id ∘ id {A} ≈ id {A}
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} 
      → f ≈ h 
      → g ≈ i 
      → f ∘ g ≈ h ∘ i
  \end{minted}
  \caption{Definition of Category~\cite{agda-categories}}
  \label{lst:category}
\end{listing}

From this it should be clear how other basic notions like functors or natural transformations look in the library. 

\section{The formalization}

\improvement{explain more}

The agda formalization of this thesis is structured similar to the agda-categories library, e.g. 'big' concepts like monads and categories get a top-level folder, that itself contains the core definitions, folders for sub-concepts and their properties, and possibly folders 'Instances' for specific instances and 'Construction' for blueprints for constructing this concept (e.g. the kleisli category of a monad would be in 'Category.Construction.Kleisli'. 

The source code of the formalization can be found \href{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}{here} (internal) or as clickable HTML \href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}{here} (public).