🎉🎉 Final commit, small changes after proof reading

thesis/.vscode/ltex.dictionary.en-US.txt

@@ -80,3 +80,5 @@ monadic
 Vatthauer
 minimality
 coequalizer
+refl
+coList

thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt

@@ -57,3 +57,5 @@
 {"rule":"IF_IS","sentence":"^\\QFurthermore, consider the setoid morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Now, by coinduction we can easily follow that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
 {"rule":"IF_IS","sentence":"^\\QConsider, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a setoid morphism that maps every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
 {"rule":"IF_IS","sentence":"^\\QConsider another setoid morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
+{"rule":"DOUBLE_PUNCTUATION","sentence":"^\\QAgda implements a Martin-Löf style dependent type theory with inductive and coinductive types as well as an infinite hierarchy of universes Set_0, Set_1, , where usually Set_0 is abbreviated as Set.\\E$"}
+{"rule":"DOUBLE_PUNCTUATION","sentence":"^\\QAgda implements a Martin-Löf style dependent type theory with inductive and coinductive types as well as an infinite hierarchy of universes Set₀, Set₁, , where usually Set₀ is abbreviated as Set.\\E$"}

thesis/src/01_introduction.tex

@@ -18,16 +18,18 @@ ones = 1 : ones
 Of course evaluation of the term \texttt{reverse ones} will never terminate, hence it is clear that \texttt{reverse} is a partial function.
 Thus, in order to reason about Haskell programs, or generally programs of any programming language offering general recursion, one needs to be able to model partiality as a side effect.
 
-Generally for modelling programming languages there are three prevailing methods. First is the operational approach introduced by Plotkin~\cite{plotkin1975call}, where partial functions are used that map programs to their resulting values, secondly there is the denotational approach by Scott~\cite{scott1993type}, where programming languages are interpreted mathematically, by functions capturing the ``meaning'' of programs.
+Generally for modelling programming languages there are three prevailing methods. First is the operational approach studied by Plotkin~\cite{plotkin1975call}, where partial functions are used that map programs to their resulting values,
+secondly there is the denotational approach by Scott~\cite{scott1993type}, where programming languages are interpreted mathematically, by functions that capture the ``meaning'' of programs.
 For this thesis we will consider the third, categorical approach that has been introduced by Moggi~\cite{moggi}.
 In the categorical approach programs are interpreted in categories, where objects represent types and monads are used to model side effects.
 The goal for this thesis is thus to study monads which are suitable for modeling partiality.
 
 We use the dependently typed programming language Agda~\cite{agda} as a safe and type-checked environment for reasoning in category theory, therefore in \autoref{chp:agda-cat} we start out by quickly showcasing the Agda programming language as well as the category theory library that we will be working with.
 In \autoref{chp:partiality} we will then consider various properties that partiality monads should satisfy and inspect Capretta's delay monad~\cite{delay}, which has been introduced in type theory as a coinductive data type and then studied as a monad in the category of setoids.
-We will examine the delay monad in a general categorical setting, where we prove strength and commutativity of this monad. However, it is not a minimal partiality monad, i.e.\ one that captures no other side effect besides some form of non-termination, since the monad comes with a too intensional notion of equality. In order to achieve minimality one can consider the quotient of the delay monad where a less intensional notion of equality is used. However, it is believed to be impossible to show that the monadic structure is preserved under such a quotient, but the axiom of countable choice has been identified as a sufficient assumption under which the monad structure is preserved in~\cite{quotienting}.
+We will examine the delay monad in a general categorical setting, where we prove strength and commutativity of this monad. However, it is not a minimal partiality monad, i.e.\ one that captures no other side effect besides some form of non-termination, since the monad comes with a too intensional notion of equality. In order to achieve minimality one can consider the quotient of the delay monad where a less intensional notion of equality is used. However, it is believed to be impossible to show that the monadic structure is preserved under such a quotient. In~\cite{quotienting} the axiom of countable choice has been identified as a sufficient assumption under which the monad structure is preserved.
+
 In order to define a partiality monad using no such assumptions, we will draw on the inherent connection between iteration and recursion in \autoref{chp:iteration} to define a suitable partiality monad, by relating to previous research on iteration theories.
 This monad has first been introduced and studied in~\cite{uniformelgot} under weaker assumptions than we use, concretely by weakening the notion of Elgot algebra to the notion of uniform iteration algebra, which uses fewer axioms.
-During mechanization of the results concerning this monad it turned out that under the weaker assumptions, desirable properties like commutativity seem not to be provable, resulting in the adaptation of this monad.
+During mechanization of the results concerning this monad it turned out that under the weaker assumptions, desirable properties like commutativity seem not to be provable, resulting in our adaptation of this monad.
-Lastly, in \autoref{chp:setoids} we will study this partiality monad in the category of setoids, where notably the axiom of countable choice holds.
+Lastly, in \autoref{chp:setoids} we will study this partiality monad in the category of setoids, where notably the axiom of countable choice is provable.
-In this category, the partiality monad will turn out to be equivalent to a certain quotient of the delay monad.
+In this category, the partiality monad turns out to be equivalent to a certain quotient of the delay monad.

thesis/src/02_preliminaries.tex

@@ -2,7 +2,7 @@
 
 We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co)products, terminal and initial objects and special classes of morphisms like isomorphisms (isos), epimorphisms (epis) and monomorphisms (monos). % chktex 36
 In this chapter we will introduce notation that will be used throughout the thesis and also introduce some notions that are crucial to this thesis in more detail.
-We write \(\obj{C}\) for the objects of a category \( \C \), \(id_X\) for the identity morphism on \(X\), \((-) \circ (-)\) for the composition of morphisms and \(\C(X,Y)\) for the set of morphisms between \(X\) and \(Y\).
+We write \(\obj{\C}\) for the objects of a category \( \C \), \(id_X\) for the identity morphism on \(X\), \((-) \circ (-)\) for the composition of morphisms and \(\C(X,Y)\) for the set of morphisms between \(X\) and \(Y\).
 We will also sometimes omit indices of the identity and of natural transformations in favor of readability.
 
 \section{Distributive and Cartesian Closed Categories}
@@ -34,7 +34,7 @@ We write \(1\) for the terminal object together with the unique morphism \(! : A
 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 Cartesian and coCartesian category \(\C \) is called distributive if the canonical (left) distributivity morphism \(dstl^{-1}\) is an iso:
+  A Cartesian and coCartesian category \(\C \) is called distributive if the canonical (left) distributivity morphism \(dstl^{-1}\) is an isomorphism:
   % https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
   \[
     \begin{tikzcd}
@@ -47,7 +47,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
 \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}
@@ -178,9 +178,9 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
   Every exponential object \(X^Y\) satisfies the following properties:
 
   \begin{enumerate}
-    \item The mapping \(curry : \C(X \times Y , Z) \rightarrow \C(X \rightarrow Z^Y)\) is injective.
+    \item The mapping \(curry : \C(X \times Y , Z) \rightarrow \C(X \rightarrow Z^Y)\) is injective,
-    \item \(curry(eval \circ (f \times id)) = f\) for any \(f : X \times Y \rightarrow Z\)
+    \item \(curry(eval \circ (f \times id)) = f\) for any \(f : X \times Y \rightarrow Z\),
-    \item \(curry\;f \circ g = curry(f \circ (g \times id))\) for any \(f : X \times Y \rightarrow Z, g : A \rightarrow X\)
+    \item \(curry\;f \circ g = curry(f \circ (g \times id))\) for any \(f : X \times Y \rightarrow Z, g : A \rightarrow X\).
   \end{enumerate}
 \end{proposition}
 \begin{proof}
@@ -195,7 +195,8 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
 \end{proof}
 
 A Cartesian closed category is a Cartesian category \(\C \) that also has an exponential object \(X^Y\) for any \(X, Y \in \obj{\C} \).
-The internal logic of Cartesian closed categories is the simply typed \(\lambda \)-calculus, which makes them a suitable environment for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however need not be Cartesian closed as to be more general.
+The internal logic of Cartesian closed categories is the simply typed \(\lambda \)-calculus, which makes them a suitable environment for interpreting programming languages.
+For the rest of this thesis we will work in an ambient distributive category \(\C\), that however need not be Cartesian closed as to be more general.
 
 \section{F-Coalgebras}
 Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tuples \((X, \alpha : FX \rightarrow X)\) consisting of an object of \(\C \) and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modeling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras; let us formally introduce them now.
@@ -205,7 +206,7 @@ Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tup
 \end{definition}
 
 \begin{definition}[Coalgebra Morphisms]\label{def:coalgmorph}
-  Let \((X \in \obj{\C} , \alpha : X \rightarrow FX)\) and \((Y \in \obj{\C} , \beta : Y \rightarrow FY)\) be two coalgebras. A morphism between these coalgebras is a morphism \(f : X \rightarrow Y\) such that the following diagram commutes:
+  Let \((X, \alpha : X \rightarrow FX)\) and \((Y, \beta : Y \rightarrow FY)\) be two coalgebras. A morphism between these coalgebras is a morphism \(f : X \rightarrow Y\) such that the following diagram commutes:
   % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMiwiWSJdLFsyLDAsIkZYIl0sWzIsMiwiRlkiXSxbMSwzLCJcXGJldGEiXSxbMCwyLCJcXGFscGhhIl0sWzAsMSwiZiIsMl0sWzIsMywiRmYiXV0=
   \[
     \begin{tikzcd}[ampersand replacement=\&]
@@ -221,7 +222,7 @@ Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tup
 
 \end{definition}
 
-Coalgebras together with their morphisms form a category that we call \(\coalgs{F}\).
+Coalgebras on a given functor together with their morphisms form a category that we call \(\coalgs{F}\).
 
 \begin{proposition}
   \(\coalgs{F}\) is a category.
@@ -239,7 +240,9 @@ Coalgebras together with their morphisms form a category that we call \(\coalgs{
   \end{alignat*}
 \end{proof}
 
-The terminal object of \(\coalgs{F}\) is sometimes called \textit{final coalgebra}, we will however call it the \textit{terminal coalgebra} for consistency with initial F-algebras. Similarly to initial F-algebras, the final coalgebra can be used for modeling the semantics of coinductive data types where terminality of the coalgebra yields corecursion as a definitional principle and coinduction as a proof principle. Let us make the universal property of terminal coalgebras concrete:
+The terminal object of \(\coalgs{F}\) is sometimes called \textit{final coalgebra}, we will however call it the \textit{terminal coalgebra} for consistency with initial F-algebras.
+Similarly to initial F-algebras, the final coalgebra can be used for modeling the semantics of coinductive data types where terminality of the coalgebra yields corecursion as a definitional principle and coinduction as a proof principle.
+Let us make the universal property of terminal coalgebras concrete.
 
 \begin{definition}[Terminal Coalgebra]
   A coalgebra \((T, t : T \rightarrow FT)\) is called a terminal coalgebra if for any other coalgebra \((X, \alpha : X \rightarrow FX)\) there exists a unique morphism \(\coalg{\alpha} : X \rightarrow T\) satisfying:
@@ -256,6 +259,7 @@ The terminal object of \(\coalgs{F}\) is sometimes called \textit{final coalgebr
       \arrow["{F\coalg{\alpha}}", from=1-3, to=3-3]
     \end{tikzcd}
   \]
+  We use the common notation \(\nu F\) to denote the terminal coalgebra for \(F\) (if it exists).
 \end{definition}
 
 We will discuss the concrete form that induction and coinduction take in a type theory in \autoref{chp:agda-cat}. Let us now reiterate a famous Lemma concerning terminal F-coalgebras.
@@ -302,7 +306,7 @@ We will discuss the concrete form that induction and coinduction take in a type
 % \end{proof}
 
 \section{Monads}
-Monads are widely known in functional programming as a means for modeling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
+Monads are widely known in functional programming as a means for modeling effects in ``pure'' languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
 
 \begin{definition}[Monad]
   A monad \(\mathbf{T}\) on a category \(\C \) is a triple \((T, \eta, \mu)\), where \(T : \C \rightarrow \C \) is an endofunctor and \(\eta : Id \rightarrow T, \mu : TT \rightarrow T\) are natural transformations, satisfying the following laws:
@@ -334,7 +338,7 @@ Monads are widely known in functional programming as a means for modeling effect
 \end{definition}
 
 \begin{definition}[Monad Morphism]\label{def:monadmorphism}
-  A morphism between monads \((S : \C \rightarrow \C, \eta^S, \mu^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T)\) is a natural transformation \(\alpha : S \rightarrow T\) between the underlying functors satisfying:
+  A morphism between monads \((S : \C \rightarrow \C, \eta^S, \mu^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T)\) is a natural transformation \(\alpha : S \rightarrow T\) between the underlying functors such that the following diagrams commute.
   % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFszLDAsIlNTWCJdLFs1LDAsIlNUWCJdLFszLDEsIlNYIl0sWzcsMCwiVFRYIl0sWzcsMSwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
   \[
     \begin{tikzcd}[ampersand replacement=\&]
@@ -358,7 +362,7 @@ This yields a category of monads on a given category \(\C\) that we call \(\mona
   \(\monads{\C}\) is a category.
 \end{proposition}
 \begin{proof}
-  The identity morphism of \(\monads{\C}\) is the identity natural transformation \(Id : F \rightarrow F\) which trivially respects the monad unit and multiplication. Composition of monad morphisms is composition of the underlying natural transformation, the diagrams then also follow easily.
+  The identity morphism of \(\monads{\C}\) is the identity natural transformation \(Id : F \rightarrow F\), which trivially respects the monad unit and multiplication. Composition of monad morphisms is composition of the underlying natural transformation, the diagrams then also follow easily.
 \end{proof}
 
 Monads can also be specified in a second equivalent way that is better suited to describe computation.
@@ -384,7 +388,7 @@ This yields the category of programs for a Kleisli triple that is called the Kle
   Given a monad \(T\) on a category \(\C \), the Kleisli category \(\C^T\) is defined as:
   \begin{itemize}
     \item \(\vert \C^T \vert = \obj{C}\)
-    \item \(\mathcal{C^T}(X, Y) = \C(X, TY)\)
+    \item \(\C^T(X, Y) = \C(X, TY)\)
     \item Composition of programs is Kleisli composition.
     \item The identity morphisms are the unit morphisms of \(T\), \(id_X = \eta_X : X \rightarrow TX\)
   \end{itemize}
@@ -398,13 +402,13 @@ This yields the category of programs for a Kleisli triple that is called the Kle
 
   ``\(\Rightarrow \)'':
   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)}^*\),
+  we obtain 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 obtain a Kleisli triple \((F, \eta, {(-)}^*)\) by restricting the functor \(F\) on objects,
   taking the underlying mapping of \(\eta \) and defining \(f^* = \mu_Y \circ Ff\) for any \(f : X \rightarrow FY\).
 \end{proof}
 
@@ -418,8 +422,8 @@ Consider the following program in do-notation
 \end{minted}
 where \(g : X \rightarrow TY\) and \(f : X \times Y \rightarrow TZ\) are programs and \(\mathbf{T}\) is a monad. Kleisli composition does not suffice for interpreting this program, we will get stuck at
 \[X \overset{\langle id , g \rangle}{\longrightarrow} X \times TY \overset{?}{\longrightarrow} T(X \times Y) \overset{f^*}{\longrightarrow} TZ. \]
-Which motivates the following notion.
 
+Instead, one needs the following stronger notion of monad.
 \begin{definition}[Strong Monad] A monad \((T, \eta, \mu)\) on a Cartesian category \(\C \) is called strong if there exists a natural transformation \(\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)\) that satisfies the following conditions:
   \begin{alignat*}{2}
      & T\pi_2 \circ \tau_{1,X}                     &  & = \pi_2 \tag*{(S1)}\label{S1}                                                                     \\
@@ -431,7 +435,7 @@ Which motivates the following notion.
 \end{definition}
 
 \begin{definition}[Strong Monad Morphism]\label{def:strongmonadmorphism}
-  A morphism between two strong monads \((S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)\) is a morphism between monads as in \autoref{def:monadmorphism} that additionally satisfies:
+  A morphism between two strong monads \((S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)\) is a morphism between monads as in \autoref{def:monadmorphism} where additionally the following diagram commutes.
   % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgU1kiXSxbMCwyLCJTKFggXFx0aW1lcyBZKSJdLFsyLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIFRZIl0sWzAsMSwiXFx0YXVeUyJdLFsxLDIsIlxcYWxwaGEiXSxbMCwzLCJpZCBcXHRpbWVzIFxcYWxwaGEiXSxbMywyLCJcXHRhdV5UIiwyXV0=
   \[
     \begin{tikzcd}[ampersand replacement=\&]
@@ -462,7 +466,7 @@ Let us now consider the following two programs
        return (x, y)
   \end{minted}
 \end{multicols}
-Where p and q are computations of some monad. A monad where such programs are equal is called commutative.
+Where \(p : TX\) and \(q : TY\) are computations of some monad \(T\). A monad where these programs are equal, is called commutative.
 
 \begin{definition}[Commutative Monad]
   A strong monad \(\mathbf{T}\) is called commutative if the (right) strength \(\tau \) commutes with the induced left strength

thesis/src/03_agda-categories.tex

@@ -6,10 +6,12 @@ In this thesis we will work with the dependently typed programming language Agda
 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\).
+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 \texttt{Set₀, Set₁, \ldots}, where usually \texttt{Set₀} is abbreviated as \texttt{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}.
+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 the inhabitants of 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.
+These are standard notions and need no further introduction.
-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:
+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 \texttt{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
@@ -17,7 +19,8 @@ Dually to inductive types that are defined by their \emph{constructors}, coinduc
       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}.
+i.e.\ the type of streams over \texttt{A} is defined by the two destructors \texttt{head : Stream A → A} and \texttt{tail : Stream A → Stream A} that return the head and the tail of the stream respectively. % chktex 26
+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
@@ -31,21 +34,22 @@ Let us introduce the usual notion of stream bisimilarity. Given two streams, the
       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.
+In this definition \texttt{\_≡\_} is the built-in propositional equality in Agda with the single constructor \texttt{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.
+Where in the coinductive step we were able to assume that \texttt{repeat a ≈ tail(repeat a)} already holds and showed that thus \texttt{tail(repeat a) ≈ tail(tail(repeat a))} holds. % chktex 36
 
-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
+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 \texttt{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:
+That is, the coinductive type \texttt{coList} is defined by the constructors \texttt{nil} and \texttt{\_∷\_}.
+Agda does implement a second way of defining 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 \texttt{coList} as two mutual types, one inductive and the other coinductive:
 \begin{minted}{agda}
 mutual
   data coList (A : Set) : Set where
@@ -55,7 +59,7 @@ mutual
     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
+Unfortunately, this does add the overhead of having to define functions on \texttt{coList} as mutual recursive functions, e.g.\ the \texttt{repeat} function from before can be defined as
 \begin{minted}{agda}
   mutual
     repeat  : {A : Set} (a : A) → coList A
@@ -63,7 +67,7 @@ Unfortunately, this does add the overhead of having to define functions on \(coL
     repeat a = a ∷ repeat′ a
     force (repeat′ a) = repeat a
 \end{minted}
-or more succinctly using an anonymous \(\lambda\)-function
+or more succinctly using a \(\lambda\)-function
 \begin{minted}{agda}
   repeat : {A : Set} (a : A) → coList A
   repeat a = a ∷ λ { .force → repeat a }
@@ -85,17 +89,19 @@ Let us now consider how to implement category theory in Agda. The usual textbook
   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.
+Here \emph{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.
+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 key differences to the definition above are firstly that instead of talking about collections, Agda's infinite \texttt{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.
+This 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.
+A 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.
+Furthermore, the types of morphisms are equipped with an equivalence relation \texttt{\_≈\_}, 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}.
+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 \emph{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.
+As a consequence of using a custom equality relation, proofs like \texttt{∘-resp-≈} are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. In the thesis we will omit such proofs, but they are contained in our formalization.
+Lastly, the designers of agda-categories also include symmetric proofs like \texttt{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 \texttt{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}

thesis/src/04_partiality-monads.tex

@@ -19,14 +19,14 @@ To ensure that programs are partial, we recall the following notion by Cockett a
 
 \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:
+  A restriction structure on a category \(\C\) is a mapping \(dom : \C(X, Y) \rightarrow \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\).
+  for any \(X, Y, Z \in \obj{\C}, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z\).
 \end{definition}
 
 The morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
@@ -62,7 +62,7 @@ Lastly, we also recall the following notion by Bucalo et al.~\cite{eqlm} which c
       \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.
+  where \(\Delta_X : X \rightarrow X \times X\) is the diagonal morphism.
 \end{definition}
 
 To make the equational lifting property more comprehensible we can alternatively state it using do-notation. The equational lifting property states that the following programs must be equal:
@@ -82,21 +82,24 @@ To make the equational lifting property more comprehensible we can alternatively
 That is, if some computation \(p : TX\) terminates with the result \(x : X\), then \(p = return\;x\) must hold afterwards. This of course implies that running \(p\) multiple times yields the same result as running \(p\) once.
 
 \begin{proposition}[\cite{eqlm}]\label{prop:liftingkleisli}
-  If \(T\) is an equational lifting monad the Kleisli category \(\mathcal{C}^T\) is a restriction category.
+  If \(T\) is an equational lifting monad the Kleisli category \(\C^T\) is a restriction category.
 \end{proposition}
 
-Definition~\ref{def:eqlm} combines all three properties stated at the beginning of the section, 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 monads that are commonly used to model partiality.
+Definition~\ref{def:eqlm} combines all three properties stated at the beginning of the section, 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 monads that are commonly used to model partiality.
 
 \section{The Maybe Monad}
-The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \rightarrow X + 1\) and \(\mu_X = [ id , i_2 ] : (X + 1) + 1 \rightarrow X + 1\). The monad laws follow easily. This is generally known as the maybe monad and can be viewed as the canonical example of an equational lifting monad:
+The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \rightarrow X + 1\) and \(\mu_X = [ id , i_2 ] : (X + 1) + 1 \rightarrow X + 1\).
+The monad laws follow easily.
+This is generally known as the maybe monad and can be viewed as the canonical example of an equational lifting monad.
 
 \begin{theorem} M is an equational lifting monad.
 \end{theorem}
 \begin{proof}
-  We define strength as:
+  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 \]
+  \[ \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\):
+  Naturality of \(\tau \) follows by naturality of \(dstl\)
 
   \begin{alignat*}{1}
          & (id + !) \circ dstl \circ (id \times (f + id))             \\
@@ -107,7 +110,7 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
 
   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.
 
-  We are left to check the equational lifting law:
+  We are thus left to check the equational lifting law:
   % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ==
   \[
     \begin{tikzcd}
@@ -140,14 +143,16 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
   \end{alignat*}
 \end{proof}
 
-In the setting of classical mathematics this monad is therefore sufficient for modeling partiality, but in general it will not be useful for modeling  non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modeling possibly non-terminating computations another monad has been developed by Capretta~\cite{delay}.
+In the setting of classical mathematics this monad is therefore sufficient for modeling partiality, but in general it will not be useful for modeling  non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modeling possibly non-terminating computations another monad has been introduced by Capretta~\cite{delay}.
 
 \section{The Delay Monad}
 Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
-This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} for a type theoretical study of this monad.
+This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\), where \(now\) lifts a value inside a computation and \(later\) intuitively delays a computation by one time unit.
-Categorically we obtain the delay monad by the final F-coalgebras \(DX = \nu A. X + A\), which we assume to exist. In this section we will show that these final F-coalgebras indeed yield a monad that is strong and commutative.
+See \autoref{chp:setoids} for a type theoretical study of this monad.
+Categorically we obtain the delay monad by the terminal coalgebras \(DX = \nu A. X + A\), which we assume to exist.
+In this section we will show that these terminal coalgebras indeed yield a monad that is strong and commutative.
 
-Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} 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\).
+Since \(DX\) is defined as a terminal coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} 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{lemma}~\label{lem:delay}
   The following conditions hold:
@@ -156,7 +161,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
           \begin{equation*}
             out \circ now = i_1 \qquad\qquad\qquad out \circ later = i_2 \tag*{(D1)}\label{D1}
           \end{equation*}
-    \item For any \(f : X \rightarrow DY\) there exists a unique morphism \(f^* : DX \rightarrow DY\) satisfying:
+    \item For any \(f : X \rightarrow DY\) there exists a unique morphism \(f^* : DX \rightarrow DY\) such that the following commutes.
           \begin{equation*}
             % https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIlggKyBEWCJdLFswLDEsIkRZIl0sWzMsMSwiWSArIERZIl0sWzAsMSwib3V0Il0sWzAsMiwiZl4qIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywib3V0Il0sWzEsMywiWyBvdXQgXFxjaXJjIGYgLCBpXzIgXFxjaXJjIGZeKiBdIl1d
             \begin{tikzcd}
@@ -169,7 +174,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
             \end{tikzcd}
             \tag*{(D2)}\label{D2}
           \end{equation*}
-    \item There exists a unique morphism \(\tau : X \times DY \rightarrow D(X \times Y)\) satisfying:
+    \item There exists a unique morphism \(\tau : X \times DY \rightarrow D(X \times Y)\) such that:
           \begin{equation*}
             % https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
             \begin{tikzcd}[ampersand replacement=\&]
@@ -186,9 +191,9 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
   \end{itemize}
 \end{lemma}
 \begin{proof}
-  We will make use of the fact that every \(DX\) is a final coalgebra:
+  We will make use of the fact that every \(DX\) is a terminal coalgebra:
   \begin{itemize}
-    \item[\ref{D1}] These follow by definition:
+    \item[\ref{D1}] These follow by definition of \(now\) and \(later\):
           \begin{alignat*}{3}
              & out \circ now &  & = out \circ out^{-1} \circ i_1 & = i_1
             \\&out \circ later &&= out \circ out^{-1} \circ i_2 &= i_2
@@ -209,7 +214,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
             \end{tikzcd}
           \]
 
-          Note that \(\coalg{\alpha} \circ i_2 = id : (DY, out) \rightarrow (DY, out)\), by uniqueness of the identity morphism and the fact that \(\coalg{\alpha} \circ i_2\) is a coalgebra morphism:
+          Note that \(\coalg{\alpha} \circ i_2 = id : (DY, out) \rightarrow (DY, out)\), by uniqueness of the identity morphism and the fact that \(\coalg{\alpha} \circ i_2\) is a coalgebra morphism, since
           \begin{alignat*}{1}
              & out \circ \coalg{\alpha} \circ i_2
             \\=\;&(id+\coalg{\alpha}) \circ \alpha \circ i_2
@@ -227,7 +232,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
           \end{alignat*}
 
           We are left to check uniqueness of \(f^*\). Let \(g : DX \rightarrow DY\) and \(out \circ g = [ out \circ f , i_2 \circ g ] \circ out\).
-          Note that \([ g , id ] : DX + DY \rightarrow DY\) is a coalgebra morphism:
+          Note that \([ g , id ] : DX + DY \rightarrow DY\) is a coalgebra morphism, since
           \begin{alignat*}{1}
              & out \circ [ g , id ]
             \\=\;&[ out \circ g , out ]
@@ -271,7 +276,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
             \\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out.\tag*{\ref{D1}}
           \end{alignat*}
     \item[3.]
-          These equations follow by monicity of \(out\):
+          This equational chain follows by monicity of \(out\):
           \begin{alignat*}{1}
              & out \circ {(later \circ f)}^*
             \\=\;&[ out \circ later \circ f , i_2 \circ {(later \circ f)}^*] \circ out\tag*{\ref{D2}}
@@ -287,9 +292,9 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
   Thus, the postulated properties have been proven.
 \end{proof}
 
-\begin{theorem}
+\begin{lemma}
-  \(\mathbf{D} = (D, now, {(-)}^*)\) is a Kleisli triple.
+  \(\mathbf{D} := (D, now, {(-)}^*)\) is a Kleisli triple.
-\end{theorem}
+\end{lemma}
 \begin{proof}
   We will now use the properties proven in \autoref{lem:delay} to prove the Kleisli triple laws:
   \begin{itemize}
@@ -314,7 +319,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
   This concludes the proof.
 \end{proof}
 
-Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}}\) yields the following proof principle:
+Terminality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}}\) yields the following proof principle.
 \begin{remark}[Proof by coinduction]~\label{rem:coinduction}
   Given two morphisms \(f, g : X \rightarrow DY\). To show that \(f = g\) it suffices to show that there exists a coalgebra structure \(\alpha : X \rightarrow Y + X\) such that the following diagrams commute:
   % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCJdXQ==
