Work on thesis

thesis/main.tex

@@ -2,22 +2,8 @@
 
 \usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
 % \usepackage[utf8]{inputenc}
-\usepackage[ngerman,english]{babel}
+\usepackage[ngerman, english]{babel}
 \babeltags{german=ngerman}
-\usepackage{amssymb}
-\usepackage{amsthm}
-\usepackage{thmtools}
-\usepackage{fancyvrb}
-\usepackage{mathtools}
-\usepackage{amsmath}
-\usepackage{ifthen}
-\usepackage{xspace}
-\usepackage{hyperref}
-\usepackage{makeidx}
-\usepackage{graphicx}
-\usepackage{fvextra}
-\usepackage[style=ieee, sorting=ynt]{biblatex}    %advanced citations
-\usepackage[english=british]{csquotes}           %biblatex recommended to load this
 \usepackage{minted}
 \setminted[agda]{
   linenos=true,
@@ -26,6 +12,23 @@
   fontsize=\small,
   frame=lines
 }
+\usepackage{amssymb}
+\usepackage{amsthm}
+\usepackage{thmtools}
+\usepackage{fancyvrb}
+\usepackage{mathtools}
+\usepackage{amsmath}
+\usepackage{tikz}
+\usetikzlibrary{cd, babel, quotes}
+\usepackage{quiver}
+\usepackage{ifthen}
+\usepackage{xspace}
+\usepackage{hyperref}
+\usepackage{makeidx}
+\usepackage{graphicx}
+\usepackage{fvextra}
+\usepackage[style=ieee, sorting=ynt]{biblatex}    %advanced citations
+\usepackage[english=british]{csquotes}           %biblatex recommended to load this
 \usepackage{etoolbox,xpatch}
 
 \makeatletter
@@ -94,7 +97,6 @@
 %\usepackage{fontspec}
 %\setmonofont{Noto Sans Mono}
 
-
 \begin{document}
 \pagestyle{plain}
 \input{src/titlepage}%
@@ -115,21 +117,15 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
 
 % \include{src/examples}
 \include{src/00_introduction}
-
-%% IDEA: swap chapter 01 and 02, first introduce category theory in agda and then subsequently explain every notion in preliminaries with agda code.
-%% This is a major design decision..., there are two alternatives:
-%%% - introduce notions in latex and later give agda code (maybe in appendix)
-%%% - introduce notions in agda directly (maybe unreadable, maybe duplication with appendix)
 \include{src/01_preliminaries}
-%\include{src/03_iteration}
-%\include{src/04_partiality-monads}
-\chapter{Modelling partiality}
-% \include{src/05_monadK}
-\chapter{Case Study: The Quotiented Delay Monad}
+\include{src/02_agda-categories}
+\include{src/03_partiality-monads}
+\include{src/04_iteration}
+\include{src/05_setoids}
 \include{src/10_conclusion}
 
 \appendix
-\include{src/A1_contributions}
+% \include{src/A1_contributions}
 
 \medskip
 

thesis/quiver.sty

@@ -0,0 +1,40 @@
+% *** quiver ***
+% A package for drawing commutative diagrams exported from https://q.uiver.app.
+%
+% This package is currently a wrapper around the `tikz-cd` package, importing necessary TikZ
+% libraries, and defining a new TikZ style for curves of a fixed height.
+%
+% Version: 1.4.2
+% Authors:
+% - varkor (https://github.com/varkor)
+% - AndréC (https://tex.stackexchange.com/users/138900/andr%C3%A9c)
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{quiver}[2021/01/11 quiver]
+
+% `tikz-cd` is necessary to draw commutative diagrams.
+\RequirePackage{tikz-cd}
+% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
+\RequirePackage{amssymb}
+% `calc` is necessary to draw curved arrows.
+\usetikzlibrary{calc}
+% `pathmorphing` is necessary to draw squiggly arrows.
+\usetikzlibrary{decorations.pathmorphing}
+
+% A TikZ style for curved arrows of a fixed height, due to AndréC.
+\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
+    .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
+    and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
+    .. (\tikztotarget)\tikztonodes}},
+    settings/.code={\tikzset{quiver/.cd,#1}
+        \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
+    quiver/.cd,pos/.initial=0.35,height/.initial=0}
+
+% TikZ arrowhead/tail styles.
+\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
+\tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}}
+\tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}}
+% TikZ arrow styles.
+\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}
+
+\endinput

thesis/src/01_preliminaries.tex

@@ -1,56 +1,73 @@
-\chapter{Category Theory in Agda}
+\chapter{Preliminaries}
 
