diff --git a/thesis/main.tex b/thesis/main.tex
index 7619561..8fa05e7 100644
--- a/thesis/main.tex
+++ b/thesis/main.tex
@@ -99,51 +99,18 @@
 
 
 \usepackage{noto-mono}
-\usepackage{mathpazo}
 \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}
 
-\usepackage{pict2e}
-
-% \newcommand{\lbparen}{%
-%   \mathopen{%
-%     \sbox0{$()$}%
-%     \setlength{\unitlength}{\dimexpr\ht0+\dp0}%
-%     \raisebox{-\dp0}{%
-%       \begin{picture}(.32,1)
-%       \linethickness{\fontdimen8\textfont3}
-%       \roundcap
-%       \put(0,0){\raisebox{\depth}{$($}}
-%       \polyline(0.32,0)(0.1,0)(0.1,1)(0.32,1)
-%       \end{picture}%
-%     }%
-%   }%
-% }
-
-% \newcommand{\rbparen}{%
-%   \mathclose{%
-%     \sbox0{$()$}%
-%     \setlength{\unitlength}{\dimexpr\ht0+\dp0}%
-%     \raisebox{-\dp0}{%
-%       \begin{picture}(.32,1)
-%       \linethickness{\fontdimen8\textfont3}
-%       \roundcap
-%       \put(0.02,0){\raisebox{\depth}{$)$}}
-%       \polyline(0.1,0)(0.32,0)(0.32,1)(0.1,1)
-%       \end{picture}%
-%     }%
-%   }%
-% }
-
-\newcommand{\lbparen}{〖}
 % https://unicodeplus.com/U+3016
-
-\newcommand{\rbparen}{〗}
+\newcommand*{\lbparen}{〖}
+\newcommand*{\rbparen}{〗}
 
 % category C
 \newcommand*{\C}{\ensuremath{\mathscr{C}}}
@@ -160,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
diff --git a/thesis/src/04_iteration.tex b/thesis/src/04_iteration.tex
index 7a00d81..57fef40 100644
--- a/thesis/src/04_iteration.tex
+++ b/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
-  $\ls{f} := eval \circ (\llbracket curry\;f \rrbracket \times id)$. 
-  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}.
-  \ref{sharpl1} and \ref{sharpl2} then follow by properties of the exponential and of distributive categories, uniqueness is more interesting:
-  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:
-  \[curry\; g = \llbracket curry\;f \rrbracket = curry (eval \circ (\llbracket curry\;f \rrbracket \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}.
+  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$.
+  We will now verify that this does indeed satisfy the requisite properties, i.e.
+  \begin{alignat*}{1}
+    &eval \circ (\free{curry\;f} \times id) \circ (\eta \times id)
+    \\=\;&eval \circ ((\free{curry\;f} \circ \eta) \times id)
+    \\=\;&eval \circ (curry\;f) \times id)
+    \\=\;&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}.
-
-\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 find a morphism $f : X \times Y \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpr1} and \ref{sharpr2}.
+Let us first introduce a proof principle similar to \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 $g \circ (id \times \eta) = f$ and $h \circ (id \times \eta) = f$.
 \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}