Work on iteration chapter

thesis/main.tex

@@ -99,6 +99,7 @@
 
 
 \usepackage{noto-mono}
+\usepackage{mathrsfs}
 \usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
 \usepackage{xargs}
 \usepackage{xstring}
@@ -106,8 +107,8 @@
 %\setmonofont{Noto Sans Mono}
 
 % category C
-\newcommand*{\C}{\ensuremath{\mathcal{C}}}
-\newcommand*{\D}{\ensuremath{\mathcal{D}}}
+\newcommand*{\C}{\ensuremath{\mathscr{C}}}
+\newcommand*{\D}{\ensuremath{\mathscr{D}}}
 % objects of category
 \newcommand*{\obj}[1]{\ensuremath{\vert #1 \vert}}
 % category of elgot algebras on #1
@@ -126,6 +127,20 @@
     \IfSubStr{#1}{\circ}{{\freee{(#1)}}}{\freee{#1}}
   }
 }
+% right stability
+\newcommand*{\rss}[1]{\ensuremath{#1^\blacktriangleright}}
+\newcommand*{\rs}[1]{
+  \ensuremath{
+    \IfSubStr{#1}{\circ}{{\rss{(#1)}}}{\rss{#1}}
+  }
+}
+% left stability
+\newcommand*{\lss}[1]{\ensuremath{#1^\blacktriangleleft}}
+\newcommand*{\ls}[1]{
+  \ensuremath{
+    \IfSubStr{#1}{\circ}{{\lss{(#1)}}}{\lss{#1}}
+  }
+}
 % terminal coalgebra
 \newcommand*{\coalg}[1]{\ensuremath{\llbracket #1 \rrbracket}}
 
@@ -171,6 +186,9 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
 \include{src/05_setoids}
 \include{src/10_conclusion}
 
+\todo[inline]{Symbolverzeichnis, siehe: https://www.namsu.de/Extra/pakete/Listofsymbols.pdf}
+\todo[inline]{Add fullstop behind every proof}
+
 \appendix
 % \include{src/A1_contributions}
 

thesis/src/01_preliminaries.tex

@@ -296,6 +296,7 @@ Monads are widely known among programmers as a way of modelling effects in pure
 
 As with many categorical concepts we may consider the category of monads:
 
+\todo[inline]{Use text => lemma style}
 \begin{definition}[The Category of Monads]~\label{def:monads}
   Let $\C$ be a category.
   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:
@@ -394,6 +395,7 @@ where p and q are (partial) computations. This condition can be expressed catego
 where $\alpha_{X,Y,Z} = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : X \times (Y \times Z) \rightarrow (X \times Y) \times Z$ is the associativity morphism on products. 
 \end{definition}
 
+\todo[inline]{Use text => lemma style}
 As with monads we can now consider the category of strong monads:
 \begin{definition}[The Category of Strong Monads]\label{def:strongmonads}
   Let $\C$ be a category. 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:monads} that additionally satisfies:

thesis/src/04_iteration.tex

@@ -21,28 +21,50 @@ In this chapter we will draw on the inherent connection between partiality and i
   \end{itemize}
 \end{definition}
 
-A morphism between Elgot algebras $h : (A, (-)^{\#_a}) \rightarrow (B, (-)^{\#_a})$ is an iteration preserving morphism $h : A \rightarrow B$ i.e. a morphism satisfying: $h \circ f^{\#_a} = ((h + id) \circ f)^{\#_b}$ for any $f : X \rightarrow A + X$.
+Morphisms between Elgot algebras that are coherent with respect to the iteration operator are of special interest to us, the following definition classifies them.
 
-\change[inline]{This should not be a theorem}
-\begin{theorem}~\label{def:elgotalgebras}
-  Elgot algebras on a category $\C$ and the morphisms between them form a category that we call $\elgotalgs{\C}$.
-\end{theorem}
-\begin{proof}
-  The identity morphism $id : (A, (-)^\#) \rightarrow (A, (-)^\#)$ is the identity morphism of $\C$ that is trivially iteration preserving.
+\begin{definition}
+  Let $(A, (-)^{\#_a}), (B, (-)^{\#_b})$ be two Elgot algebras. 
+  
+  A morphism $f : X \times A \rightarrow B$ is called \textit{right iteration preserving} if
+  \[f \circ (id \times h^{\#_a}) = ((f + id) \circ dstl \circ (id \times h))^{\#_b}\]
+  for any $h : Y \rightarrow A + Y$.
 
-  Composition of two morphisms $f : (B , (-)^{\#_b}) \rightarrow (C, (-)^{\#_c})$ and $g : (A , (-)^{\#_a}) \rightarrow (B , (-)^{\#_b})$ is the composition of the underlying morphisms, we are left to check that it is iteration preserving, i.e. let $X \in \obj{\C}$ and $h : X \rightarrow A + X$:
-  \begin{alignat*}{1}
-    &f \circ g \circ h^{\#_a}\\
-    =\;& f \circ ((g + id) \circ h)^{\#_b}\tag*{g iteration preserving}\\
-    =\;&((f \circ g) \circ h)^{\#_c}\tag*{f iteration preserving}
-  \end{alignat*}
+  Symmetrically a morphism $g : A \times X \rightarrow B$ is called \textit{left iteration preserving} if
+  \[f \circ (h^{\#_a} \times id) = ((f + id) \circ dstr \circ (h \times id))^{\#_b}\]
+  for any $h : Y \rightarrow A + Y$.
 
-  The laws concerning $id$ and composition follow directly since they hold in $\C$.
-\end{proof}
+  Let us also consider the special case where $X = 1$.
+  A morphism $f : A \rightarrow B$ is called \textit{iteration preserving} if
+  \[f \circ h^{\#_a} = ((f + id) \circ h)^{\#_b}\]
+  for any $h : Y \rightarrow A + Y$.
+\end{definition}
 
-We can form products and exponentials of Elgot algebras in a canonical way, for products this is even stronger:
+The previous definition yields the category of Elgot algebras over a category $\C$ and iteration preserving morphisms between these algebras. We call this category $\elgotalgs{\C}$.
 
 \begin{lemma}
+  $\elgotalgs{\C}$ is a category.
+\end{lemma}
+\begin{proof}
+  It suffices to show that the identity morphism in $\C$ is iteration preserving and the composite of two iteration preserving morphisms is also iteration preserving.
+
+  Let $(A , (-)^{\#_a}), (B , (-)^{\#_b}), (C , (-)^{\#_c})$ be Elgot algebras.
+  The identity trivially satisfies 
+  \[id \circ f^{\#_a} = f^{\#_a} = ((id + id) \circ f)^{\#_a}\]
+  for any $f : X \rightarrow A + X$.
+  Given two iteration preserving morphisms $f : B \rightarrow C, g : A \rightarrow B$, the composite is iteration preserving since
+  \begin{alignat*}{1}
+    &f \circ g \circ h^{\#_a}
+    \\=\;& f \circ ((g + id) \circ h)^{\#_b}
+    \\=\;&((f + id) \circ (g + id) \circ h)^{\#_c}
+    \\=\;&(((f \circ g) + id) \circ h)^{\#_c}
+  \end{alignat*}
+  for any $h : X \rightarrow A + X$.
+\end{proof}
+
+Products and exponentials of Elgot algebras can be formed in a canonical way.
+
+\begin{lemma}\label{lem:elgotalgscat}
   If $\C$ is a cartesian category, so is $\elgotalgs{\C}$.
 \end{lemma}
 
@@ -53,7 +75,7 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
   \[f^\# = \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle : X \rightarrow A \times B\]
   Next we show that $(A \times B, (-)^\#)$ is indeed an Elgot algebra:
   \begin{itemize}
-    \item \textbf{Fixpoint}: Let $f : X \rightarrow (A \times B) + X$. \change{rewrite} The fixpoint law for $f^\#$ follows by the fixpoint law of $((\pi_1 + id) \circ f)^{\#_a}$ and $((\pi_2 + id) \circ f)^{\#_b}$:
+    \item \textbf{Fixpoint}: Let $f : X \rightarrow (A \times B) + X$. The requisite equation follows by the fixpoint identities of $((\pi_1 + id) \circ f)^{\#_a}$ and $((\pi_2 + id) \circ f)^{\#_b}$:
     \begin{alignat*}{1}
       &\langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle
       \\=\;&\langle [ id , ((\pi_1 + id) \circ f)^{\#_a} ] \circ (\pi_1 + id) \circ f 
@@ -118,7 +140,7 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
   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}
 \begin{proof}
-  Take $f^\# = curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ for any $f : Z \rightarrow A^X + Z$.
+  Take $f^\# = curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ as the iteration of some $f : Z \rightarrow A^X + Z$.
 
   \begin{itemize}
     \item \textbf{Fixpoint}: Let $f : Y \rightarrow X^A + Y$ with $Y \in \obj{C}$. By uniqueness of $f^\# = curry\;(((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ it suffices to show:
@@ -205,21 +227,27 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
 \improvement{Add some text, explain Elgot monads and while loops}
 
 \begin{definition}[(Strong) Pre-Elgot Monad]
-  A monad $\mathbf{T}$ is called pre-Elgot if every $TX$ extends to an Elgot algebra such that Kleisli lifting is iteration preserving, i.e.
-  \[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; Z \in \obj{\C}, f : Z \rightarrow TX + Z, h : X \rightarrow TY\]
+  A monad $\mathbf{T}$ is called pre-Elgot if every $TX$ extends to an Elgot algebra such that for every $f : X \rightarrow TY$ the Kleisli lifting $f^* : TX \rightarrow TY$ is iteration preserving.
 
-  If $\mathbf{T}$ is additionally strong and the strength $\tau$ is iteration preserving in the following sense:
-  \[\tau \circ (id \times f^\#) = ((\tau + id) \circ dstl \circ (id \times f))^\# \qquad \text{for}\; Z \in \obj{\C}, f : Z \rightarrow TX + Z\]
-  Then $\mathbf{T}$ is called strong pre-Elgot.
+  If $\mathbf{T}$ is additionally strong and the strength $\tau$ is right iteration preserving we call it strong pre-Elgot.
 \end{definition}
 
-Let us briefly introduce the category of (strong) pre-Elgot monads because the initial object of this category will be of special interest to us.
+(Strong) pre-Elgot monads form a subcategory of $\monads{\C}$ where objects are (strong) pre-Elgot monads and morphisms between pre-Elgot monads are natural transformations $\alpha$ as in \autoref{def:monads} such that additionally each $\alpha_X$ is iteration preserving. Similarly, morphisms between strong pre-Elgot monads are natural transformations $\alpha$ as in \autoref{def:strongmonads} such that each $\alpha_X$ is iteration preserving. We call these categories $\preelgot{\C}$ and $\strongpreelgot{\C}$ respectively.
 
-\begin{definition}[The Category of (Strong) Pre-Elgot Monads]
-  Let $\C$ be a category. We define the category $\preelgot{\C}$ where objects are pre-Elgot monads and morphisms between pre-Elgot monads are morphisms between monads as in \autoref{def:monads} and additionally every $\alpha_X$ is a morphism between Elgot algebras as in \autoref{def:elgotalgebras}.
+\begin{lemma}
+  $\preelgot{\C}$ and $\strongpreelgot{\C}$ are categories.
+\end{lemma}
+\begin{proof}
+  Using \autoref{def:monads} and \autoref{def:strongmonads} it suffices to show that the components of the identity natural transformation are iteration preserving and that the composition of two pre-Elgot monad morphisms is iteration preserving component wise. This has already been shown in \autoref{lem:elgotalgscat}.
+\end{proof}
 
-  Similarly, morphisms between strong pre-Elgot Monads are morphisms between strong monads as in \autoref{def:strongmonads} and every $\alpha_X$ is a morphism between Elgot algebras. This describes the category of strong pre-Elgot monads that we call $\strongpreelgot{\C}$.
-\end{definition}
+% Let us briefly introduce the category of (strong) pre-Elgot monads because the initial objects of these categories will be of special interest to us.
+
+% \begin{definition}[The Category of (Strong) Pre-Elgot Monads]
+%   Let $\C$ be a category. We define the category $\preelgot{\C}$ where objects are pre-Elgot monads and morphisms between pre-Elgot monads are morphisms between monads as in \autoref{def:monads} and additionally every $\alpha_X$ is a morphism between Elgot algebras as in \autoref{def:elgotalgebras}.
+
+%   Similarly, morphisms between strong pre-Elgot Monads are morphisms between strong monads as in \autoref{def:strongmonads} and every $\alpha_X$ is a morphism between Elgot algebras. This describes the category of strong pre-Elgot monads that we call $\strongpreelgot{\C}$.
+% \end{definition}
 
 \todo[inline]{Initial pre-Elgot bridges gap to Elgot monads under countable choice\ldots}
 
@@ -233,44 +261,102 @@ In this section we will study the monad that arises from existence of all free E
   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:
+We will need a notion of stability for $\mathbf{K}$ to make progress, since we do not assume $\C$ to be cartesian closed.
 
 \begin{definition}[Right-Stable Free Elgot Algebra]\label{def:rightstablefreeelgot}
-  Let $KY$ be a free Elgot algebra on $Y \in \obj{\C}$. We call $KY$ \textit{right-stable} if for every $A \in \elgotalgs{\C}$ and $f : X \times Y \rightarrow A$ there exists a unique $f^{\sharp_r} : X \times KY \rightarrow A$ satisfying:
-  \begin{alignat*}{1}
-    &f = f^{\sharp_r} \circ (id \times \eta)\tag*{($\sharp_r 1$)}\label{sharpr1}\\
-    &f^{\sharp_r} \circ (id \times h^\#) = ((f + id) \circ dstl \circ (id \times h))^\#\tag*{($\sharp_r 2$)}\label{sharpr2}
-  \end{alignat*}
-  We also call the property that \ref{sharpr2} establishes \textit{right iteration preserving}.
+  Let $KY$ be a free Elgot algebra on $Y \in \obj{\C}$. We call $KY$ \textit{right-stable} if for every $A \in \elgotalgs{\C}, X \in \obj{\C}$, and $f : X \times Y \rightarrow A$ there exists a unique right iteration preserving $\rs{f} : X \times KY \rightarrow A$ such that
+  % https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIFxcdGltZXMgWSJdLFsyLDAsIkEiXSxbMCwyLCJYIFxcdGltZXMgS1kiXSxbMCwxLCJmIl0sWzAsMiwiaWRcXHRpbWVzXFxldGEiLDJdLFsyLDEsIlxccnN7Zn0iLDJdXQ==
+  \[\begin{tikzcd}[ampersand replacement=\&]
+    {X \times Y} \&\& A \\
+    \\
+    {X \times KY}
+    \arrow["f", from=1-1, to=1-3]
+    \arrow["id\times\eta"', from=1-1, to=3-1]
+    \arrow["{\rs{f}}"', from=3-1, to=1-3]
+  \end{tikzcd}\]
+  commutes.
 \end{definition}
 
-We obtain the following dual definition:
+A symmetrical variant of the previous definition is sometimes useful.
 
 \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:
-  \begin{alignat*}{1}
-    &f = f^{\sharp_l} \circ (\eta \times id)\tag*{($\sharp_l 1$)}\label{sharpl1}\\
-    &f^{\sharp_l} \circ (h^\# \times id) = ((f + id) \circ dstr \circ (h \times id))^\#\tag*{($\sharp_l 2$)}\label{sharpl2}
-  \end{alignat*}
-  We also call the property that \ref{sharpl2} establishes \textit{left iteration preserving}.
+  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}, X \in \obj{\C}$, and $f : Y \times X \rightarrow A$ there exists a unique left iteration preserving $\ls{f} : KY \times X \rightarrow A$ such that
+  % https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIFxcdGltZXMgWSJdLFsyLDAsIkEiXSxbMCwyLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJmIl0sWzAsMiwiXFxldGFcXHRpbWVzIGlkIiwyXSxbMiwxLCJcXGxze2Z9IiwyXV0=
+  \[\begin{tikzcd}[ampersand replacement=\&]
+    {X \times Y} \&\& A \\
+    \\
+    {KX \times Y}
+    \arrow["f", from=1-1, to=1-3]
+    \arrow["{\eta\times id}"', from=1-1, to=3-1]
+    \arrow["{\ls{f}}"', from=3-1, to=1-3]
+  \end{tikzcd}\]
+  commutes.
 \end{definition}
 
 \begin{lemma}
   Definitions \ref{def:rightstablefreeelgot} and \ref{def:leftstablefreeelgot} are equivalent in the sense that they imply each other.
 \end{lemma}
-\begin{proof} We show that we can derive both operators from each other, the full proof that the laws are satisfied is not very insightful and as such we just refer to the formalization.
+\begin{proof} Let $(KY, (-)^{\#_y})$ be a left stable free Elgot algebra on $Y \in \obj{\C}$. Furthermore, let $A \in \elgotalgs{\C}, X \in \obj{\C}, f : Y \times X \rightarrow A$.
+  
+  We take $\rs{f} := \ls{f \circ swap} \circ swap$, which is indeed right iteration preserving, since
+  \begin{alignat*}{1}
+    &\rs{f} \circ (id \times h^{\#_y})
+    \\=\;&\ls{f \circ swap} \circ swap \circ (id \times h^{\#_y})
+    \\=\;&\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}
+  \end{alignat*}
+  for any $Z \in \obj{\C}, h : Z \rightarrow KY + Z$.
 
-  \begin{itemize}
-    \item[$"\Rightarrow"$]\;\\
-    Given a left-stable free Elgot algebra $KY$ with an iteration operator $(-)^{\sharp_l}$, then $KY$ is also right-stable with the iteration operator $f^{\sharp_r} := (f \circ swap)^{\sharp_l} \circ swap$.
-    \item[$"\Leftarrow"$]\;\\
-    Dually given a right-stable free Elgot Algebra $KY$ with an iteration operator $(-)^{\sharp_r}$, then $KY$ is also left-stable with the iteration operator $f^{\sharp_l} := (f \circ swap)^{\sharp_r} \circ swap$.
-  \end{itemize}
+  Where the application of \ref{law:uniformity} is justified by
+  \begin{alignat*}{1}
+    &(id + swap) \circ ((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h)
+    \\=\;&((\ls{f \circ swap} \circ swap) + swap) \circ dstl \circ (id \times h)
+    \\=\;&(\ls{f \circ swap} + id) \circ (swap + swap) \circ dstl \circ (id \times h)
+    \\=\;&(\ls{f \circ swap} + id) \circ dstr \circ swap \circ (id \times h)
+    \\=\;&(\ls{f \circ swap} + id) \circ dstr \circ (h \times id) \circ swap.
+  \end{alignat*}
+
+  The diagram commutes, since
+  \begin{alignat*}{1}
+    &\rs{f} \circ (id \times \eta)
+    \\=\;&\ls{f \circ swap} \circ swap \circ (id \times \eta)
+    \\=\;&\ls{f \circ swap} \circ (\eta \times id) \circ swap
+    \\=\;&f \circ swap \circ swap
+    \\=\;&f.
+  \end{alignat*}
+  
+  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,
+  \end{alignat*}
+  and
+  \begin{alignat*}{1}
+    &g \circ swap \circ (h^{\#_y} \times id)
+    \\=\;&g \circ (id \times h^{\#_y}) \circ swap
+    \\=\;&((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*}
+
+  where 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
+  \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.
 \end{proof}
 
-We will usually refer to right-stable free Elgot algebras as just stable Elgot algebras and omit the index of the operator.
+The following theorem illustrates that stability of $KX$ indeed simulates the behavior of $KX$ in a cartesian closed category.
 
-Stability of $KX$ expresses that it behaves like it would in a cartesian closed category, the following theorem illustrates this.
+\todo[inline]{Fix proof, replace free object operator, fix references.}
 
 \begin{theorem}\label{thm:stability}
   In a cartesian closed category every free Elgot algebra is stable.
@@ -279,7 +365,7 @@ Stability of $KX$ expresses that it behaves like it would in a cartesian closed
   Let $X \in \obj{\C}$ and $((KX, (-)^\#), \llbracket - \rrbracket)$ be a free Elgot algebra on $X$.
 
   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
-  $f^{\sharp_l} := eval \circ (\llbracket curry\;f \rrbracket \times id)$. 
+  $\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: