Finish partiality, minor work on iteration

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

@@ -61,3 +61,4 @@ isos
 Corecursion
 subobject
 isomorphisms
+epicness

thesis/src/01_preliminaries.tex

@@ -429,7 +429,7 @@ to establish some notation and then describe how to obtain a monad via existence
   \end{tikzcd}\]
 \end{definition}
 
-\begin{theorem}
+\begin{theorem}\label{thm:freemonad}
   Let $U : \C \rightarrow \D$ be a forgetful functor.
   If for every $X \in \obj{\D}$ a free object $FX \in \obj{C}$ exists then $(X \mapsto UFX, \eta : X \rightarrow UFX, \free{(f : X \rightarrow UFY)} : UFX \rightarrow UFY)$ is a Kleisli triple on $\D$. 
 \end{theorem}

thesis/src/03_partiality-monads.tex

@@ -162,7 +162,7 @@ Categorically we obtain this monad by the final coalgebras $DX = \nu A. X + A$,
 
 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{proposition}~\label{col:delay}
+\begin{lemma}~\label{lem:delay}
   The following conditions hold:
   \begin{itemize}
     \item $now : X \rightarrow DX$ and $later : DX \rightarrow DX$ satisfy:
@@ -195,7 +195,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
             \end{tikzcd}\tag*{(D3)}\label{D3}
           \end{equation*}
   \end{itemize}
-\end{proposition}
+\end{lemma}
 \begin{proof}
   We will make use of the fact that every $DX$ is a final coalgebra:
   \begin{itemize}
@@ -255,11 +255,51 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
   \end{itemize}
 \end{proof}
 
+\begin{lemma}
+  The following properties follow from \autoref{lem:delay}:
+  \begin{enumerate}
+    \item $out \circ Df = (f + Df) \circ out$
+    \item $f^* = [ f , {(later \circ f)}^* ] \circ out$
+    \item $later \circ f^* = {(later \circ f)}^* = f^* \circ later$
+  \end{enumerate}
+\end{lemma}
+\begin{proof}
+  \begin{itemize}
+    \item[1.] Note that definitionally: $Df = {(now \circ f)}^*$ for any $f : X \rightarrow TY$. The statement is then simply a consequence of~\ref{D1} and~\ref{D2}:
+    \begin{alignat*}{1}
+      &out \circ Df
+      \\=\;&out \circ {(now \circ f)}^*
+      \\=\;&[ out \circ now \circ f , i_2 \circ {(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
+      \\=\;&(f + Df) \circ out\tag*{\ref{D1}}
+    \end{alignat*}
+    \item[2.] By uniqueness of $f^*$ it suffices to show:
+    \begin{alignat*}{1}
+      &out \circ [ f , {(later \circ f)}^* ] \circ out
+      \\=\;&[ out \circ f , out \circ {(later \circ f)}^* ] \circ out
+      \\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
+      \\=\;&[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$:
+    \begin{alignat*}{1}
+      &out \circ {(later \circ f)}^*
+      \\=\;&[ out \circ later \circ f , i_2 \circ {(later \circ f)}^*] \circ out\tag*{\ref{D2}}
+      \\=\;&i_2 \circ [ f , {(later \circ f)}^*] \circ out\tag*{\ref{D1}}
+      \\=\;&i_2 \circ f^*
+      \\=\;&out \circ later \circ f^*\tag*{\ref{D1}}
+      \\=\;&i_2 \circ f^*\tag*{\ref{D1}}
+      \\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
+      \\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
+      \\=\;&out \circ f^* \circ later \tag*{\ref{D2}}
+    \end{alignat*}
+  \end{itemize}
+\end{proof}
+
 \begin{theorem}
   $\mathbf{D} = (D, now, (-)^*)$ is a Kleisli triple.
 \end{theorem}
 \begin{proof}
-  We will now use the properties proven in Corollary~\ref{col:delay} to prove the Kleisli triple laws:
+  We will now use the properties proven in Corollary~\ref{lem:delay} to prove the Kleisli triple laws:
   \begin{itemize}
     \item[\ref{K1}]
           By uniqueness of $now^*$ it suffices to show that $out \circ id = [ out \circ now , i_2 \circ id ] \circ out$ which instantly follows by \ref{D1}.
@@ -419,20 +459,7 @@ To prove that $\mathbf{D}$ is commutative we will use another proof principle pr
 Let us record some facts that we will use to prove commutativity of $\mathbf{D}$:
 
 \begin{corollary}
-  The following properties hold:
-  % \begin{alignat}{1}
-  %   &out \circ Df = (f + Df) \circ out\label{eq:outD}
-  %   \\&f^* = [ f , {(later \circ f)}^* ] \circ out\label{eq:f*help}
-  %   \\&later \circ f^* = {(later \circ f)}^* = f^* \circ later\label{eq:later*}
-  % \end{alignat}
-  \change[inline]{Move this to beginning, this is not commutativity specific!}
-  \begin{enumerate}
-    \item $out \circ Df = (f + Df) \circ out$
-    \item $f^* = [ f , {(later \circ f)}^* ] \circ out$
-    \item $later \circ f^* = {(later \circ f)}^* = f^* \circ later$
-  \end{enumerate}
-
-  As well as these properties of $\tau$ and $\sigma$:
+  These properties of $\tau$ and $\sigma$ hold:
   \begin{alignat*}{2}
      & out \circ \tau &  & = (id + \tau) \circ dstl \circ (id \times out)\tag*{($\tau_1$)}\label{tau1}
     \\&out \circ \sigma &&= (id + \sigma) \circ dstr \circ (out \times id)\tag*{($\sigma_1$)}\label{sigma1}
@@ -442,41 +469,6 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
 \end{corollary}
 
 \begin{proof}
-  We prove them one by one:
-
-  \begin{itemize}
-    \item[1.] Note that $Df = {(now \circ f)}^*$ definitionally for any $f : X \rightarrow TY$. This is then simply a consequence of~\ref*{D2}.
-    \begin{alignat*}{1}
-      &out \circ Df
-      \\=\;&out \circ {(now \circ f)}^*
-      \\=\;&[ out \circ now \circ f , i_2 \circ {(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
-      \\=\;&(f + Df) \circ out\tag*{\ref{D1}}
-    \end{alignat*}
-    \item[2.] By uniqueness of $f^*$ it suffices to show:
-    \begin{alignat*}{1}
-      &out \circ [ f , {(later \circ f)}^* ] \circ out
-      \\=\;&[ out \circ f , out \circ {(later \circ f)}^* ] \circ out
-      \\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
-      \\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D1}}
-    \end{alignat*}
-    \item[3.] 
-    The next one 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}}
-      \\=\;&i_2 \circ [ f , {(later \circ f)}^*] \circ out\tag*{\ref{D1}}
-      \\=\;&i_2 \circ f^*
-      \\=\;&out \circ later \circ f^*\tag*{\ref{D1}}
-      \\=\;&i_2 \circ f^*\tag*{\ref{D1}}
-      \\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
-      \\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
-      \\=\;&out \circ f^* \circ later \tag*{\ref{D2}}
-    \end{alignat*}
-  \end{itemize}
-
-
-
   \begin{itemize}
     \item[\ref{tau1}] This is just~\ref{D3} restated.
     \item[\ref{sigma1}]
@@ -519,7 +511,7 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
   \[\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 \]
   \[\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 holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$ by 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}}
@@ -552,7 +544,7 @@ 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}\]
-  follows by the fact that $dstr^{-1}$ is epic:
+  is proven using epicness of $dstr^{-1}$:
 
   \begin{alignat*}{1}
      & Ddstr \circ \tau \circ dstr^{-1}

thesis/src/04_iteration.tex

@@ -46,18 +46,26 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
 \end{lemma}
 
 \begin{proof}
-  Let $1$ be the terminal object of $\C$. Given $f : X \rightarrow 1 + X$ we define the iteration $f^\# =\;! : X \rightarrow 1$ as the unique morphism into the terminal object. The laws of Elgot algebras then follow instantly, i.e. $(1 , !)$ is an Elgot algebra and it is the terminal object in $\elgotalgs{\C}$ since $!$ is trivially iteration preserving.
+  Let $1$ be the terminal object of $\C$. Given $f : X \rightarrow 1 + X$ we define the iteration $f^\# =\;! : X \rightarrow 1$ as the unique morphism into the terminal object. The Elgot algebra laws follow instantly by uniqueness of $!$. $(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.
 