@@ -335,9 +340,9 @@ Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}
   Uniqueness of the coalgebra morphism \(\coalg{\alpha} : (X, \alpha) \rightarrow (DY, out)\) then results in \(f = g\).
 \end{remark}
 
-\begin{theorem}
+\begin{lemma}
   \(\mathbf{D}\) is a strong monad.
-\end{theorem}
+\end{lemma}
 \begin{proof}
   Most of the following proofs are done via coinduction (Remark~\ref{rem:coinduction}). We will only give the requisite coalgebra structure. The proofs that the diagrams commute can be looked up in the Agda formalization.
 
@@ -423,10 +428,10 @@ Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}
   Thus, it has been shown that \(\mathbf{D}\) is a strong monad.
 \end{proof}
 
-To prove that \(\mathbf{D}\) is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
+To prove that \(\mathbf{D}\) is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form.
 
 \begin{definition}
-  We call a morphism \(g : X \rightarrow D (Y + X)\) \textit{guarded} if there exists an \(h : X \rightarrow Y + D(Y+X)\) such that the following diagram commutes:
+  We call a morphism \(g : X \rightarrow D (Y + X)\) \textit{guarded} if there exists a morphism \(h : X \rightarrow Y + D(Y+X)\) such that the following diagram commutes:
   % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
   \[
     \begin{tikzcd}[ampersand replacement=\&]
@@ -510,17 +515,16 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
 \begin{proof}
   Using \autoref{cor:solution} it suffices to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of some guarded morphism \(g\).
 
-  Let \(w = (dstr + dstr) \circ dstl \circ (out \times out)\) and take
+  Let \(w := (dstr + dstr) \circ dstl \circ (out \times out)\) and take
-  \[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w.\]
+  \[g := out^{-1} \circ [ i_1 + D i_1 \circ \sigma , 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 \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\).
+  Note that \(g\) is trivially guarded by \([ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\).
-
+  It thus suffices to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider
-  We are left to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider
 
   \[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = {[ now , \tau^* \circ \sigma]}^* \circ g, \]
   and
   \[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = {[ now , \sigma^* \circ \tau]}^* \circ g. \]
 
-  The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\)
+  The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\):
   \begin{alignat*}{1}
      & out \circ {[ now , f ]}^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w
     \\=\; & [ out \circ [ now , f ] , i_2 \circ {[ now , f ]}^* ] \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}}
