work on thesis

thesis/bib.bib

@@ -34,16 +34,68 @@
   booktitle = {Lecture Notes in Computer Science}
 }
 
-@article{delay2005,
+@article{delay,
-  doi       = {10.2168/lmcs-1(2:1)2005},
-  url       = {https://doi.org/10.2168%2Flmcs-1%282%3A1%292005},
-  year      = {2005},
-  month     = {jul},
-  publisher = {Centre pour la Communication Scientifique Directe ({CCSD})},
-  volume    = {Volume 1, Issue 2},
   author     = {Venanzio Capretta},
   title      = {General Recursion via Coinductive Types},
-  journal   = {Logical Methods in Computer Science}
+  journal    = {CoRR},
+  volume     = {abs/cs/0505037},
+  year       = {2005},
+  url        = {http://arxiv.org/abs/cs/0505037},
+  eprinttype = {arXiv},
+  eprint     = {cs/0505037},
+  timestamp  = {Mon, 13 Aug 2018 16:46:14 +0200},
+  biburl     = {https://dblp.org/rec/journals/corr/abs-cs-0505037.bib},
+  bibsource  = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{elgotalgebras,
+  author     = {Jir{\'{\i}} Ad{\'{a}}mek and
+                Stefan Milius and
+                Jir{\'{\i}} Velebil},
+  title      = {Elgot Algebras},
+  journal    = {CoRR},
+  volume     = {abs/cs/0609040},
+  year       = {2006},
+  url        = {http://arxiv.org/abs/cs/0609040},
+  eprinttype = {arXiv},
+  eprint     = {cs/0609040},
+  timestamp  = {Mon, 04 Sep 2023 12:29:24 +0200},
+  biburl     = {https://dblp.org/rec/journals/corr/abs-cs-0609040.bib},
+  bibsource  = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{elgotmonad,
+  title     = {Elgot theories: a new perspective on the equational properties of iteration},
+  volume    = {21},
+  doi       = {10.1017/S0960129510000496},
+  number    = {2},
+  journal   = {Mathematical Structures in Computer Science},
+  publisher = {Cambridge University Press},
+  author    = {Jir{\'{\i}} Ad{\'{a}}mek and
+               Stefan Milius and
+               Jir{\'{\i}} Velebil},
+  year      = {2011},
+  pages     = {417–480}
+}
+
+@article{eqlm,
+  author     = {Bucalo, Anna and F\"{u}hrmann, Carsten and Simpson, Alex},
+  title      = {An Equational Notion of Lifting Monad},
+  year       = {2003},
+  issue_date = {15 February 2003},
+  publisher  = {Elsevier Science Publishers Ltd.},
+  address    = {GBR},
+  volume     = {294},
+  number     = {1–2},
+  issn       = {0304-3975},
+  url        = {https://doi.org/10.1016/S0304-3975(01)00243-2},
+  doi        = {10.1016/S0304-3975(01)00243-2},
+  abstract   = {We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus, equational lifting monads precisely capture the equational properties of partial maps as induced by partial map classifiers. The representation theorem also provides a tool for transferring nonequational properties of partial map classifiers to equational lifting monads. It is proved using a direct axiomatization of Kleisli categories of equational lifting monads. This axiomatization is of interest in its own right.},
+  journal    = {Theor. Comput. Sci.},
+  month      = {2},
+  pages      = {31–60},
+  numpages   = {30},
+  keywords   = {premonoidal categories, categories, partiality and partial categories, abstract Kleish, commutative strong monads}
 }
 
 @inproceedings{Lane1971,
@@ -53,29 +105,84 @@
   url    = {https://api.semanticscholar.org/CorpusID:122892655}
 }
 
- @article{moggi,
+@article{moggi,
-  title    = {Notions of computation and monads},
+  author     = {Moggi, Eugenio},
-  journal  = {Information and Computation},
+  title      = {Notions of Computation and Monads},
+  year       = {1991},
+  issue_date = {July 1991},
+  publisher  = {Academic Press, Inc.},
+  address    = {USA},
   volume     = {93},
   number     = {1},
-  pages    = {55-92},
-  year     = {1991},
-  note     = {Selections from 1989 IEEE Symposium on Logic in Computer Science},
   issn       = {0890-5401},
-  doi      = {https://doi.org/10.1016/0890-5401(91)90052-4},
+  url        = {https://doi.org/10.1016/0890-5401(91)90052-4},
-  url      = {https://www.sciencedirect.com/science/article/pii/0890540191900524},
+  doi        = {10.1016/0890-5401(91)90052-4},
-  author   = {Eugenio Moggi},
+  journal    = {Inf. Comput.},
-  abstract = {The λ-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs for a wide range of notions of computation.}
+  month      = {7},
+  pages      = {55–92},
+  numpages   = {38}
 }
 
-@inproceedings{uni-elgot2021,
+@inproceedings{quotienting,
-  doi       = {10.4230/LIPICS.ICALP.2021.131},
+  author    = {Chapman, James and Uustalu, Tarmo and Veltri, Niccol\`{o}},
-  url       = {https://drops.dagstuhl.de/opus/volltexte/2021/14200/},
+  title     = {Quotienting the Delay Monad by Weak Bisimilarity},
-  author    = {Goncharov, Sergey},
+  year      = {2015},
-  keywords  = {Elgot monad, partiality monad, delay monad, restriction category, Theory of computation → Categorical semantics, Theory of computation → Constructive mathematics},
+  isbn      = {9783319251493},
-  language  = {en},
+  publisher = {Springer-Verlag},
-  title     = {Uniform Elgot Iteration in Foundations},
+  address   = {Berlin, Heidelberg},
-  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
+  url       = {https://doi.org/10.1007/978-3-319-25150-9_8},
-  year      = {2021},
+  doi       = {10.1007/978-3-319-25150-9_8},
-  copyright = {Creative Commons Attribution 4.0 International license}
+  abstract  = {The delay datatype was introduced by Capretta [3] as a means to deal with partial functions as in computability theory in Martin-L\"{o}f type theory. It is a monad and it constitutes a constructive alternative to the maybe monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay monad quotiented by weak bisimilarity is still a monad. In this paper, we consider Hofmann's alternative approach [6] of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the semi-classical axiom of countable choice. We have fully formalized our results in the Agda dependently typed programming language.},
+  booktitle = {Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 9399},
+  pages     = {110–125},
+  numpages  = {16}
+}
+
+@article{restriction,
+  author     = {Cockett, J. R. B. and Lack, Stephen},
+  title      = {Restriction Categories I: Categories of Partial Maps},
+  year       = {2002},
+  issue_date = {January},
+  publisher  = {Elsevier Science Publishers Ltd.},
+  address    = {GBR},
+  volume     = {270},
+  number     = {1–2},
+  issn       = {0304-3975},
+  url        = {https://doi.org/10.1016/S0304-3975(00)00382-0},
+  doi        = {10.1016/S0304-3975(00)00382-0},
+  abstract   = {Given a category with a stable system of monics, one can form the corresponding category of partial maps. To each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. This structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. Categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call MCat. The construction of categories of partial maps provides a 2-functor Par:Mcat→Cat. We show that Par can be made into an equivalence of 2-categories between MCat and a 2-category of restriction categories. The underlying ordinary functor Par&r0:Mcat&0 → Ca t0 of the above 2-functor Par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of M-categories and of restriction categories. We also consider the problem of how to turn a formal system of subobjects into an actual system of subobjects. A formal system of subobjects is given by a functor into the category sLat of semilattices. This structure gives rise to a restriction category which, via the above equivalence of 2-categories, gives an M-category. This M-category contains the universal realization of the given formal subobjects as actual subobjects.},
+  journal    = {Theor. Comput. Sci.},
+  month      = {1},
+  pages      = {223–259},
+  numpages   = {37}
+}
+
+@article{uniformelgot,
+  author     = {Sergey Goncharov},
+  title      = {Uniform Elgot Iteration in Foundations},
+  journal    = {CoRR},
+  volume     = {abs/2102.11828},
+  year       = {2021},
+  url        = {https://arxiv.org/abs/2102.11828},
+  eprinttype = {arXiv},
+  eprint     = {2102.11828},
+  timestamp  = {Fri, 26 Feb 2021 14:31:25 +0100},
+  biburl     = {https://dblp.org/rec/journals/corr/abs-2102-11828.bib},
+  bibsource  = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{while,
+  author     = {Sergey Goncharov and
+                Lutz Schr{\"{o}}der and
+                Christoph Rauch},
+  title      = {(Co-)Algebraic Foundations for Effect Handling and Iteration},
+  journal    = {CoRR},
+  volume     = {abs/1405.0854},
+  year       = {2014},
+  url        = {http://arxiv.org/abs/1405.0854},
+  eprinttype = {arXiv},
+  eprint     = {1405.0854},
+  timestamp  = {Mon, 13 Aug 2018 16:47:19 +0200},
+  biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
+  bibsource  = {dblp computer science bibliography, https://dblp.org}
 }

thesis/main.tex

@@ -93,10 +93,15 @@
 \newcommand*{\theauthor}{\@author}
 \makeatother
 
+
 \usepackage{noto-mono}
 %\usepackage{fontspec}
 %\setmonofont{Noto Sans Mono}
 
+\usepackage{mathpartir}
+
+\newcommand{\obj}[1]{\ensuremath{\vert \mathcal{#1} \vert}}
+
 \begin{document}
 \pagestyle{plain}
 \input{src/titlepage}%

thesis/src/00_introduction.tex

@@ -1,2 +1 @@
 \chapter{Introduction}
-citing elgot~\cite{uni-elgot2021}

thesis/src/01_preliminaries.tex

@@ -4,8 +4,8 @@ We assume familiarity with basic categorical notions, in particular categories,
 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{Distributive Categories}
+\section{Distributive and Cartesian Closed Categories}
-Let us first introduce notation for binary (co-)products by giving their defining diagrams:
+Let us first introduce notation for binary (co-)products by giving their usual diagrams:
 
 \begin{figure}[ht]
 % https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
@@ -27,30 +27,26 @@ Let us first introduce notation for binary (co-)products by giving their definin
 \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 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$ on 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$.
 
+Categories with finite products (i.e. binary products and a terminal object) are also called cartesian and categories with finite coproducts (i.e. binary coproducts and an initial object) are called cocartesian.
+
 \begin{definition}[Distributive Category]
   \label{def:distributive}
-  A category $\mathcal{C}$ is called distributive if it has 
+  A cartesian and cocartesian category $\mathcal{C}$ is called distributive if the canonical (left) distributivity morphism morphism $dstl^{-1}$ is an iso:
-  \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}
 
 \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:
+  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}
@@ -65,84 +61,79 @@ We write $1$ for the terminal object together with the unique morphism $! : A \r
   where $swap := \langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A$.
 \end{remark}
 
-\section{Exponential Objects}
+The following is the categorical abstraction of function spaces:
+\begin{definition}[Exponential Object]
+  % TODO introduce notation | C |
+  Let $\mathcal{C}$ be a cartesian category and $X , Y \in \vert \mathcal{C} \vert$.
+  An object $X^Y$ is called an exponential object (of $X$ and $Y$) if there exists an evaluation morphism $eval : X^Y \times Y \rightarrow X$ and for any $f : X \times Y \rightarrow Z$ there exists a morphism $curry\; f : X \rightarrow Z^Y$ that is unique with respect to the following diagram:
+  % https://q.uiver.app/#q=WzAsMyxbMCwwLCJaIFxcdGltZXMgWSJdLFsyLDAsIlheWSBcXHRpbWVzIFkiXSxbMiwyLCJYIl0sWzEsMiwiZXZhbCJdLFswLDEsImN1cnJ5XFw7ZiBcXHRpbWVzIGlkIl0sWzAsMiwiZiIsMl1d
+  \[\begin{tikzcd}
+    {Z \times Y} && {X^Y \times Y} \\
+    \\
+    && X
+    \arrow["eval", from=1-3, to=3-3]
+    \arrow["{curry\;f \times id}", from=1-1, to=1-3]
+    \arrow["f"', from=1-1, to=3-3]
+  \end{tikzcd}\]
+\end{definition}
+
+A cartesian closed category is a cartesian category $\mathcal{C}$ that also has an exponential object $X^Y$ for any $X, Y \in \mathcal{C}$.
+The internal logic of cartesian closed categories is the simply typed $\lambda$-calculus, which makes them a suitable target for interpreting programming languages. But in this thesis we will not assume a cartesian closed category as to be more general.
 
 \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}.
+Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis. Let's recall the basic definitions\cite{Lane1971}\cite{moggi}.
 
-\begin{listing}[H]
+\begin{definition}[Monad]
-  \begin{minted}{agda}
+  A monad on a category $\mathcal{C}$ is a triple $(F, \eta, \mu)$, where $F : \mathcal{C} \rightarrow \mathcal{C}$ is an endofunctor and $\eta : Id \rightarrow F, \mu : F^2 \rightarrow F$ are natural transformations, satisfying the following laws:
-record Monad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
+  \begin{enumerate}
-field
+    % TODO add quantifiers
-  F : Endofunctor C
+    \item $\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X$
-  η : NaturalTransformation idF F
+    \item $\mu_X \circ \eta_{FX} = id_{FX}$
-  μ : NaturalTransformation (F ∘F F) F
+    \item $\mu_X \circ F\eta_X = id_{FX}$
+  \end{enumerate}
+\end{definition}
 
-  open Category C
+For programmers a second equivalent definition is more useful:
-  module F = Functor F
-  module η = NaturalTransformation η
-  module μ = NaturalTransformation μ
 
-  assoc     : ∀ {X : Obj} → μ.η X ∘ F.₁ (μ.η X) ≈ μ.η X ∘ μ.η (F.₀ X)
+\begin{definition}[Kleisli Triple]
-  sym-assoc : ∀ {X : Obj} → μ.η X ∘ μ.η (F.₀ X) ≈ μ.η X ∘ F.₁ (μ.η X)
+  A kleisli triple on a category $\mathcal{C}$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting, where the following laws hold:
-  identityˡ : ∀ {X : Obj} → μ.η X ∘ F.₁ (η.η X) ≈ id
+  \begin{enumerate}
-  identityʳ : ∀ {X : Obj} → μ.η X ∘ η.η (F.₀ X) ≈ id
+    % TODO add quantifiers
-  \end{minted}
+    \item $\eta_X^* = id_{FX}$
-  \caption{Definition of Monad~\cite{agda-categories}}
+    \item $\eta_X \circ f^* = f$
-  \label{lst:monad}
+    \item $f^* \circ g* = (f \circ g^*)^*$ 
-\end{listing}
+  \end{enumerate}
+\end{definition}
 
-(Note: \mintinline{agda}|F.₀| is the functor action on objects, \mintinline{agda}|F.₁| is the functor action on morphisms and \mintinline{agda}|μ.η X| and \mintinline{agda}|η.η X| are the underlying morphisms of the respective natural transformation for \mintinline{agda}|X|)
+In functional programming languages like Haskell the Kleisli lifting $(-)^*$ is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation:
-
-% For programmers a second equivalent definition is more useful:
-For programmers the notion of Kleisli triple is more useful, a Kleisli triple consists of an action on \mintinline{agda}|F| on objects, a family of morphisms \mintinline{agda}|η| and a lifting operator on morphisms, the definition can be seen in listing~\ref{lst:kleisli}.
-
-\begin{listing}[H]
-  \begin{minted}{agda}
-record KleisliTriple {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
-  open Category C
-  field
-    F : Obj → Obj
-    η : ∀ (X : Obj) → X ⇒ F X
-    _* : ∀ {X Y} (f : X ⇒ F Y) → F X ⇒ F Y
-
-    identityˡ : ∀ {X} → (η X)* ≈ id
-    identityʳ : ∀ {X Y} (f : X ⇒ F Y) → f * ∘ (η X) ≈ f
-    assoc : ∀ {X Y Z} (f : Y ⇒ F Z) (g : X ⇒ F Y) 
-      → (f * ∘ g)* ≈ f * ∘ g *
-    sym-assoc : ∀ {X Y Z} (f : Y ⇒ F Z) (g : X ⇒ F Y) 
-      → f * ∘ g * ≈ (f * ∘ g)*
-    *-resp-≈ : ∀ {X Y} {f g : X ⇒ F Y} → f ≈ g → f * ≈ g *
-  \end{minted}
-  \caption{Definition of Kleisli Triple~\cite{agda-categories}}
-  \label{lst:kleisli}
-\end{listing}
-
-In functional programming languages like Haskell the Kleisli lifting (\mintinline{agda}|_*|) is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and \mintinline{agda}|η| is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation:
 \begin{minted}{haskell}
   do y <- f x
      g y
 \end{minted}
 
+% TODO
+\begin{definition}[Kleisli Category]
+\end{definition}
+
 % todo change moggi citation to manes, once I got the original
 \begin{theorem}[\cite{moggi}] The notions of Kleisli triple and monad are equivalent.
 \end{theorem}
 \begin{proof}
-The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out and can be looked up in the appendix. % TODO add reference to appendix
+The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out.
 
 
 ''$\Rightarrow$'':
-Given a Kleisli triple $(F, \eta, \_^*)$, 
+Given a Kleisli triple $(F, \eta, (-)^*)$, 
 we get a monad $(F, \eta, \mu)$ where $F$ is the object mapping of the Kleisli triple together with the functor action $F(f : X \rightarrow Y) = (\eta_Y \circ f)^*$,
 $\eta$ is the morphism family of the Kleisli triple where naturality is easy to show and $\mu$ is a natural transformation defined as $\mu_X = id_{FX}^*$
 
 
 ''$\Leftarrow$'': \\
 Given a monad $(F, \eta, \mu)$,
-we get a Kleisli triple $(F, \eta, \_^*)$ by restricting the functor $F$ on objects, 
+we get a Kleisli triple $(F, \eta, (-)^*)$ by restricting the functor $F$ on objects, 
-forgetting the naturality of $\eta$ and defining $f^* = \mu_Y \circ Ff$ for any $f : X \rightarrow FY$.
+taking the underlying mapping of $\eta$ and defining $f^* = \mu_Y \circ Ff$ for any $f : X \rightarrow FY$.
 \end{proof}
 
 For the rest of this thesis we will use both equivalent notions interchangeably to make definitions easier.
@@ -164,7 +155,7 @@ When modelling partiality with a monad, one would expect the following two progr
 \end{multicols}
 where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
 
-\begin{definition}[Strong Monad~\cite{moggi}] A monad $M$ on a cartesian category $\mathcal{C}$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times MY \rightarrow M(X \times Y)$, satisfying the following conditions:
+\begin{definition}[Strong Monad] A monad $M$ on a cartesian category $\mathcal{C}$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times MY \rightarrow M(X \times Y)$, satisfying the following conditions:
   \begin{enumerate}
   \item $M\pi_2 \circ \tau_{1,X} = \pi_2$
   \item $M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,MZ}$
@@ -174,11 +165,14 @@ where p and q are (partial) computations. This condition can be expressed catego
 \end{definition}
 
 Now we can express the above condition:
-\begin{definition}[Commutative Monad~\cite{moggi}]
+\begin{definition}[Commutative Monad]
-  A strong monad $M$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength $\hat{\tau}_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap$, where $swap = \langle \pi_2 , \pi_1 \rangle$. Concretely if the following equation holds:
+  A strong monad $M$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength $\hat{\tau}_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap$. Concretely if the following equation holds:
   \[
   \tau_{X,Y}^* \circ \hat{\tau}_{X, MY} = \hat{\tau}_{X,Y}^* \circ \tau_{X, MY}
   \]
 \end{definition}
 
 \section{Free Objects}
+
+
+For the rest of this thesis we will work in an ambient distributive category $\mathcal{C}$ that has a stable natural numbers object $\mathbb{N}$.

thesis/src/02_agda-categories.tex

@@ -2,7 +2,10 @@
 
 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.
+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. 
+This section shall serve as a quick introduciton to the library.
+
+% 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:
@@ -22,7 +25,7 @@ Here a \textit{collection} usually is something that behaves set-like, but preve
 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.
+% 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}
@@ -51,3 +54,11 @@ record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
   \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}
+
+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).

thesis/src/03_partiality-monads.tex

@@ -1,4 +1,119 @@
 \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.
+
 \section{Properties of Partiality Monads}
+We will now look at how to express the following non-controversial properties of partiality monads categorically:
+
+\begin{itemize}
+  \item Commutativity of programs
+  \item Programs should be partial
+  \item There should be no other effect besides partiality
+\end{itemize}
+
+The first property of course holds for any commutative monad, the other two are more interesting.
+
+To ensure that programs are partial, we recall the following notion by Cockett and Lack~\cite{restriction}, that ensures that morphisms of a category are partial maps:
+
+\newcommand{\tdom}{\text{dom}\;}
+\begin{definition}[Restriction Structure]
+  A restriction structure on a category $\mathcal{C}$ is a mapping $dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)$ with the following properties:
+  \begin{alignat}{1}
+    f \circ (\tdom f) &= f\\
+    (\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\\
+    \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\\
+    (\tdom h) \circ f &= f \circ \tdom (h \circ f)
+  \end{alignat}
+  for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
+\end{definition}
+Intuitively $\tdom f$ captures the domain of definedness of $f$.
+
+\begin{definition}[Restriction Category]
+  Every category has a trivial restriction structure by taking $dom (f : X \rightarrow Y) = id_X$.
+  A \textit{restriction category} is a category with a non-trivial restriction structure.
+\end{definition}
+
+A partiality monad $T$ should then have the property that $\mathcal{C}^T$ is a restriction category.
+
+Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides partiality:
+
+\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} \\
+    \\
+    && {T(TX \times X)}
+    \arrow["\Delta", from=1-1, to=1-3]
+    \arrow["\tau", from=1-3, to=3-3]
+    \arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
+  \end{tikzcd}\]
+  where $\Delta : X \rightarrow X \times X$ is the diagonal morphism.
+\end{definition}
+
+\begin{theorem}
+  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.
+
 \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:
+
+\begin{theorem} M is an equational lifting monad.
+\end{theorem}
+\begin{proof}
+  We define strength as:
+  \[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1 \]
+
+  naturality of $\tau$ follows by naturality of dstl:
+
+  \begin{alignat*}{1}
+    &(id + !) \circ dstl \circ (id \times (f + id))\\
+    = \;&(id + !) \circ ((id \times f) + (id \times id)) \circ dstl\\
+    = \;&((id \times f) + !) \circ dstl\\
+    = \;&((id \times f) + id) \circ (id + !) \circ dstl
+  \end{alignat*}
+
+  and commutativity:
+
+  and the equational lifting law:
+
+\end{proof}
+
+
 \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:
+
+\[\mprset{fraction={===}}
+\inferrule {x : X} {now\; x : DX}\hskip 2cm
+\inferrule {c : DX} {later\; c : DX}\]
+
+Categorically we get this monad by the final coalgebras $DX = \nu A. X + A$, which we assume to exist. In this section we will show that $\mathbf{D}$ is a strong and commutative monad.
+
+Since $DX$ is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By Lambek's lemma the coalgebra structure $out : DX \rightarrow X + DX$ is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: $out^{-1} = [ now , later ] : X + DX \rightarrow DX$.
+
+\begin{theorem}
+  $\mathbf{D}$ is a monad.
+\end{theorem}
+\begin{proof}
+  We show that $\mathbf{D}$ is a kleisli triple.
+
+  Choose $now : X \rightarrow DX$ and given $f : X \rightarrow DY$ we define $f^* =\; ! \circ i_1$ by:
+
+  % https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzYsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNiwyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBp4oKBICwgaeKCgiDiiJggaeKCgiBdIOKImCAob3V0IOKImCBmKSAsIGnigoIg4oiYIGnigoEgXSDiiJggb3V0ICwgKGlkQyAr4oKBIGnigoIpIOKImCBvdXQgXSJdLFsyLDAsImlfMSJdLFswLDMsIiEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMyw0LCJvdXQiXSxbMSw0LCJGICEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
+  \[\begin{tikzcd}
+    DX \\
+    {DX + DY} &&&&&& {Y + (DX + DY)} \\
+    DY &&&&&& {Y + DY}
+    \arrow["{[ [ [ i_1 , i_2 \circ i_2 ] \circ (out \circ f) , i_2 \circ i_1 ] \circ out , (id +₁ i_2) \circ out ]}", from=2-1, to=2-7]
+    \arrow["{i_1}", from=1-1, to=2-1]
+    \arrow["{!}", dashed, from=2-1, to=3-1]
+    \arrow["out", from=3-1, to=3-7]
+    \arrow["{F !}", dashed, from=2-7, to=3-7]
+  \end{tikzcd}\]
+\end{proof}