-There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits are clear, having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
-Also ideally such a development will bring researchers together and enable them to work in a unified setting.
-In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development. This also serves as a quick introduction to the library.
+We assume familiarity with basic categorical notions, in particular categories, functors, functor algebras and natural transformations.
+Other notions that are crucial to this thesis will be introduced in this section. 
+In the following sections we will work in an ambient category that is distributive and has a parametrized natural numbers object $\mathbb{N}$.
 
-\section{Setoid Enriched Categories}
-The usual textbook definition of category hides 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.
+\section{Distributive Categories}
+Let us first introduce notation for binary (co-)products by giving their defining diagrams:
+
+\begin{figure}[ht]
+% https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
+\[\begin{tikzcd}
+	A && {A \times B} && B && A && {A + B} && B \\
+	\\
+	&& C &&&&&& C
+	\arrow["{\pi_1}"', from=1-3, to=1-1]
+	\arrow["{\pi_2}", from=1-3, to=1-5]
+	\arrow["g"', from=3-3, to=1-5]
+	\arrow["f", from=3-3, to=1-1]
+	\arrow["{\exists! \langle f , g \rangle}"', dashed, from=3-3, to=1-3]
+	\arrow["{i_1}", from=1-7, to=1-9]
+	\arrow["{i_2}"', from=1-11, to=1-9]
+	\arrow["f"', from=1-7, to=3-9]
+	\arrow["g", from=1-11, to=3-9]
+	\arrow["{\exists ! [f , g]}", dashed, from=1-9, to=3-9]
+\end{tikzcd}\]
+\caption{The defining diagrams of products and coproducts}  
+\end{figure}
+
+We will furthermore overload this notation and write $f \times g := \langle f \circ \pi_1 , g \circ \pi_2 \rangle$ and $f + g := \lbrack i_1 \circ f ,  i_2 \circ g \rbrack$ for morphisms.
+
+We write $1$ for the terminal object together with the unique morphism $! : A \rightarrow 1$ and $0$ for the initial object with the unique morphism $\text{!`} : A \rightarrow 0$.
+
+\begin{definition}[Distributive Category]
+  \label{def:distributive}
+  A category $\mathcal{C}$ is called distributive if it has 
+  \begin{itemize}
+    \item finite products (i.e. binary products and a terminal object)
+    \item finite coproducts (i.e. binary coproducts and an initial object)
+  \end{itemize}
+  and the following is an iso:
+  % https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
+  \[\begin{tikzcd}
+    {X \times Y + X \times Z} &&& {X \times (Y + Z)}
+    \arrow["{dstl^{-1} := {\lbrack id \times i_1 , id \times i_2 \rbrack}}", curve={height=-18pt}, from=1-1, to=1-4]
+    \arrow["dstl", curve={height=-18pt}, from=1-4, to=1-1]
+  \end{tikzcd}\]
+  That is, a category is distributive if the canonical left-distributivity morphism $dstl^{-1}$ is an iso.
+  
 \end{definition}
 
-Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, preventing Russel's Paradox), it is not instantly clear how to translate this to a proof assistant. 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 Agda we need to be more thorough, there is no global notion of equality that 'just works', e.g. the standard notion of propositional equality has trouble dealing with functions and needs extra axioms like functional extensionality. 
+\begin{remark}
+  Definition~\ref{def:distributive} can equivalently be expressed by requiring that the canonical right-distributivity morphism is an iso, giving these inverse morphisms:
+  % https://q.uiver.app/#q=WzAsMixbMCwwLCJZIFxcdGltZXMgWCArIFpcXHRpbWVzIFgiXSxbMywwLCIoWSArIFopIFxcdGltZXMgWCJdLFswLDEsImRzdHJeey0xfSA6PSBbIGlfMSBcXHRpbWVzIGlkICwgaV8yIFxcdGltZXMgaWQgXSIsMCx7ImN1cnZlIjotM31dLFsxLDAsImRzdHIiLDAseyJjdXJ2ZSI6LTN9XV0=
+  \[\begin{tikzcd}
+    {Y \times X + Z\times X} &&& {(Y + Z) \times X}
+    \arrow["{dstr^{-1} := [ i_1 \times id , i_2 \times id ]}", curve={height=-18pt}, from=1-1, to=1-4]
+    \arrow["dstr", curve={height=-18pt}, from=1-4, to=1-1]
+  \end{tikzcd}\]
 
-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 \mintinline{agda}|Set| hierarchy is utilized to prevent size issues, i.e. the whole category is 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 set of all morphisms, instead it contains a set of morphisms for any pair of objects. Furthermore the sets of morphisms are equipped with an equivalence relation \mintinline{agda}|_≈_|, making them setoids. This solves the aforementioned issue of how to implement equality between morphisms, it is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}.
-Because of this proofs like \mintinline{agda}|∘-resp-≈| are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. Lastly, the authors also add symmetric proofs like \mintinline{agda}|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 \mintinline{agda}|identity²|, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis.
+  These two can be derived from each other by taking either
+  \[dstr := (swap + swap) \circ dstl \circ swap \]
+  or
+  \[dstl := (swap + swap) \circ dstr \circ swap \]
+  where $swap := \langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A$.
+\end{remark}
 
-For the rest of this thesis we will assume familiarity with basic concepts of category theory (like functors and natural transformations)~\cite{Lane1971}. We will not explain how they are implemented in order to look at more interesting concepts, for that one should seek out the agda-categories library (\href{https://github.com/agda/agda-categories}{Github}) or consult \cite{agda-categories}. We will however introduce further categorical notions using only their agda representation, it goes without saying that every time we say category, we actually mean setoid-enriched category as defined above.
+\section{Exponential Objects}
 
-\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}
+\section{Stable Natural Numbers Object}
 
 \section{Monads}
 Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis, so we will introduce them now. Categorically a Monad is a triple consisting of an endofunctor and two natural transformations called unit and multiplication satisfying some identity and associativity laws (also called the monad laws), the definition can be seen in listing~\ref{lst:monad}.
@@ -130,8 +147,6 @@ forgetting the naturality of $\eta$ and defining $f^* = \mu_Y \circ Ff$ for any
 
 For the rest of this thesis we will use both equivalent notions interchangeably to make definitions easier.
 
-% TODO agdaify this part
-
 \section{Strong and Commutative Monads}
 When modelling partiality with a monad, one would expect the following two programs to be equivalent:
 \begin{multicols}{2}
@@ -166,8 +181,4 @@ Now we can express the above condition:
   \]
 \end{definition}
 
-\section{Stable Natural Numbers Object}
-
-\section{Extensive and Distributive Categories}
-
-\section{Free objects}
+\section{Free Objects}

thesis/src/02_agda-categories.tex

@@ -0,0 +1,53 @@
+\chapter{Category Theory in Agda}
+
+There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits are clear, having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
+Also ideally such a development will bring researchers together and enable them to work in a unified setting.
+In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with. In this section we will talk about some design decisions that Hu and Carette made in their library that influence this development. This also serves as a quick introduction to the library.
+
+\section{Setoid Enriched Categories}
+The usual textbook definition of category hides 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 a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, preventing Russel's Paradox), it is not instantly clear how to translate this to a proof assistant. 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 Agda we need to be more thorough, there is no global notion of equality that 'just works', e.g. the standard notion of propositional equality has trouble dealing with functions and needs 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 \mintinline{agda}|Set| hierarchy is utilized to prevent size issues, i.e. the whole category is 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 set of all morphisms, instead it contains a set of morphisms for any pair of objects. Furthermore the sets of morphisms are equipped with an equivalence relation \mintinline{agda}|_≈_|, making them setoids. This solves the aforementioned issue of how to implement equality between morphisms, it is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}.
+Because of this proofs like \mintinline{agda}|∘-resp-≈| are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. Lastly, the authors also add symmetric proofs like \mintinline{agda}|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 \mintinline{agda}|identity²|, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis.
+
+For the rest of this thesis we will assume familiarity with basic concepts of category theory (like functors and natural transformations)~\cite{Lane1971}. We will not explain how they are implemented in order to look at more interesting concepts, for that one should seek out the agda-categories library (\href{https://github.com/agda/agda-categories}{Github}) or consult \cite{agda-categories}. We will however introduce further categorical notions using only their agda representation, it goes without saying that every time we say category, we actually mean setoid-enriched category as defined above.
+
+\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}

thesis/src/03_partiality-monads.tex

@@ -1,4 +1,4 @@
 \chapter{Partiality Monads}
-\section{Classifying Partiality Monads}
+\section{Properties of Partiality Monads}
 \section{The Maybe Monad}
 \section{The Delay Monad}

thesis/src/04_iteration.tex

@@ -1,3 +1,4 @@
 \chapter{Iteration Algebras and Monads}
 \section{Elgot Algebras}
-\section{Pre-Elgot Monads}
+\section{Pre-Elgot Monads}
+\section{The initial Pre-Elgot Monad}

thesis/src/05_monadK.tex

@@ -1 +0,0 @@
-\chapter{The K monad}

thesis/src/05_setoids.tex

@@ -0,0 +1 @@
+\chapter{A Case Study on Setoids}