Continue working on proofs concerning K

thesis/main.tex

@@ -99,12 +99,18 @@
 
 
 \usepackage{noto-mono}
+\usepackage{unicode-math}
+% \setmainfont{STIX-Regular}
+% \setmathfont{STIX Two Math Regular}
+
 \usepackage{mathrsfs}
 \usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
 \usepackage{xargs}
 \usepackage{xstring}
-%\usepackage{fontspec}
+
-%\setmonofont{Noto Sans Mono}
+% https://unicodeplus.com/U+3016
+\newcommand*{\lbparen}{〖}
+\newcommand*{\rbparen}{〗}
 
 % category C
 \newcommand*{\C}{\ensuremath{\mathscr{C}}}
@@ -121,10 +127,15 @@
 \newcommand*{\strongpreelgot}[1]{\ensuremath{\mathit{StrongPreElgot}(#1)}}
 \newcommand*{\setoids}{\ensuremath{\mathit{Setoids}}}
 % free objects
-\newcommand*{\freee}[1]{\ensuremath{#1^\bigstar}}
+\newcommand*{\freee}[1]{\ensuremath{#1^\star}}
 \newcommand*{\free}[1]{
   \ensuremath{
-    \IfSubStr{#1}{\circ}{{\freee{(#1)}}}{\freee{#1}}
+    \IfSubStr{#1}{\circ}
+      {{\freee{(#1)}}}
+      {\IfSubStr{#1}{\;}
+        {\freee{(#1)}}
+        {\freee{#1}}
+      }
   }
 }
 % right stability
@@ -142,7 +153,7 @@
   }
 }
 % terminal coalgebra
-\newcommand*{\coalg}[1]{\ensuremath{\llbracket #1 \rrbracket}}
+\newcommand*{\coalg}[1]{\ensuremath{\lbparen#1\rbparen}}
 
 \begin{document}
 \pagestyle{plain}
@@ -168,6 +179,7 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
 \newcommandx{\info}[2][1=]{\todo[inline,linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}}
 \newcommandx{\improvement}[2][1=]{\todo[inline,linecolor=Plum,backgroundcolor=Plum!25,bordercolor=Plum,#1]{#2}}
 
+
 % for creating custom labels like (Fixpoint)
 \makeatletter
 \newcommand{\customlabel}[2]{%

thesis/src/03_partiality-monads.tex

@@ -357,11 +357,12 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
       \arrow["out", from=3-1, to=3-5]
       \arrow["{id \times out}", from=1-1, to=1-2]
       \arrow["dstl", from=1-2, to=1-3]
-      \arrow["{\coalg{-}}", dashed, from=1-1, to=3-1]
+      \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
       \arrow["{f \times g + id}", from=1-3, to=1-5]
-      \arrow["{id + \coalg{-}}", dashed, from=1-5, to=3-5]
+      \arrow["{id + \coalg{\text{-}}}", dashed, from=1-5, to=3-5]
     \end{tikzcd}\]
-  We write $\coalg{-}$ to abbreviate the used coalgebra, i.e.\ in this diagram $\coalg{-} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}$
+  We write $\coalg{\text{-}}$ to abbreviate the used coalgebra, i.e.\ in the previous diagram
+  \[\coalg{\text{-}} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}.\]
 
   Next we check the strength laws:
   \begin{itemize}
@@ -371,8 +372,8 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
               {1 \times DX} \& {1 \times X + DX} \& {1 \times X + 1 \times DX} \& {X + 1 \times DX} \\
               DX \&\&\& {X + DX}
               \arrow["out", from=2-1, to=2-4]
-              \arrow["{\coalg{-}}", dashed, from=1-1, to=2-1]
+              \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
-              \arrow["{id + \coalg{-}}", from=1-4, to=2-4]
+              \arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4]
               \arrow["{id \times out}", from=1-1, to=1-2]
               \arrow["dstl", from=1-2, to=1-3]
               \arrow["{\pi_2 + id}", from=1-3, to=1-4]
@@ -396,11 +397,11 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
               {X \times DDY} \& {X \times (DY + DDY)} \& {X \times DY + X \times DDY} \\
               \&\& {X \times Y + X \times DDY} \\
               {D(X\times Y)} \&\& {X \times Y + D(X \times Y)}
-              \arrow["{\coalg{-}}", dashed, from=1-1, to=3-1]
+              \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
               \arrow["{id \times out}", from=1-1, to=1-2]
               \arrow["dstl", from=1-2, to=1-3]
               \arrow["out", from=3-1, to=3-3]
-              \arrow["{id + \coalg{-}}"', from=2-3, to=3-3]
+              \arrow["{id + \coalg{\text{-}}}"', from=2-3, to=3-3]
               \arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3]
             \end{tikzcd}\]
     \item[\ref{S4}] To show $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ by coinduction we take the coalgebra:
@@ -409,9 +410,9 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
               {(X \times Y) \times DZ} \& {(X \times Y) \times (Z+ DZ)} \& {(X\times Y) \times Z + (X \times Y) \times DZ} \\
               \&\& {X \times Y  \times Z + (X \times Y) \times DZ} \\
               {D(X \times Y \times Z)} \&\& {X \times Y \times Z + D(X \times Y \times Z)}
-              \arrow["{\coalg{-}}", dashed, from=1-1, to=3-1]
+              \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
               \arrow["out", from=3-1, to=3-3]
-              \arrow["{id +\coalg{-}}"', from=2-3, to=3-3]
+              \arrow["{id +\coalg{\text{-}}}"', from=2-3, to=3-3]
               \arrow["{id \times out}", from=1-1, to=1-2]
               \arrow["dstl", from=1-2, to=1-3]
               \arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3]
@@ -451,8 +452,8 @@ To prove that $\mathbf{D}$ is commutative we will use another proof principle pr
       \arrow["out", from=2-1, to=2-4]
       \arrow["out", from=1-1, to=1-2]
       \arrow["{[ [ i_1 , h ] , i_2 ]}", from=1-2, to=1-4]
-      \arrow["{id + \coalg{-}}", from=1-4, to=2-4]
+      \arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4]
-      \arrow["{\coalg{-}}", dashed, from=1-1, to=2-1]
+      \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
     \end{tikzcd}\]
 \end{proof}
 

thesis/src/04_iteration.tex

@@ -305,7 +305,7 @@ A symmetrical variant of the previous definition is sometimes useful.
     \\=\;&\ls{f \circ swap} \circ (h^{\#_y} \times id) \circ swap
     \\=\;&((\ls{f \circ swap} + id) \circ dstr \circ (id \times h))^{\#_a} \circ swap
     \\=\;&(((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h))^{\#_a}\tag{\ref{law:uniformity}}
-    \\=\;&(((\rs{f} + id) \circ dstl \circ (id \times h))^{\#_a}
+    \\=\;&(((\rs{f} + id) \circ dstl \circ (id \times h))^{\#_a},
   \end{alignat*}
   for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$.
 
@@ -318,7 +318,7 @@ A symmetrical variant of the previous definition is sometimes useful.
     \\=\;&(\ls{f \circ swap} + id) \circ dstr \circ (h \times id) \circ swap.
   \end{alignat*}
 
-  The diagram commutes, since
+  The requisite diagram commutes, since
   \begin{alignat*}{1}
     &\rs{f} \circ (id \times \eta)
     \\=\;&\ls{f \circ swap} \circ swap \circ (id \times \eta)
@@ -342,19 +342,20 @@ A symmetrical variant of the previous definition is sometimes useful.
     \\=\;&((g + id) \circ dstl \circ (id \times h))^{\#_a} \circ swap
     \\=\;&(((g \circ swap) + id) \circ dstr \circ (h \times id))^{\#_a},\tag{\ref{law:uniformity}}
   \end{alignat*}
+  for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$.
 
-  where the application of \ref{law:uniformity} is justified by
+  The application of \ref{law:uniformity} is justified by
   \begin{alignat*}{1}
     &(id + swap) \circ ((g \circ swap) + id) \circ dstr \circ (h \times id)
     \\=\;&(g + id) \circ (swap + swap) \circ dstr \circ (h \times id)
     \\=\;&(g + id) \circ dstl \circ swap \circ (h \times id)
-    \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap
+    \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap.
   \end{alignat*}
 
-  This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows by a symmetrical proof.
+  This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows symmetrically.
 \end{proof}
 
-The following theorem illustrates that stability of $KX$ indeed simulates the behavior of $KX$ in a cartesian closed category.
+In a less general setting stability indeed follows automatically.
 
 \todo[inline]{Fix proof, replace free object operator, fix references.}
 
@@ -362,31 +363,70 @@ The following theorem illustrates that stability of $KX$ indeed simulates the be
   In a cartesian closed category every free Elgot algebra is stable.
 \end{theorem}
 \begin{proof}
-  Let $X \in \obj{\C}$ and $((KX, (-)^\#), \llbracket - \rrbracket)$ be a free Elgot algebra on $X$.
+  Let $\C$ be cartesian closed and let $(KX, (-)^\#, \free{(-)})$ be a free Elgot algebra on some $X \in \obj{\C}$.
 
-  We will show that $KX$ is left-stable, i.e. given $X \in \obj{\C}, A \in \vert\elgotalgs{\C}\vert$ and $f : Y \times X \rightarrow A$ we define
+  To show left stability of $KX$ we define $\ls{f} := eval \circ (\free{curry\;f} \times id)$ for any $X \in \obj{\C}, A \in \vert\elgotalgs{\C}\vert$, and $f : Y \times X \rightarrow A$.
-  $\ls{f} := eval \circ (\llbracket curry\;f \rrbracket \times id)$. 
+  We will now verify that this does indeed satisfy the requisite properties, i.e.
-  Note that we are using the universal property of a free object over $\textit{Elgot}(\C)$ which when spelled out requires us to show that $A^X$ is an Elgot algebra, for that we reference lemma~\ref{lem:elgotexp}.
+  \begin{alignat*}{1}
-  \ref{sharpl1} and \ref{sharpl2} then follow by properties of the exponential and of distributive categories, uniqueness is more interesting:
+    &eval \circ (\free{curry\;f} \times id) \circ (\eta \times id)
-  Let $g : KY \times X \rightarrow A$ be a morphism satisfying \ref{sharpl1} and \ref{sharpl2}, we need to show that $g = eval \circ (\llbracket curry\;f \rrbracket \times id)$. We use that fact that $curry$ is an injective mapping, i.e. it suffices to show that:
+    \\=\;&eval \circ ((\free{curry\;f} \circ \eta) \times id)
-  \[curry\; g = \llbracket curry\;f \rrbracket = curry (eval \circ (\llbracket curry\;f \rrbracket \times id))\]
+    \\=\;&eval \circ (curry\;f) \times id)
-  Where the second step holds for any exponential and the first step is proven by the universal property of free objects, i.e. we need to show that $curry\;g \circ \eta = curry\;f$ which follows by \ref{sharpl1}, and we need to check that $curry\;g$ is left iteration preserving which follows from \ref{sharpl2}.
+    \\=\;&f
+  \end{alignat*}
+  and for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$:
+  \begin{alignat*}{1}
+    &eval \circ (\free{curry\;f} \times id) \circ (h^{\#_a} \times id)
+    \\=\;&eval \circ ((\free{curry\;f} \circ h^{\#_a}) \times id)
+    \\=\;&eval \circ (curry(((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\#_b})) \times id)
+    \\=\;&((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\#_b}
+    \\=\;&((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))^{\#_b}
+    \\=\;&((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))^{\#_b}
+    \\=\;&(((eval \circ (\free{curry\;f} \times id)) + id) \circ dstr \circ (h \times id))^{\#_b}.
+  \end{alignat*}
+
+  \unsure[inline]{Maybe prove that curry is injective in preliminaries.}
+  
+  Lastly, we need to check uniqueness of $\ls{f}$. Let us consider a left iteration preserving morphism $g : KY \times X \rightarrow A$ that satisfies $g \circ (\eta \times id) = f$. Since $curry$ is an injective mapping it suffices to show that
+  \begin{alignat*}{1}
+    &curry\;\ls{f}
+    \\=\;&curry(eval \circ (\free{curry\;f} \times id))
+    \\=\;&\free{curry\;f}
+    \\=\;&curry\;g.
+  \end{alignat*}
+  Where the last step is the only non-trivial one. Since $\free{curry\;f}$ is a unique iteration preserving morphism satisfying $\free{curry\;f} \circ \eta = curry\;f$, we are left to show that $g$ is also iteration preserving and satisfies the same property.
+
+  \unsure[inline]{Maybe prove helper lemmas about exponentials in preliminaries, like subst, beta and eta.}
+  
+  Indeed,
+  \begin{alignat*}{1}
+    &curry\;g \circ h^{\#}
+    \\=\;&curry\;(g \circ (h^{\#} \times id))
+    \\=\;&curry\;(((g + id) \circ dstr \circ (h \times id))^{\#_a})
+    \\=\;&curry\;((((eval \circ (curry\; g \times id)) + id) \circ dstr \circ (h \times id))^{\#_a})
+    \\=\;&curry\;(((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))^{\#_a})
+    \\=\;&curry\;(((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))^{\#_a})
+    \\=\;&curry\;(((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))^{\#_a})
+  \end{alignat*} 
+  for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$, and
+  \begin{alignat*}{1}
+    &curry\;g \circ \eta
+    \\=\;&curry(g \circ (\eta \times id))
+    \\=\;&curry\;f
+  \end{alignat*}
+
+  This completes the proof.
 \end{proof}
 
-For the rest of this chapter we will assume every $KX$ to exist and be stable to show that it is an equational lifting monad and in fact the initial strong pre-Elgot monad.
+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.
 
-Before proving strength, we will introduce a proof principle similar to remark~\ref{rem:coinduction}.
+Let us first introduce a proof principle similar to \autoref{rem:coinduction}.
-
+\begin{remark}[Proof by right-stability]~\label{rem:proofbystability}
-\begin{remark}[Proof by 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 $g \circ (id \times \eta) = f$ and $h \circ (id \times \eta) = f$.
-  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 find a morphism $f : X \times Y \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpr1} and \ref{sharpr2}.
 \end{remark}
-
+Of course there is also a symmetric version of this.
-Of course there is also a symmetric version of this:
-
 \begin{remark}[Proof by left-stability]~\label{rem:proofbyleftstability}
-  Given two morphisms $g, h : KY \times X \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to find a morphism $f : Y \times X \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpl1} and \ref{sharpl2}.
+  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 left iteration preserving and there exists a morphism $f : Y \times X \rightarrow A$ such that $g \circ (\eta \times id) = f$ and $h \circ (\eta \times id) = f$.
 \end{remark}
-
 \todo[inline]{Maybe do a helper proposition first that characterizes tau with the three laws in the file}
 
 \begin{theorem}
@@ -397,7 +437,7 @@ Of course there is also a symmetric version of this:
 
   \change[inline]{Maybe put complete proof}
 
-  To check naturality and the strength laws we will use remark~\ref{rem:proofbystability} and for brevity only state the needed unifying morphism by pasting \ref{sharpl1} into the required diagram. The proofs of \ref{sharpr1} and \ref{sharpr2} can then be looked up in the formalization.
+  To check naturality and the strength laws we will use \autoref{rem:proofbystability} and for brevity only state the needed unifying morphism by pasting \ref{sharpl1} into the required diagram. The proofs of \ref{sharpr1} and \ref{sharpr2} can then be looked up in the formalization.
 
   For naturality of $\tau$ we use:
   % https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
@@ -507,7 +547,38 @@ Of course there is also a symmetric version of this:
 \end{theorem}
 
 \begin{proof}
-  \todo[inline]{Proof that K is equational lifting}
+  We need to show that $\tau \circ \Delta = K \langle \eta , id \rangle$. Note that $K \langle \eta , id \rangle = \free{\eta \circ \langle \eta , id \rangle}$, which is a unique Elgot algebra morphism satisfying $K \langle \eta , id \rangle \circ \eta = \eta \circ \langle \eta , id \rangle$. It thus suffices to show that $\tau \circ \Delta$ satisfies the same identity and is iteration preserving.
+
+  The identity follows easily
+
+  \todo[inline]{Reference $\tau-\eta$ in last step:}
+
+  \begin{alignat*}{1}
+    &\tau \circ \Delta \circ \eta
+    \\=\;&\tau \circ \langle \eta , \eta \rangle
+    \\=\;&\tau \circ (id \times \eta) \circ \langle \eta , id \rangle
+    \\=\;&\eta \circ \langle \eta , id \rangle.
+  \end{alignat*}
+
+  For iteration preservation of $\tau \circ \Delta$ consider $Z \in \obj{\C}$ and $h : Z \rightarrow KX + Z$, then
+  \begin{alignat*}{1}
+    &\tau \circ \Delta \circ h^{\#}
+    \\=\;&\tau \circ \langle h^{\#} , h^{\#} \rangle
+    \\=\;&\tau \circ (id \times h^{\#}) \circ \langle h^{\#} , id \rangle
+    \\=\;&((\tau + id) \circ dstl \circ (id \times f))^\# \circ \langle h^{\#} , id \rangle
+    \\=\;&(((\tau \circ \Delta) + id) \circ f)^\#.\tag{\ref{law:uniformity}}
+  \end{alignat*}
+
+  Note that by monicity of $dstl^{-1}$ and by \ref{law:fixpoint}
+  \[(\Delta + \langle f^\# , id \rangle) \circ f = dstl \circ \langle f^\# , f \rangle. \]
+  The application of \ref{law:uniformity} is then justified by
+  \begin{alignat*}{1}
+    &(id + \langle f^\# , id \rangle) \circ ((\tau \circ \Delta) + id) \circ f
+    \\=\;&((\tau \circ \Delta) + \langle f^\# , id \rangle) \circ f
+    \\=\;&(\tau + id) \circ (\Delta + \langle f^\# , id \rangle) \circ f
+    \\=\;&(\tau + id) \circ dstl \circ \langle f^\# , f \rangle
+    \\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\# , id \rangle.
+  \end{alignat*}
 \end{proof}
 
 \begin{theorem}