-  Let $(A, (-)^{\#_a}) , (B, (-)^{\#_b}) \in \vert\elgotalgs{\C}\vert$ and $A \times B$ be the product in $\C$. Given $f : X \rightarrow (A \times B) + X$ we define the iteration as:
+  Let $(A, (-)^{\#_a}) , (B, (-)^{\#_b}) \in \vert\elgotalgs{\C}\vert$ and $A \times B$ be the product of $A$ and $B$ in $\C$. Given $f : X \rightarrow (A \times B) + X$ we define the iteration as:
   \[f^\# = \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle : X \rightarrow A \times B\]
-  Then $(A \times B, (-)^\#)$ is indeed an Elgot algebra, the laws follow by the laws of the algebras on A and B.
+  We show that $(A \times B, (-)^\#)$ is indeed an Elgot algebra:
+  \todo[inline]{Show Elgot laws for product}
+  \begin{itemize}
+    \item \textbf{Fixpoint}:
+    \item \textbf{Uniformity}:
+    \item \textbf{Folding}:
+  \end{itemize}
 
+  \todo[inline]{More explicit}
   The product diagram of $A \times B$ in $\C$ then also holds in $\elgotalgs{\C}$, we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism $\langle f , g \rangle$ is iteration preserving for any $f : (Z, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_y})$, which follows since $f$ and $g$ are iteration preserving.
 \end{proof}
 
 \begin{lemma}\label{lem:elgotexp}
   Given $X \in \obj{\C}$ and $(A, (-)^{\#_a}) \in \vert\elgotalgs{\C}\vert$. The exponential $X^A$ (if it exists) can be equipped with an Elgot algebra structure.
 \end{lemma}
+\todo[inline]{Prove explicitly}
 \begin{proof}
   Take $f^\# = curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ for any $f : Z \rightarrow A^X + Z$.
   The \textbf{Fixpoint}, \textbf{Uniformity} and \textbf{Folding} laws for $(A^X, (-)^\#)$ follow by the laws of $(A, (-)^{\#_a})$ and some rewriting using properties of distributive categories.
@@ -107,13 +115,11 @@ Pre-Elgot monads on $\C$ form a category that is a subcategory of $\monads{\C}$.
 \section{The Initial Strong Pre-Elgot Monad}
 In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial pre-Elgot monad.
 
-\begin{lemma}
-  If every $X \in \obj{\C}$ extends to a free Elgot algebra $KX$ we get a monad $\mathbf{K}$.
-\end{lemma}
+\begin{proposition}
+  Existence of all free Elgot algebras yields a monad that we call $\mathbf{K}$.
+\end{proposition}
 \begin{proof}
-  \todo[inline]{Maybe this can even be proven without adjunction, show that free objects yield a Kleisli triple!}
-  \todo[inline]{Proof in preliminaries}
-  Existence of all free objects in $\elgotalgs{\C}$ yields an adjunction between $\C$ and $\elgotalgs{\C}$ that in turn gives us a monad on $\C$.
+  This is a direct consequence of \autoref{thm:freemonad}.
 \end{proof}
 
 To show that $\mathbf{K}$ is strong we will need a notion of stability:
@@ -127,7 +133,7 @@ To show that $\mathbf{K}$ is strong we will need a notion of stability:
   We also call the property that \ref{sharpr2} establishes \textit{right iteration preserving}.
 \end{definition}
 
-We get the following dual definition:
+We obtain the following dual definition:
 
 \begin{definition}[Left-Stable Free Elgot Algebra]\label{def:leftstablefreeelgot}
   Let $KY$ be a free Elgot algebra on $Y \in \obj{\C}$. We call $KY$ \textit{left-stable} if for every $A \in \elgotalgs{\C}$ and $f : Y \times X \rightarrow A$ there exists a unique $f^{\sharp_l} : KY \times X \rightarrow A$ satisfying:
@@ -153,7 +159,7 @@ We get the following dual definition:
 
 We will usually refer to right-stable free Elgot algebras as just stable Elgot algebras and omit the index of the operator.
 
-Stability of $KX$ expresses that it somehow behaves like it would in a cartesian closed category, the following theorem should then follow trivially:
+Stability of $KX$ expresses that it behaves like it would in a cartesian closed category, the following theorem illustrates this.
 
 \begin{theorem}\label{thm:stability}
   In a cartesian closed category every free Elgot algebra is stable.