mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
137 lines
11 KiB
TeX
137 lines
11 KiB
TeX
\chapter{Implementing Category Theory in Agda}\label{chp:agda-cat}
|
||
|
||
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 type checked 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 relevant parts of Agda's type theory, the agda-categories library, and the formalization of this thesis.
|
||
|
||
\section{The Underlying Type Theory}\label{sec:typetheory}
|
||
Agda implements a Martin-Löf style dependent type theory with \emph{inductive} and \emph{coinductive types} as well as an infinite hierarchy of universes \(Set_0, Set_1, \ldots\), where usually \(Set_0\) is abbreviated as \(Set\).
|
||
Recall that inductive types usually come with a principle for defining functions from inductive types, called \emph{recursion} and a principle for proving facts about inductive types, called \emph{induction}.
|
||
These are standard notions and need no further introduction. Coinductive types come with dual principles that are however lesser known.
|
||
Dually to inductive types that are defined by their \emph{constructors}, coinductive types are defined by their \emph{destructors} or their observational behavior. Take the type of streams over a type \(A\), for example. In Agda one would define this type as a coinductive record like so:
|
||
\begin{minted}{agda}
|
||
record Stream (A : Set) : Set where
|
||
coinductive
|
||
field
|
||
head : A
|
||
tail : Stream A
|
||
\end{minted}
|
||
i.e.\ the type of streams containing elements of type \(A\) is defined by its two destructors \(head : Stream\;A \rightarrow A\) and \(tail : Stream\;A \rightarrow Stream\;A\) that return the head and the tail of the stream respectively. Now, \emph{corecursion} is a principle for defining functions into coinductive types by specifying how results of the function may be observed. Take for example the following function which defines an infinite stream repeating the same argument and is defined by use of Agda's \emph{copatterns}.
|
||
\begin{minted}{agda}
|
||
repeat : {A : Set} (a : A) → Stream A
|
||
head (repeat a) = a
|
||
tail (repeat a) = repeat a
|
||
\end{minted}
|
||
Let us introduce the usual notion of stream bisimilarity. Given two streams, they are bisimilar if their heads are equal and their tails are bisimilar.
|
||
\begin{minted}{agda}
|
||
record _≈_ {A} (s : Stream A) (t : Stream A) : Set where
|
||
coinductive
|
||
field
|
||
head : head s ≡ head t
|
||
tail : tail s ≈ tail t
|
||
\end{minted}
|
||
In this definition \(≡\) is the built-in propositional equality in Agda with the single constructor \(refl\). We can now use coinduction as a proof principle to proof a fact about streams.
|
||
\begin{minted}{agda}
|
||
repeat-eq : ∀ {A} (a : A) → repeat a ≈ tail (repeat a)
|
||
head (repeat-eq {A} a) = refl
|
||
tail (repeat-eq {A} a) = repeat-eq a
|
||
\end{minted}
|
||
Where in the coinductive step we were able to assume that \(repeat\;a \approx tail(repeat\;a)\) already holds and showed that thus \(tail(repeat\;a) \approx tail(tail(repeat\;a))\) holds.
|
||
|
||
Streams are always infinite and thus this representation of coinductive types as coinductive records is well suited for them. However, consider the type of \emph{possibly} infinite lists, that we will call \(coList\). In pseudo notation this type can be defined as
|
||
\begin{minted}{agda}
|
||
codata coList (A : Set) : Set where
|
||
nil : coList A
|
||
_∷_ : A → coList A → coList A
|
||
\end{minted}
|
||
That is, the coinductive type \(coList\) is defined by the constructors \(nil\) and \(∷\). Agda does implement a second kind of coinductive types that allows exactly such definitions, however the use of these sometimes called \emph{positive coinductive types} is discouraged, since it is known to break subject reduction~\cite{agda-man}\cite{coq-man}. Instead, sticking to coinductive records, we can define \(coList\) as two mutual types, one inductive and the other coinductive:
|
||
\begin{minted}{agda}
|
||
mutual
|
||
data coList (A : Set) : Set where
|
||
nil : coList A
|
||
_∷_ : A → coList′ A → coList A
|
||
record coList′ (A : Set) : Set where
|
||
coinductive
|
||
field force : coList A
|
||
\end{minted}
|
||
Unfortunately, this does add the overhead of having to define functions on \(coList\) as mutual recursive functions, e.g.\ the \(repeat\) function from before can be defined as
|
||
\begin{minted}{agda}
|
||
mutual
|
||
repeat : {A : Set} (a : A) → coList A
|
||
repeat′ : {A : Set} (a : A) → coList′ A
|
||
repeat a = a ∷ repeat′ a
|
||
force (repeat′ a) = repeat a
|
||
\end{minted}
|
||
or more succinctly using an anonymous \(\lambda\)-function
|
||
\begin{minted}{agda}
|
||
repeat : {A : Set} (a : A) → coList A
|
||
repeat a = a ∷ λ { .force → repeat a }
|
||
\end{minted}
|
||
In \autoref{chp:setoids} we will work with such a coinductive type that is defined by constructors, hence to avoid the overhead of defining every data type twice and using mutual function definitions in the thesis, we will work in a type theory that does offer coinductive types with constructors and their respective corecursion and coinduction principles.
|
||
However, in the formalization we stick to using coinductive records as to implement best practices.
|
||
The translation between the two styles is straightforward, as illustrated by the previous example.
|
||
|
||
\section{Setoid Enriched Categories}
|
||
Let us now consider how to implement category theory in Agda. 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 \autoref{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 version of the notion 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 designers of agda-categories 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}
|
||
Every result and used fact (except for \autoref{prop:liftingkleisli}) in this thesis has been proven either in our own formalization\footnote{\href{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}} or in the agda-categories library~\cite{agda-categories}.
|
||
The formalization is meant to be used as a reference alongside this thesis, where concrete details of proofs can be looked up and verified.
|
||
The preferred format for viewing the formalization is as automatically generated clickable HTML code\footnote{\href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}},
|
||
where multiple annotations explaining the structure have been added in Markdown, however concrete explanations of the proofs and their main ideas are mostly just contained in this thesis.
|
||
|
||
In the future this formalization may be adapted into a separate library that uses the agda-categories library as a basis but is more focussed on the study of partiality monads and iteration theories.
|
||
As such the formalization has been structured similar to the agda-categories library, where key concepts such as monads correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties.
|