@@ -530,9 +534,7 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
     \\=\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w.
   \end{alignat*}
 
-  Let us now check the first step in the equation for \(\sigma^* \circ \tau \), the same step for \(\tau^* \circ \sigma \) is then symmetric.
+  Let us now check the first step in the equation for \(\sigma^* \circ \tau \), the same step for \(\tau^* \circ \sigma \) is then symmetric. Again, we proceed by monicity of \(out\), which yields
-
-  Again, we proceed by monicity of \(out\), which yields
   \begin{alignat*}{1}
      & out \circ \sigma^* \circ \tau
     \\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
@@ -553,7 +555,6 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
   where
   \[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\]
   indeed follows by epicness of \(dstr^{-1}\):
-
   \begin{alignat*}{1}
      & Ddstr \circ \tau \circ dstr^{-1}
     \\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ]
@@ -568,4 +569,4 @@ This is a result of the too intensional notion of equality that this monad comes
 In \autoref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored.
 This will then yield an equational lifting monad on the category of setoids.
 However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient.
-Chapman et al.\ have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of \(\mathbf{D}\).
+Chapman et al.~\cite{quotienting} have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of \(\mathbf{D}\).

thesis/src/05_iteration.tex

@@ -6,7 +6,7 @@ Recall the following notion from~\cite{elgotalgebras}, previously called \emph{c
 \begin{definition}[Guarded Elgot Algebra]
   \  Given a functor \(H : \C \rightarrow \C\), a \emph{(H-)guarded Elgot algebra} consists of: % chktex 36
   \begin{itemize}
-    \item An object \(A : \obj{\C}\),
+    \item An object \(A \in \obj{\C}\),
     \item a H-algebra structure \(a : H\;A \rightarrow A\),
     \item and for every \(f : X \rightarrow A + HX\) an \emph{iteration} \(f^\sharp : X \rightarrow A\), satisfying the following axioms:
           \begin{itemize}
@@ -27,7 +27,7 @@ The previous intuition gives rise to the following simpler definition that has b
 \begin{definition}[Elgot Algebra]
   A \emph{(unguarded) Elgot Algebra}~\cite{uniformelgot} consists of:
   \begin{itemize}
-    \item An object \(A : \obj{\C}\),
+    \item An object \(A \in \obj{\C}\),
     \item and for every \(f : X \rightarrow A + X\) an \emph{iteration} \(f^\sharp : X \rightarrow A\), satisfying the following axioms:
           \begin{itemize}
             \item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: \(f^\sharp = [ id , f ^\sharp ] \circ f\)
@@ -44,7 +44,7 @@ Note that the \ref{law:uniformity} axiom requires an identity to be proven, befo
 However, we will omit these proofs in most parts of the thesis, since they mostly follow by simple rewriting on (co)products, the full proofs can be looked up in the accompanying formalization. % chktex 36
 
 Now, in this setting the simpler \ref{law:folding} axiom replaces the sophisticated \ref{law:guardedcompositionality} axiom. % chktex 2
-Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the \ref{law:folding} and \ref{law:guardedcompositionality} axioms are equivalent, which is partly illustrated by the following Lemma. % chktex 2
+Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the \ref{law:folding} and \ref{law:guardedcompositionality} axioms are equivalent~\cite{uniformelgot}, which is partly illustrated by the following Lemma. % chktex 2
 
 \begin{lemma}
   Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional axioms
@@ -73,7 +73,7 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
             \\=\;&{(f^\sharp + h)}^\sharp \circ i_2 \tag{\ref{law:fixpoint}}
             \\=\;&{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2. \tag{\ref{law:folding}}
           \end{alignat*}
-          Using \ref{law:folding'}, we are left to show that % chktex 2
+          Using \ref{law:folding'}, it suffices to show that % chktex 2
           \[{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2 = {([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2.\]
           Indeed,
           \begin{alignat*}{1}
@@ -85,11 +85,11 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
             \\=\;&{([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2.\tag{\ref{law:uniformity}}
           \end{alignat*}
 
-    \item \ref{law:stutter}: Note that % chktex 2
+    \item \ref{law:stutter}: Let us first establish % chktex 2
           \begin{equation}
             [ h , h ] = {(h + i_1)}^\sharp, \tag{*}\label{stutter-helper}
           \end{equation}
-          since
+          which follows by
           \begin{alignat*}{1}
              & {(h + i_1)}^\sharp
             \\=\;&[ id , {(h + i_1)}^\sharp ] \circ (h + i_1) \tag{\ref{law:fixpoint}}
@@ -107,6 +107,7 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
             \\=\;&{[ i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] \circ f ]}^\sharp \circ i_2. \tag{\ref{law:uniformity}}
           \end{alignat*}
     \item \ref{law:diamond}: Let \(h = [ i_1 \circ i_1 , i_2 + id ] \circ f\) and \(g = (id + \Delta) \circ f\). %chktex 2
+
           First, note that
           \begin{equation*}
             [ id , g^\sharp ] = {[ i_1 , (id + i_2) \circ g ]}^\sharp, \tag{\(∗\)}\label{diamond-helper}
@@ -120,14 +121,11 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
             \\=\;&{[ i_1 , (id + i_2) \circ g ]}^\sharp. \tag{\ref{law:fixpoint}}
           \end{alignat*}
 
-          Furthermore, by \ref{law:folding}: % chktex 2
-          \[{[ (id + i_1) \circ [ i_1 , (id + i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2 = {({[i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2.\]
-
           It thus suffices to show that,
           \begin{alignat*}{1}
              & g^\sharp
             \\=\;&{[ (id + i_1) \circ [ i_1 , (id + i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2
-            \\=\;&{({[i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2
+            \\=\;&{({[i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2\tag{\ref{law:folding}}
             \\=\;&{([ i_1 , g^\sharp + id] \circ f)}^\sharp.
           \end{alignat*}
           Indeed,
@@ -206,7 +204,6 @@ Products and exponentials of Elgot algebras can be formed in a canonical way, wh
 \begin{lemma}\label{lem:elgotalgscart}
   If \(\C\) is a Cartesian category, so is \(\elgotalgs{\C}\).
 \end{lemma}
-
 \begin{proof}
   Let \(1\) be the terminal object of \(\C \). Given \(f : X \rightarrow 1 + X\) we define the iteration \(f^\sharp =\;! : X \rightarrow 1\) as the unique morphism into the terminal object. The Elgot algebra laws follow instantly by uniqueness of \(!\) and \((1 , !)\) is the terminal Elgot algebra since for every Elgot algebra \(A\) the morphism \(! : A \rightarrow 1\) extends to a morphism between Elgot algebras by uniqueness. % chktex 40
 
@@ -486,11 +483,7 @@ A symmetrical variant of the previous definition is sometimes useful.
   Finally, let us check uniqueness of \(\rs{f} = \ls{f \circ swap} \circ swap\). Let \(g : X \times KY \rightarrow A\) be right iteration preserving with \(g \circ (id \times \eta) = f\). To show that \(g = \ls{f \circ swap} \circ swap\), by uniqueness of \(\ls{f \circ swap}\) it suffices to show that \(g \circ swap\) satisfies \(g \circ swap \circ (\eta \times id) = f \circ swap\) and is left iteration preserving.
 
   Indeed,
-  \begin{alignat*}{1}
+  \[ g \circ swap \circ (\eta \times id) = g \circ (id \times \eta) \circ swap = f \circ swap\]
-     & g \circ swap \circ (\eta \times id)
-    \\=\;&g \circ (id \times \eta) \circ swap
-    \\=\;&f \circ swap,
-  \end{alignat*}
   and
   \begin{alignat*}{1}
      & g \circ swap \circ (h^\sharp \times id)
@@ -511,8 +504,6 @@ A symmetrical variant of the previous definition is sometimes useful.
   This concludes one direction of the proof, the other direction follows symmetrically.
 \end{proof}
 
-In a less general setting stability would indeed follow automatically.
-
 \begin{lemma}\label{thm:stability}
   In a Cartesian closed category every free Elgot algebra is stable.
 \end{lemma}
@@ -561,14 +552,12 @@ In a less general setting stability would indeed follow automatically.
   \begin{alignat*}{1}
      & curry\;g \circ \eta
     \\=\;&curry(g \circ (\eta \times id))
-    \\=\;&curry\;f
+    \\=\;&curry\;f.
   \end{alignat*}
-
   Which completes the proof.
 \end{proof}
 
 For the rest of this chapter we will assume every \(KX\) to exist and be stable. Under these assumptions we show that \(\mathbf{K}\) is an equational lifting monad and in fact the initial strong pre-Elgot monad.
-
 Let us first introduce a proof principle similar to the one introduced in \autoref{rem:coinduction}.
 \begin{remark}[Proof by right-stability]~\label{rem:proofbystability}
   Given two morphisms \(g, h : X \times KY \rightarrow A\) where \(X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}\). To show that \(g = h\), it suffices to show that \(g\) and \(h\) are right iteration preserving and there exists a morphism \(f : X \times Y \rightarrow A\) such that
@@ -609,7 +598,6 @@ Of course there is also a symmetric version of this.
 \end{lemma}
 \begin{proof}
   We define strength as \(\tau = \rs{(\eta : X \times Y \rightarrow K(X \times Y))} : X \times KY \rightarrow K(X \times Y)\). Note that by definition \(\tau\) is right iteration preserving and \(\tau \circ (id \times \eta) = \eta\).
-
   Most of the requisite proofs will be done by right-stability using \autoref{rem:proofbystability}, i.e.\ to prove an identity we need to give a unifying morphism such that the requisite diagram commutes, and we need to show that both sides of the identity are right iteration preserving. The proofs of commutativity follow by easy rewriting and are thus deferred to the formalization. The proofs of right iteration preservation follow in most cases instantly since the morphisms are composed of (right) iteration preserving morphisms but in non-trivial cases we will give the full proof.
 
   Naturality of \(\tau \) follows by:
@@ -629,7 +617,7 @@ Of course there is also a symmetric version of this.
     \end{tikzcd}
   \]
 
-  Notably, \(\tau \circ (f \times Kg)\) is right iteration preserving, since for any \(Z : \obj{\C}\) and \(h : Z \rightarrow KY + Z\):
+  Notably, \(\tau \circ (f \times Kg)\) is right iteration preserving, since for any \(Z \in \obj{\C}\) and \(h : Z \rightarrow KY + Z\):
   \begin{alignat*}{1}
      & \tau \circ (f \times Kg) \circ (id \times h^\sharp)
     \\=\;&\tau \circ (f \times {((Kg + id) \circ h)}^\sharp)
@@ -659,7 +647,7 @@ Of course there is also a symmetric version of this.
   Let us now check the strength laws.
 
   \begin{itemize}
-    \item[\ref{S1}] Note that for \(\mathbf{K}\), the identity \(K\pi_2 \circ \tau = \pi_2\) holds more generally for any \(X, Y \in \obj{\C}\), instead of just for \(X = 1\), proven by right-stability, using:
+    \item[\ref{S1}] Note that for \(\mathbf{K}\), the identity \(K\pi_2 \circ \tau = \pi_2\) holds more generally for any \(X, Y \in \obj{\C}\) instead of just for \(X = 1\), which is proven by right-stability, using:
           % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
           \[
             \begin{tikzcd}
@@ -708,7 +696,7 @@ Of course there is also a symmetric version of this.
               \arrow["{\eta \circ \alpha}"', curve={height=12pt}, from=4-1, to=3-4]
             \end{tikzcd}
           \]
-          where \(\tau \circ (id \times \tau) \circ \alpha \) is right iteration preserving, since for any \(Z : \obj{\C}\) and \(h : Z \rightarrow KX + Z\):
+          where \(\tau \circ (id \times \tau) \circ \alpha \) is right iteration preserving, since for any \(Z \in \obj{\C}\) and \(h : Z \rightarrow KX + Z\):
           \begin{alignat*}{1}
              & \tau \circ (id \times \tau) \circ \alpha \circ (id \times h^\sharp)
             \\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle \circ (id \times h^\sharp)
@@ -986,13 +974,13 @@ The following Lemma is central to the proof of commutativity.
   \end{alignat*}
 
   Note that by monicity of \(dstl^{-1}\) and by~\ref{law:fixpoint}
-  \[(\Delta + \langle f^\sharp , id \rangle) \circ f = dstl \circ \langle f^\sharp , f \rangle. \]
+  \[(\Delta + \langle f^\sharp , id \rangle) \circ f = dstl \circ \langle f^\sharp , f \rangle.\tag{*}\label{helperinkey} \]
   The application of~\ref{law:uniformity} is then justified by
   \begin{alignat*}{1}
      & (id + \langle f^\sharp , id \rangle) \circ ((\tau \circ \Delta) + id) \circ f
     \\=\;&((\tau \circ \Delta) + \langle f^\sharp , id \rangle) \circ f
     \\=\;&(\tau + id) \circ (\Delta + \langle f^\sharp , id \rangle) \circ f
-    \\=\;&(\tau + id) \circ dstl \circ \langle f^\sharp , f \rangle
+    \\=\;&(\tau + id) \circ dstl \circ \langle f^\sharp , f \rangle\tag{\ref{helperinkey}}
     \\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\sharp , id \rangle.\tag*{\qedhere}
   \end{alignat*}
 \end{proof}

thesis/src/06_setoids.tex

@@ -1,6 +1,8 @@
 \chapter{A Case Study on Setoids}\label{chp:setoids}
 
-In \autoref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e.\ we will work in the category of setoids and show that the quotiented delay monad is an instance of the previously defined monad \(\mathbf{K}\) in this category.
+In \autoref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also considers computation time in its built-in notion of equality.
+One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified.
+In this chapter we will use the quotients-as-setoid approach, i.e.\ we will work in the category of setoids and show that the quotiented delay monad is an instance of the previously defined monad \(\mathbf{K}\) in this category.
 
 \section{Setoids in Type Theory}
 We will now introduce the category that the rest of the chapter will take place in. Let us start with some basic definitions.
@@ -12,14 +14,15 @@ We will now introduce the category that the rest of the chapter will take place
 For brevity, we will not use the tuple notation most of the time, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
 
 \begin{definition}[Setoid Morphism]
-  A morphism between setoids \(A\) and \(B\) is a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid morphisms as \(A ⇝ B\).
+  A morphism between setoids \(A\) and \(B\) constitutes a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid morphisms as \(A ⇝ B\).
 \end{definition}
 Let us now consider the function space setoid, which is of special interest, since it carries a notion of equality between functions.
 \begin{definition}[Function Space Setoid]
   Given two setoids \(A\) and \(B\), the function space setoid on these setoids is defined as \((A ⇝ B, \doteq)\) or just \(A ⇝ B\), where \(\doteq\) is the point wise equality on setoid morphisms.
 \end{definition}
 
-Setoids together with setoid morphisms form a category that we will call \(\setoids\). Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
+Setoids together with setoid morphisms form a category that we will call \(\setoids\).
+Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
 
 \begin{proposition}
   \(\setoids\) is a distributive category.
@@ -73,7 +76,8 @@ Setoids together with setoid morphisms form a category that we will call \(\seto
           The initial setoid is then \((\bot, \emptyset)\), where the equivalence is the empty relation.
   \end{itemize}
 
-  Lastly we need to show that the canonical distributivity function is an iso. Recall that the canonical distributivity function is defined as \(dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)\). This is equivalent to the following definition that uses pattern matching.
+  Lastly we need to show that the canonical distributivity function is an iso. Recall that the canonical distributivity morphism is defined as \(dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)\).
+  This is equivalent to the following definition that uses pattern matching.
   \begin{minted}{agda}
     distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
                     → (A × B) + (A × C) → A × (B + C)
@@ -87,7 +91,7 @@ Setoids together with setoid morphisms form a category that we will call \(\seto
     distributeˡ (x , i₁ y) = i₁ (x , y)
     distributeˡ (x , i₂ y) = i₂ (x , y)
   \end{minted}
-  Note that these functions are inverse by definition, and it follows quickly that they are setoid morphism.
+  Note that these functions are inverse by definition, and it follows quickly that they are setoid morphisms.
 \end{proof}
 
 \begin{proposition}\label{prop:setoids-ccc}
@@ -268,7 +272,7 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
 \end{theorem}
 \begin{proof}
   We build on \autoref{lem:Delgot}, it thus suffices to show that for any setoid \(A\), the Elgot algebra \((\dbtilde{D}\;A, {(-)}^\sharp)\) together with the setoid morphism \(now : A ⇝ \dbtilde{D}\;A\) is a free such algebra.
-  Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid morphism \(f : A ⇝ B\). We need to define an Elgot algebra function \(\free{f} : \dbtilde{D}\;A ⇝ B\). Consider \(g : \tilde{D}\;A ⇝ B + \tilde{D}\;A\) defined by
+  Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid morphism \(f : A ⇝ B\). We need to define an Elgot algebra morphism \(\free{f} : \dbtilde{D}\;A ⇝ B\). Consider \(g : \tilde{D}\;A ⇝ B + \tilde{D}\;A\) defined by
   \[g\;x =
     \begin{cases}
       i_1(f\;a) & \text{if } x = now\;a   \\
@@ -290,8 +294,8 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
     \\\overset{B}{=}\;&{((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\tag{\ref{law:compositionality}}
   \end{alignat*}
 
-  Thus, \(g^{\sharp_b}\) is an Elgot algebra function. We are left to check that \(g^{\sharp_b}\) satisfies the requisite properties of free objects. First, note that \(g^{\sharp_b} \circ now \doteq [ id , g^\sharp_b ] \circ g \circ now \doteq f\) by \ref{law:fixpoint} and the definition of \(g\). % chktex 2
+  Thus, \(g^{\sharp_b}\) is an Elgot algebra morphism. We are left to check that \(g^{\sharp_b}\) satisfies the requisite properties of free objects. First, note that \(g^{\sharp_b} \circ now \doteq [ id , g^\sharp_b ] \circ g \circ now \doteq f\) by \ref{law:fixpoint} and the definition of \(g\). % chktex 2
-  Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra functions \(e, h : \dbtilde{D}\;A ⇝ B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
+  Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra morphisms \(e, h : \dbtilde{D}\;A ⇝ B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
 
   First, note that the identity function extends to the following conversion setoid morphism \(conv : \tilde{D}\;A ⇝ \dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid morphism \(o : \tilde{D}\;A ⇝ \tilde{D}\;A + \tilde{D}\;A\) defined by
   \[o\;x := \begin{cases}
@@ -352,7 +356,7 @@ Now, consider the following function \(race : D\;A \rightarrow D\;A \rightarrow
     later\;(race\;a\;b) & \text{if } p = later\;a \text{ and } q = later\;b
   \end{cases}\]
 
-The following Corollary, whose proof can be found in the formalization, will be crucial.
+The following Corollary, whose proof can be found in the formalization, will be needed.
 
 \begin{corollary}\label{cor:race}
   \(race\) satisfies the following properties: