remove old readme

.gitignore

@@ -52,3 +52,5 @@ _region_.tex
 *.xdv
 thesis/_minted-main/
 slides/_minted-main/
+thesis/main.bbl-SAVE-ERROR
+thesis/main.bcf-SAVE-ERROR

README.md

@@ -1,38 +1,7 @@
-# BSc Leon Vatthauer
+# Implementing Categorical Notions of Partiality and Delay in Agda
 
-Here I am formalizing some notions of this paper [https://arxiv.org/pdf/2102.11828.pdf](https://arxiv.org/pdf/2102.11828.pdf) in agda.
-The whole project consists of literate agda files, where I add my documentation as markdown.
-A (mostly up to date) version can be found here: https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/
+This repository contains the work I have done for my bachelor thesis.
 
-## Usage
-The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project.
+The goal was to formalize proofs of this paper [https://arxiv.org/pdf/2102.11828.pdf](https://arxiv.org/pdf/2102.11828.pdf) in Agda and study categorical notions in general.
 
-To use the project you just have to open a development shell:
-```sh
-nix develop .
-```
-(this will take 20 - 30 minutes the first time, because it has to typecheck the agda-categories library)
-
-There is also a Makefile for compiling every module and generating the html documentation.
-
-```
-make
-```
-
-## Contributions to *agda-categories*
-This project uses the awesome category theory library for agda ([agda-categories](https://github.com/agda/agda-categories)), it is already very extensive, but some notions needed here are missing, so I contribute them to the library.
-So far the contributions are:
-1. Kleisli triples [[merged](https://github.com/agda/agda-categories/pull/381)]
-    - `Categories.Monad.Construction.Kleisli`
-2. Distributive categories (and the relation to extensivity) [[merged](https://github.com/agda/agda-categories/pull/383)] [[merged](https://github.com/agda/agda-categories/pull/410)]
-    - `Categories.Category.Distributive`
-    - `Categories.Category.Distributive.Properties`
-    - `Categories.Category.Extensive.Bundle`
-    - `Categories.Category.Extensive.Properties.Distributive`
-3. Parametrized (or stable) natural numbers objects [[merged](https://github.com/agda/agda-categories/pull/394)]
-    - `Categories.Object.NaturalNumbers.Parametrized`
-    - `Categories.Object.NaturalNumbers.Properties.F-Algebra`
-    - `Categories.Object.NaturalNumbers.Properties.Parametrized`
-4. Commutative monad [[merged](https://github.com/agda/agda-categories/pull/404)]
-    - `Categories.Monad.Commutative`
-    - `Categories.Monad.Strong.Properties`
+The subfolders contain my code, the thesis and the slides of my presentation, each with its own README documenting how to build it.

agda/README.md

@@ -0,0 +1,37 @@
+# The Agda formalization
+
+The whole project consists of literate agda files, where I add my documentation as markdown.
+A (mostly up to date) version can be found here: https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/
+
+## Usage
+The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project.
+
+To use the project you just have to open a development shell:
+```sh
+nix develop .
+```
+(this will take 20 - 30 minutes the first time, because it has to typecheck the agda-categories library)
+
+There is also a Makefile for compiling every module and generating the html documentation.
+
+```
+make
+```
+
+## Contributions to *agda-categories*
+This project uses the awesome category theory library for agda ([agda-categories](https://github.com/agda/agda-categories)), it is already very extensive, but some notions needed here are missing, so I contribute them to the library.
+So far the contributions are:
+1. Kleisli triples [[merged](https://github.com/agda/agda-categories/pull/381)]
+    - `Categories.Monad.Construction.Kleisli`
+2. Distributive categories (and the relation to extensivity) [[merged](https://github.com/agda/agda-categories/pull/383)] [[merged](https://github.com/agda/agda-categories/pull/410)]
+    - `Categories.Category.Distributive`
+    - `Categories.Category.Distributive.Properties`
+    - `Categories.Category.Extensive.Bundle`
+    - `Categories.Category.Extensive.Properties.Distributive`
+3. Parametrized (or stable) natural numbers objects [[merged](https://github.com/agda/agda-categories/pull/394)]
+    - `Categories.Object.NaturalNumbers.Parametrized`
+    - `Categories.Object.NaturalNumbers.Properties.F-Algebra`
+    - `Categories.Object.NaturalNumbers.Properties.Parametrized`
+4. Commutative monad [[merged](https://github.com/agda/agda-categories/pull/404)]
+    - `Categories.Monad.Commutative`
+    - `Categories.Monad.Strong.Properties`

slides/Makefile

@@ -0,0 +1,17 @@
+src = $(wildcard *.tex)
+pdf = $(src:.tex=.pdf)
+imgpdf = $(wildcard img/*.pdf)
+
+.PHONY: all clean
+
+all: $(pdf) $(imgpdf)
+
+%.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib) $(imgpdf)
+	latexmk -pdf -xelatex -shell-escape -file-line-error -synctex=1 -halt-on-error -shell-escape $<
+
+clean:
+	latexmk -C $(src)
+	rm -f $(wildcard *.out *.nls *.nlo *.bbl *.blg *-blx.bib *.run.xml *.bcf *.synctex.gz *.fdb_latexmk *.fls *.toc)
+	rm -f $(wildcard src/*.aux)
+
+

slides/README.md

@@ -0,0 +1,8 @@
+# The slides
+This folder contains the source of my slides for the presentation at the Oberseminar on the 23.01.2024.
+
+## Requirements
+Building the slides requires a working xelatex installation. Since I am using the [minted]([minted](https://ctan.org/pkg/minted)) package for representing Agda code you will also need the Python syntax highlighter [Pygments](https://pygments.org/).
+
+## Usage
+To compile the slides just run `make` with the needed programs installed.

thesis/Makefile

@@ -2,16 +2,12 @@ src = $(wildcard *.tex)
 pdf = $(src:.tex=.pdf)
 imgpdf = $(wildcard img/*.pdf)
 
-.PHONY: all clean install
+.PHONY: all clean
 
 all: $(pdf) $(imgpdf)
 
 %.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib) $(imgpdf)
-	latexmk -file-line-error -synctex=1 -halt-on-error -shell-escape -pdf $<
-
-fast:
-	# enforce tex execution
-	pdflatex -synctex=1 $(src)
+	latexmk -pdf -xelatex -shell-escape -file-line-error -synctex=1 -halt-on-error -shell-escape $<
 
 clean:
 	latexmk -C $(src)

thesis/README.adoc

@@ -1,42 +0,0 @@
-README
-======
-
-About
------
-The present collection of files offers a template for a final thesis (no matter
-whether project, bachelor, or master thesis). You are welcome to modify anything
-to your personal needs. In case of any ambiguity, consult your supervisor on
-formal aspects of the document, instead of just relying of my design choices for
-the present template.
-
-Also see the content of template-master-thesis.pdf for some more suggestions.
-
-Usage
------
-It is strongly recommended to use a latex wrapper like latexmk (or rubber), in
-order to build it. You can find a Makefile in the toplevel directory providing
-a nice interface to latexmk:
-
-Type `make` In order to build the PDF, type `make clean` to remove all
-automatically generated files (including the PDF).
-
-License of this Template
-------------------------
-You can freely use the present template for your final thesis (i.e. master or bachelor or project thesis).
-It is not mandatory at all to use this template for your final thesis.
-It is just a suggestion! You are also allowed to change anything you would like to change in order to fit your needs/taste/...
-
-License for your Thesis
------------------------
-The template includes a http://creativecommons.org/licenses/by-sa/4.0/[Creative Commons Attribution-ShareAlike 4.0 International License] license remark as suggested license for your thesis.
-We suggest you keep this license although you are free to choose a different license.
-
-License for your Implementation
--------------------------------
-For implementations you write as part of your thesis we recommend to use a different repository and license this code under an Open Source license like GPL-3 or Apache.
-When choosing a license for your implementations keep in mind that containing/modifying previous implementations licensed under GPL-3 requires you to use GPL-3 for your code as well.
-
-It is common to indicate the license of your code via a file called LICENSE in the folder of your repository.
-If such a file does not exist already, GitLab displays a button "Add LICENSE" where you can select from common licenses as a template.
-
-// vim: tw=80 ft=asciidoc

thesis/README.md

@@ -0,0 +1,8 @@
+# The thesis
+This folder contains the source of my thesis.
+
+## Requirements
+Building the thesis requires a working xelatex installation. Since I am using the [minted]([minted](https://ctan.org/pkg/minted)) package for representing Agda code you will also need the Python syntax highlighter [Pygments](https://pygments.org/).
+
+## Usage
+To compile the thesis just run `make` with the needed programs installed.

thesis/bib.bib

@@ -186,7 +186,7 @@
   doi        = {10.1016/S0304-3975(02)00728-4},
   abstract   = {Infinite trees form a free completely iterative theory over any given signature--this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(-) + X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees.This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H ⊗ _ + I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.},
   journal    = {Theor. Comput. Sci.},
-  month      = {may},
+  month      = {5},
   pages      = {1–45},
   numpages   = {45},
   keywords   = {coalgebra, completely iterative theory, monad, monoidal category, solution theorem}

thesis/main.tex

@@ -18,6 +18,12 @@
 \usepackage{fancyvrb}
 \usepackage{mathtools}
 \usepackage{amsmath}
+\usepackage{mathpartir}
+% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
+\makeatletter
+\let\atop\@@atop
+\makeatother
+
 \usepackage{tikz}
 \usetikzlibrary{cd, babel, quotes}
 \usepackage{quiver}
@@ -79,7 +85,7 @@
 \setlength{\parskip}{6pt}
 \setlength{\marginparsep}{0cm}
 
-\title{Implementing Notions of Partiality and Delay in Agda}
+\title{Implementing Categorical Notions of Partiality and Delay in Agda}
 
 \author{Leon Vatthauer}
 
@@ -98,8 +104,6 @@
 %\usepackage{fontspec}
 %\setmonofont{Noto Sans Mono}
 
-\usepackage{mathpartir}
-
 \newcommand{\obj}[1]{\ensuremath{\vert \mathcal{#1} \vert}}
 \begin{document}
 \pagestyle{plain}

thesis/src/01_preliminaries.tex

@@ -67,8 +67,8 @@ Categories with finite products (i.e. binary products and a terminal object) are
 
 \begin{proposition}
   The distribution morphisms can be viewed as natural transformations i.e. they satisfy the following diagrams:
-% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiIsMl1d
-\[\begin{tikzcd}
+  % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiJdXQ==
+  \[\begin{tikzcd}[column sep=4ex]
     {X \times (Y +Z)} && {A \times (B + C)} & {(Y + Z) \times X} && {(B + C) \times A} \\
     {X \times Y + X \times Z} && {A \times B + A \times C} & {Y \times X + Z \times X} && {B \times A + C \times A}
     \arrow["{f \times (g + h)}", from=1-1, to=1-3]
@@ -78,8 +78,8 @@ Categories with finite products (i.e. binary products and a terminal object) are
     \arrow["{(g + h) \times f}", from=1-4, to=1-6]
     \arrow["dstr"', from=1-4, to=2-4]
     \arrow["dstr", from=1-6, to=2-6]
-	\arrow["{g \times f + h \times f}"', from=2-4, to=2-6]
-\end{tikzcd}\]
+    \arrow["{g \times f + h \times f}", from=2-4, to=2-6]
+  \end{tikzcd}\]
 \end{proposition}
 \begin{proof}
   We will prove naturality of $dstl$, naturality for $dstr$ is then analogous. We use the fact that $dstl^{-1}$ is an iso and therefore also an epi.

thesis/src/03_partiality-monads.tex

@@ -1,7 +1,7 @@
 \chapter{Partiality Monads}
 Moggi's categorical semantics~\cite{moggi} give us a way to interpret an effectul programming language in a category. For this one needs a (strong) monad $T$ capturing the desired effects, then we can take the elements of $TA$ as denotations for programs of type $A$. The kleisli category of $T$ can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
 
-For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this section is to capture what it means to be a partiality monad and look at two common examples.
+For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples.
 
 \section{Properties of Partiality Monads}
 We will now look at how to express the following non-controversial properties of partiality monads categorically:
@@ -41,7 +41,6 @@ Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which ca
 \begin{definition}[Equational Lifting Monad]
   \label{def:eqlm}
   A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:
-
   % https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ==
   \[\begin{tikzcd}
     TX && {TX \times TX} \\
@@ -54,11 +53,11 @@ Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which ca
   where $\Delta : X \rightarrow X \times X$ is the diagonal morphism.
 \end{definition}
 
-\begin{theorem}
+\begin{theorem}[no proof]
   Let $T$ be an equational lifting monad, then $\mathcal{C}^T$ is a restriction category~\cite{eqlm}.
 \end{theorem}
 
-Definition~\ref{def:eqlm} combines all three properties stated above, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads. For the rest of this chapter we will use these definitions to classify two common examples of monads that are used to model partiality.
+Definition~\ref{def:eqlm} combines all three properties stated above, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads. For the rest of this chapter we will use these definitions to compare two common examples of monads that are used to model partiality.
 
 \section{The Maybe Monad}
 The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X : X \rightarrow X + 1 = i_1$ and $\mu_X : (X + 1) + 1 \rightarrow X + 1 = [ id , i_2 ]$. The monad laws follow easily. This is generally known as the maybe monad and can be viewed as the prototypical example of an equational lifting monad:
@@ -77,17 +76,36 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X : X \rightarro
     = \;&((id \times f) + !) \circ dstl\\
     = \;&((id \times f) + id) \circ (id + !) \circ dstl
   \end{alignat*}
+  the other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness.
 
-  and commutativity:
-
-  and the equational lifting law:
-
+  We are left to check the equational lifting law:
+  % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ==
+  \[\begin{tikzcd}
+    {X+1} &&& {(X+1)\times(X+1)} \\
+    \\
+    &&& {((X+1)\times X) +((X+1)\times 1)} \\
+    \\
+    &&& {((X+1)\times X)+1}
+    \arrow["\Delta", from=1-1, to=1-4]
+    \arrow["dstl", from=1-4, to=3-4]
+    \arrow["{id+\;!}", from=3-4, to=5-4]
+    \arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4]
+  \end{tikzcd}\]
+  By postcomposing $i_1$ and $i_2$ it suffices to show that:
+  \[i_1 \circ \langle i_1 , id \rangle = (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle\]
+  and
+  \[i_2 \;\circ \;! = (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle\]
+  which follow easily by the fact that
+  \[dstl \circ (id \times i_1) = i_1\]
+  and
+  \[dstl \circ (id \times i_2) = i_2\]
 \end{proof}
 
+In a classical setting this monad is therefore sufficient for modelling partiality, but in general it won't be useful for modelling programming languages that have non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modelling possibly non-terminating computations another monad has been developed by Venanzio Capretta.
 
 \section{The Delay Monad}
-Capretta's delay monad is a coinductive datatype whose inhabitants can be viewed as suspended computations. 
-It is defined by the two coinductive constructors $now$ and $later$, where $now$ is for lifting a value to a computation and $later$ intuitively delays a computation by one time unit:
+Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations. 
+It is usually defined by the two coinductive constructors $now$ and $later$, where $now$ is for lifting a value to a computation and $later$ intuitively delays a computation by one time unit:
 
 \[\mprset{fraction={===}}
 \inferrule {x : X} {now\; x : DX}\hskip 2cm
@@ -132,7 +150,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
     \end{equation*}
   \end{itemize}
 \end{corollary}
-\begin{proof}\;\\
+\begin{proof}
   \begin{itemize}
     \item[\ref{D1}] Take $\eta = now$ then $out \circ now = i_1$ follows by definition of $now$.
     \item[\ref{D2}] We define $f^* = \;! \circ i_1$, where $!$ is the unique coalgebra-morphism in this diagram:
@@ -256,17 +274,17 @@ Since $(DX, out)$ is a final coalgebra we get the following proof principle:
         \arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3]
       \end{tikzcd}\]
     \item[\ref{S4}] To show that $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ we take the following coalgebra:
-      % https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMywyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMywxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzIsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMywwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXDshIiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
+    % https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzEsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMiwwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXDshIiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
     \[\begin{tikzcd}
-        {(X \times Y) \times DZ} && {(X \times Y) \times (Z+ DZ)} & {(X\times Y) \times Z + (X \times Y) \times DZ} \\
-        &&& {X \times Y  \times Z + (X \times Y) \times DZ} \\
-        {D(X \times Y \times Z)} &&& {X \times Y \times Z + D(X \times Y \times Z)}
+      {(X \times Y) \times DZ} & {(X \times Y) \times (Z+ DZ)} & {(X\times Y) \times Z + (X \times Y) \times DZ} \\
+      && {X \times Y  \times Z + (X \times Y) \times DZ} \\
+      {D(X \times Y \times Z)} && {X \times Y \times Z + D(X \times Y \times Z)}
       \arrow["{!}", dashed, from=1-1, to=3-1]
-        \arrow["out", from=3-1, to=3-4]
-        \arrow["{id +\;!}"', from=2-4, to=3-4]
-        \arrow["{id \times out}", from=1-1, to=1-3]
-        \arrow["dstl", from=1-3, to=1-4]
-        \arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-4, to=2-4]
+      \arrow["out", from=3-1, to=3-3]
+      \arrow["{id +\;!}"', from=2-3, to=3-3]
+      \arrow["{id \times out}", from=1-1, to=1-2]
+      \arrow["dstl", from=1-2, to=1-3]
+      \arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3]
     \end{tikzcd}\]
   \end{itemize}
 \end{proof}
@@ -314,7 +332,7 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
 \begin{proof}
   Using corollary~\ref{cor:solution} it suffices to show that both $\tau^* \circ \hat{\tau}$ and $\hat{\tau}^* \circ \tau$ are solutions of some guarded morphism $g$.
 
-  Let $w = (dstr + dstr) ∘ dstl ∘ (out \times out)$ and 
+  Let $w = (dstr + dstr) \circ dstl \circ (out \times out)$ and 
   \[g = out^{-1} \circ [ i_1 + D i_1 \circ \hat{\tau} , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\]
   $g$ is trivially guarded by $[ id + D i_1 \circ \hat{\tau} , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$.
 
@@ -336,3 +354,7 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
   \end{tikzcd}\]
   the last step holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$.
 \end{proof}
+
+We have now seen that $\mathbf{D}$ is strong and commutative, ideally we would want it to be an equational lifting monad, but this is not the case since besides modelling non-termination, the delay monad also captures the execution time. This is a result of the too intensional notion of equality that this monad comes with.
+
+In chapter~\ref{chp:setoids} we will see how to remedy this, by taking the quotient of the delay monad where execution time is ignored. This will then give us an equational lifting monad in the category of setoids, but Chapman et al.~\cite{quotienting} have found that this does not work generally without assuming some form of the axiom of countable choice (which crucially holds in the category of setoids).

thesis/src/05_setoids.tex

@@ -1 +1 @@
-\chapter{A Case Study on Setoids}
+\chapter{A Case Study on Setoids}\label{chp:setoids}

thesis/src/titlepage.tex

@@ -20,10 +20,10 @@ Erlangen-Nürnberg%
   \makeatletter
   \@title \\[1cm]
   \makeatother
-\large\bfseries
-An exploration of \ldots % TODo
-\\ and \ldots
-\\[1cm]
+% \large\bfseries
+% An exploration of \ldots % TODo
+% \\ and \ldots
+% \\[1cm]
 \textbf{\large Bachelor Thesis in Computer Science}
 }\\[0.5\baselineskip]
 \rule{\textwidth}{1pt}\par