leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Finishing touches for iteration chapter

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-15 10:10:25 +01:00
parent 1a6f409cd1
commit 2dbf69bcf6
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 174 additions and 166 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
thesis/src/02_preliminaries.tex
View file

@ -177,7 +177,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\]
\end{definition}
\begin{lemma}
\begin{proposition}
Every exponential object \(X^Y\) satisfies the following properties:
\begin{enumerate}
@ -185,7 +185,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\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\)
\end{enumerate}
\end{lemma}
\end{proposition}
\begin{proof}
\begin{enumerate}
\item Let \(f, g : X \times Y \rightarrow Z\) and \(curry\;f = curry\;g\), then indeed
@ -394,8 +394,8 @@ This yields the category of programs for a Kleisli triple that is called the Kle
The laws of categories then follow from the Kleisli triple laws.
\end{definition}
\begin{theorem}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
\end{theorem}
\begin{proposition}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
\end{proposition}
\begin{proof}
The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out.
@ -505,10 +505,10 @@ to establish some notation and then describe how to obtain a monad via existence
\]
\end{definition}
\begin{theorem}\label{thm:freemonad}
\begin{proposition}\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}
\end{proposition}
\begin{proof}
We are left to check the laws of Kleisli triples.

328
thesis/src/05_iteration.tex
View file

@ -40,8 +40,11 @@ The previous intuition gives rise to the following simpler definition that has b
\end{itemize}
\end{definition}
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 illustrated by the following Lemma. % chktex 2
Note that the \ref{law:uniformity} axiom requires an identity to be proven, before it can be applied. % chktex 2
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
\begin{lemma}
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional axioms
@ -176,46 +179,46 @@ Let us now consider morphisms that are coherent with respect to the iteration op
for any \(h : Y \rightarrow A + Y\).
\end{definition}
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}\).
We will now study the category of Elgot algebras and iteration preserving morphisms that we call \(\elgotalgs{\C}\). Let us introduce notation for morphisms between Elgot algebras: we denote an Elgot algebra morphism \(f : (A , {(-)}^{\sharp_a}) \rightarrow (B,{(-)}^{\sharp_b})\) as \(f : A \hookrightarrow B\), where we omit stating the iteration operator.
\begin{lemma}
\begin{lemma}\label{lem:elgotalgscat}
\(\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 , {(-)}^{\sharp_a}), (B , {(-)}^{\sharp_b}), (C , {(-)}^{\sharp_c})\) be Elgot algebras.
Let \(A, B\) and \(C\) be Elgot algebras.
The identity trivially satisfies
\[id \circ f^{\sharp_a} = f^{\sharp_a} = {((id + id) \circ f)}^{\sharp_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
Given two iteration preserving morphisms \(f : B \hookrightarrow C, g : A \hookrightarrow B\), the composite is iteration preserving since
\begin{alignat*}{1}
& f \circ g \circ h^{\sharp_a}
\\=\;& f \circ {((g + id) \circ h)}^{\sharp_b}
\\=\;&{((f + id) \circ (g + id) \circ h)}^{\sharp_c}
\\=\;&{(((f \circ g) + id) \circ h)}^{\sharp_c}
\\=\;&{((f \circ g + id) \circ h)}^{\sharp_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.
Products and exponentials of Elgot algebras can be formed in a canonical way, which is illustrated by the following two Lemmas.
\begin{lemma}\label{lem:elgotalgscat}
\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
Let \((A, {(-)}^{\sharp_a}) , (B, {(-)}^{\sharp_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^\sharp = \langle ((\pi_1 + id) \circ f)^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle : X \rightarrow A \times B\]
Next we show that \((A \times B, {(-)}^\sharp)\) is indeed an Elgot algebra:
Let \(A, 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^\sharp = \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle : X \rightarrow A \times B\]
Now, we show that \(A \times B\) indeed constitutes an Elgot algebra:
\begin{itemize}
\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)^{\sharp_a}\) and \({((\pi_2 + id) \circ f)}^{\sharp_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)}^{\sharp_a}\) and \({((\pi_2 + id) \circ f)}^{\sharp_b}\):
\begin{alignat*}{1}
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle
\\=\;&\langle [ id , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ (\pi_1 + id) \circ f
\\ &, [ id , ((\pi_2 + id) \circ f)^{\sharp_b} ] \circ (\pi_2 + id) \circ f \rangle \tag{\ref{law:fixpoint}}
\\ &, [ id , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \circ (\pi_2 + id) \circ f \rangle \tag{\ref{law:fixpoint}}
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ f , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \circ f \rangle
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \rangle \circ f
\\=\;&[ \langle \pi_1 , \pi_2 \rangle , \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle ] \circ f
@ -253,90 +256,94 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
and
\begin{alignat*}{1}
& {((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_b}
\\=\;&{(((\pi_2 + id) \circ f)^{\sharp_b} + h)}^{\sharp_b}
\\=\;&{({((\pi_2 + id) \circ f)}^{\sharp_b} + h)}^{\sharp_b}
\\=\;&{[ (id + i_1) \circ (\pi_2 + id) \circ f , i_2 \circ h ]}^{\sharp_b}\tag{\ref{law:folding}}
\\=\;&(\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_b}
\end{alignat*}
which concludes the proof of the folding law.
\end{itemize}
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, {(-)}^{\sharp_z}) \rightarrow (X, {(-)}^{\sharp_x}), g : (Z, {(-)}^{\sharp_z}) \rightarrow (Y, {(-)}^{\sharp_y})\):
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 : C \hookrightarrow A, g : C \rightarrow B\) where \(C \in \obj{\elgotalgs{\C}}\).
Let \(h : X \rightarrow E + X\) where \(E \in \obj{\elgotalgs{\C}}\). We use the fact that \(f, g\) are iteration preserving to show:
Let \(h : X \rightarrow C + X\). We use the fact that \(f\) and \(g\) are iteration preserving to show:
\begin{alignat*}{1}
& \langle f , g \rangle \circ (h^{\sharp_e})
\\=\;&\langle f \circ (h^{\sharp_e}) , g \circ (h^{\sharp_e}) \rangle
\\=\;&\langle ((f + id) \circ h)^{\sharp_a} , ((g + id) \circ h)^{\sharp_b} \rangle
\\=\;&\langle ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\sharp_a} , ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\sharp_b} \rangle
& \langle f , g \rangle \circ (h^{\sharp_c})
\\=\;&\langle f \circ (h^{\sharp_c}) , g \circ (h^{\sharp_c}) \rangle
\\=\;&\langle {((f + id) \circ h)}^{\sharp_a} , {((g + id) \circ h)}^{\sharp_b} \rangle
\\=\;&\langle {((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_a} , {((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_b} \rangle
\end{alignat*}
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, we have shown that \(A \times B\) extends to a product in \(\elgotalgs{\C}\) and therefore \(\elgotalgs{\C}\) is Cartesian, assuming that \(\C\) is Cartesian.
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, it follows that \(A \times B\) extends to a product in \(\elgotalgs{\C}\) and therefore \(\elgotalgs{\C}\) is Cartesian, if \(\C\) is Cartesian.
\end{proof}
\begin{lemma}\label{lem:elgotexp}
Given \(X \in \obj{\C}\) and \((A, {(-)}^{\sharp_a}) \in \vert\elgotalgs{\C}\vert \). The exponential \(X^A\) (if it exists) can be equipped with an Elgot algebra structure.
Given \(X \in \obj{\C}\) and \(A \in \obj{\elgotalgs{\C}} \). The exponential \(X^A\) (if it exists) can be equipped with an Elgot algebra structure.
\end{lemma}
\begin{proof}
Take \(f^\sharp = curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a})\) as the iteration of some \(f : Z \rightarrow A^X + Z\).
Take \(f^\sharp = curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_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^\sharp = curry\;(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a})\) it suffices to show:
\item \textbf{Fixpoint}: Let \(f : Y \rightarrow X^A + Y\). We need to show that \(f^\sharp = [ id , f^\sharp ] \circ f\), which follows by uniqueness of \[f^\sharp = curry\;({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a})\] and
\begin{alignat*}{1}
& eval \circ ([ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \circ f] \times id)
\\=\;&eval \circ [ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr \circ (f \times id)\tag*{\ref{hlp:elgot_exp_fixpoint}}
\\=\;&[ eval , eval \circ curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr \circ (f \times id)
\\=\;&[ eval , ((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} ] \circ dstr \circ (f \times id)
\\=\;&[ id , ((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} ] \circ (eval + id) \circ dstr \circ (f \times id)
\\=\;&((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}\tag{\ref{law:fixpoint}}
& eval \circ ([ id , curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ f \times id)
\\=\;&eval \circ [ id , curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr \circ (f \times id)\tag*{\ref{hlp:elgot_exp_fixpoint}}
\\=\;&[ eval , eval \circ (curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr \circ (f \times id)
\\=\;&[ eval , {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} ] \circ dstr \circ (f \times id)
\\=\;&[ id , {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} ] \circ (eval + id) \circ dstr \circ (f \times id)
\\=\;&{((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a},\tag{\ref{law:fixpoint}}
\end{alignat*}
Where
where
\begin{alignat*}{1}
& [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \times id
\\= \;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr \tag*{(*)}\label{hlp:elgot_exp_fixpoint}
& [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \times id
\\= \;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr \tag*{(*)}\label{hlp:elgot_exp_fixpoint}
\end{alignat*}
follows by post-composing with \(\pi_1\) and \(\pi_2\):
follows by post-composing with \(\pi_1\) and \(\pi_2\), indeed:
\begin{alignat*}{1}
& \pi_1 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
\\=\;&[ \pi_1 , \pi_1 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
\\=\;&[ \pi_1 , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \circ \pi_1 ] \circ dstr
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \circ (\pi_1 + \pi_1) \circ dstr
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \circ \pi_1
& \pi_1 \circ [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr
\\=\;&[ \pi_1 , \pi_1 \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr
\\=\;&[ \pi_1 , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \circ \pi_1 ] \circ dstr
\\=\;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ (\pi_1 + \pi_1) \circ dstr
\\=\;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ \pi_1,
\end{alignat*}
and
\begin{alignat*}{1}
& \pi_2 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
\\=\;&[ \pi_2 , \pi_2 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
& \pi_2 \circ [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr
\\=\;&[ \pi_2 , \pi_2 \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr
\\=\;&[ \pi_2 , \pi_2 ] \circ dstr
\\=\;&\pi_2
\\=\;&\pi_2.
\end{alignat*}
\item \textbf{Uniformity}: Let \(Y, Z \in \obj{C}, f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z\) and \((id + h) \circ f = g \circ h\). By uniqueness of \(f^\sharp = curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a})\) it suffices to show:
\item \textbf{Uniformity}: Let \(f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z\) and \((id + h) \circ f = g \circ h\). Again, by uniqueness of \(f^\sharp = curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a})\) it suffices to show:
\begin{alignat*}{1}
& ((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}
\\=\;&((eval + id) \circ dstr \circ (g \times id))^{\sharp_a} \circ (h \times id)\tag{\ref{law:uniformity}}
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\sharp_a} \times id) \circ (h \times id)
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\sharp_a} \circ h \times id)
& {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}
\\=\;&{((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \circ (h \times id)\tag{\ref{law:uniformity}}
\\=\;&eval \circ ({((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \times id) \circ (h \times id)
\\=\;&eval \circ ({((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \circ h \times id)
\end{alignat*}
Note that the application of \ref{law:uniformity} requires:
Note that the application of \ref{law:uniformity} requires: % chktex 2
\begin{alignat*}{1}
& (id + (h \times id)) \circ (eval + id) \circ dstr \circ (f \times id)
\\=\;&(eval + id) \circ (id + (h \times id)) \circ dstr \circ (f \times id)
\\=\;&(eval + id) \circ dstr \circ (id \times h) \circ (id \times id) \circ (f \times id)
\\=\;&(eval + id) \circ dstr \circ (g \times id) \circ (h \times id)
\end{alignat*}
\item \textbf{Folding}: Let \(Y, Z \in \obj{C}, f : Y \rightarrow X^A + Y, h : Y \rightarrow Z\).
\item \textbf{Folding}: Let \(f : Y \rightarrow X^A + Y, h : Y \rightarrow Z\). We need to show that
\begin{alignat*}{1}
& (f^\sharp + h)^\sharp
\\=\;&curry(((eval + id) \circ dstr \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) + h) \times id))^{\sharp_a})
\\=\;&curry(((eval + id) \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id) + (h \times id)) \circ dstr)^{\sharp_a})
\\=\;&curry(((eval \circ (curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id) + (h \times id)) \circ dstr)^{\sharp_a})
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} + (h \times id)) \circ dstr)^{\sharp_a})
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} + dstr \circ (h \times id)))^{\sharp_a} \circ dstr)\tag{\ref{law:uniformity}}
\\=\;&curry([ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr)\tag{\ref{law:folding}}
\\=\;&curry(((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))^{\sharp_a})\tag{\ref{law:uniformity}}
\\=\;&[ (id + i_1) \circ f , i_2 \circ h ]^\sharp
& {(f^\sharp + h)}^\sharp
\\=\;&curry({((eval + id) \circ dstr \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) + h) \times id))}^{\sharp_a})
\\=\;&curry({((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))}^{\sharp_a})
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp.
\end{alignat*}
\
The second application of~\ref{law:uniformity} is non-trivial, using epicness of \(dstr^{-1}\):
Indeed, we are done by:
\begin{alignat*}{1}
& {((eval + id) \circ dstr \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) + h) \times id))}^{\sharp_a}
\\=\;&{((eval + id) \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) + (h \times id)) \circ dstr)}^{\sharp_a}
\\=\;&{((eval \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) + (h \times id)) \circ dstr)}^{\sharp_a}
\\=\;&{(({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} + (h \times id)) \circ dstr)}^{\sharp_a}
\\=\;&{(({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} + dstr \circ (h \times id)))}^{\sharp_a} \circ dstr\tag{\ref{law:uniformity}}
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr\tag{\ref{law:folding}}
\\=\;&{((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))}^{\sharp_a}.\tag{\ref{law:uniformity}}
\end{alignat*}
Note that the second application of~\ref{law:uniformity} is non-trivial, using epicness of \(dstr^{-1}\):
\begin{alignat*}{1}
& (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ dstr^{-1}
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_1 \times id)
@ -354,7 +361,7 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
\end{proof}
\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 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 strong pre-Elgot monad. Starting in this section we will now omit indices of the iteration operator of Elgot algebras for the sake of readability.
Let us first recall the following notion that was introduced in~\cite{elgotmonad} and reformulated in~\cite{uniformelgot}.
\begin{definition}[Elgot Monad]
@ -382,7 +389,7 @@ The following notion has been introduced in~\cite{uniformelgot} as a weaker appr
\begin{definition}[Pre-Elgot Monad]
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 right iteration preserving we call it strong pre-Elgot.
If the monad \(\mathbf{T}\) is additionally strong and the strength \(\tau \) is right iteration preserving we call \(\mathbf{T}\) strong pre-Elgot.
\end{definition}
(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:monadmorphism} such that additionally each \(\alpha_X\) is iteration preserving. Similarly, morphisms between strong pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:strongmonadmorphism} such that each \(\alpha_X\) is iteration preserving. We call these categories \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) respectively.
@ -443,16 +450,16 @@ A symmetrical variant of the previous definition is sometimes useful.
\begin{lemma}
Definitions~\ref{def:rightstablefreeelgot} and~\ref{def:leftstablefreeelgot} are equivalent in the sense that they imply each other.
\end{lemma}
\begin{proof} Let \((KY, {(-)}^{\sharp_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\).
\begin{proof} Let \(KY\) be a left stable free Elgot algebra on \(Y \in \obj{\C}\). Furthermore, let \(A\) be an Elgot algebra and \(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^{\sharp_y})
\\=\;&\ls{f \circ swap} \circ swap \circ (id \times h^{\sharp_y})
\\=\;&\ls{f \circ swap} \circ (h^{\sharp_y} \times id) \circ swap
\\=\;&((\ls{f \circ swap} + id) \circ dstr \circ (id \times h))^{\sharp_a} \circ swap
\\=\;&(((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h))^{\sharp_a}\tag{\ref{law:uniformity}}
\\=\;&(((\rs{f} + id) \circ dstl \circ (id \times h))^{\sharp_a},
& \rs{f} \circ (id \times h^\sharp)
\\=\;&\ls{f \circ swap} \circ swap \circ (id \times h^\sharp)
\\=\;&\ls{f \circ swap} \circ (h^\sharp \times id) \circ swap
\\=\;&{((\ls{f \circ swap} + id) \circ dstr \circ (id \times h))}^\sharp \circ swap
\\=\;&{((\ls{f \circ swap} \circ swap + id) \circ dstl \circ (id \times h))}^\sharp\tag{\ref{law:uniformity}}
\\=\;&{((\rs{f} + id) \circ dstl \circ (id \times h))}^\sharp,
\end{alignat*}
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
@ -484,10 +491,10 @@ A symmetrical variant of the previous definition is sometimes useful.
\end{alignat*}
and
\begin{alignat*}{1}
& g \circ swap \circ (h^{\sharp_y} \times id)
\\=\;&g \circ (id \times h^{\sharp_y}) \circ swap
\\=\;&((g + id) \circ dstl \circ (id \times h))^{\sharp_a} \circ swap
\\=\;&(((g \circ swap) + id) \circ dstr \circ (h \times id))^{\sharp_a},\tag{\ref{law:uniformity}}
& g \circ swap \circ (h^\sharp \times id)
\\=\;&g \circ (id \times h^\sharp) \circ swap
\\=\;&{((g + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
\\=\;&{((g \circ swap + id) \circ dstr \circ (h \times id))}^\sharp,\tag{\ref{law:uniformity}}
\end{alignat*}
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
@ -499,34 +506,34 @@ A symmetrical variant of the previous definition is sometimes useful.
% \\=\;&(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 symmetrically.
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{theorem}\label{thm:stability}
\begin{lemma}\label{thm:stability}
In a Cartesian closed category every free Elgot algebra is stable.
\end{theorem}
\end{lemma}
\begin{proof}
Let \(\C\) be Cartesian closed and let \((KX, {(-)}^\sharp, \free{(-)})\) be a free Elgot algebra on some \(X \in \obj{\C}\).
Let \(\C\) be Cartesian closed and let \(KX\) be a free Elgot algebra on some \(X \in \obj{\C}\).
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\).
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)
\\=\;&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^{\sharp_a} \times id)
\\=\;&eval \circ ((\free{curry\;f} \circ h^{\sharp_a}) \times id)
\\=\;&eval \circ (curry(((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\sharp_b})) \times id)
\\=\;&((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\sharp_b}
\\=\;&((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))^{\sharp_b}
\\=\;&((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))^{\sharp_b}
\\=\;&(((eval \circ (\free{curry\;f} \times id)) + id) \circ dstr \circ (h \times id))^{\sharp_b}.
& eval \circ (\free{curry\;f} \times id) \circ (h^\sharp \times id)
\\=\;&eval \circ (\free{curry\;f} \circ h^\sharp \times id)
\\=\;&eval \circ (curry({((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))}^\sharp) \times id)
\\=\;&{((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \circ h \times id))}^\sharp
\\=\;&{((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))}^\sharp
\\=\;&{((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))}^\sharp
\\=\;&{((eval \circ (\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))}^\sharp.
\end{alignat*}
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
@ -540,13 +547,13 @@ In a less general setting stability would indeed follow automatically.
Indeed,
\begin{alignat*}{1}
& curry\;g \circ h^{\sharp}
\\=\;&curry\;(g \circ (h^{\sharp} \times id))
\\=\;&curry\;(((g + id) \circ dstr \circ (h \times id))^{\sharp_a})
\\=\;&curry\;((((eval \circ (curry\; g \times id)) + id) \circ dstr \circ (h \times id))^{\sharp_a})
\\=\;&curry\;(((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))^{\sharp_a})
\\=\;&curry\;(((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))^{\sharp_a})
\\=\;&curry\;(((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))^{\sharp_a})
& curry\;g \circ h^\sharp
\\=\;&curry\;(g \circ (h^\sharp \times id))
\\=\;&curry\;({((g + id) \circ dstr \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval \circ (curry\; g \times id) + id) \circ dstr \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))}^\sharp)
\end{alignat*}
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\), and
\begin{alignat*}{1}
@ -555,7 +562,7 @@ In a less general setting stability would indeed follow automatically.
\\=\;&curry\;f
\end{alignat*}
This completes the proof.
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.
@ -599,9 +606,9 @@ Of course there is also a symmetric version of this.
\(\mathbf{K}\) is a strong monad.
\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 \(\tau\) is right iteration preserving by definition and \(\tau \circ (id \times \eta) = \eta\).
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, 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.
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:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
@ -623,9 +630,9 @@ Of course there is also a symmetric version of this.
Notably, \(\tau \circ (f \times Kg)\) is right iteration preserving, since for any \(Z : \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)
\\=\;&((\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)))^\sharp \circ (f \times id)
\\=\;&(((\tau \circ (f \times Kg)) + id) \circ dstl \circ (id \times h))^\sharp.\tag{\ref{law:uniformity}}
\\=\;&\tau \circ (f \times {((Kg + id) \circ h)}^\sharp)
\\=\;&{((\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)))}^\sharp \circ (f \times id)
\\=\;&{(((\tau \circ (f \times Kg)) + id) \circ dstl \circ (id \times h))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
% where uniformity is justified by
@ -650,7 +657,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 \(K\pi_2 \circ \tau = \pi_2\) holds more generally for any \(X, Y \in \obj{\C}\), instead of just for \(X = 1\):
\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:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
\[
\begin{tikzcd}
@ -666,7 +673,7 @@ Of course there is also a symmetric version of this.
\]
\item[\ref{S2}] As already mentioned, \(\tau \circ (id \times \eta) = \eta\) follows by definition of \(\tau\).
\item[\ref{S3}] To show that \(\tau \circ (id \times \mu) = \tau^* \circ \tau\), consider:
\item[\ref{S3}] To show that \(\tau \circ (id \times \mu) = \tau^* \circ \tau\), we will proceed by right-stability using:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS0tZIl0sWzMsMCwiWCBcXHRpbWVzIEtZIl0sWzMsMiwiSyhYXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFswLDMsIlggXFx0aW1lcyBLWSJdLFswLDEsImlkIFxcdGltZXMgXFxtdSIsMl0sWzEsMiwiXFx0YXUiLDJdLFswLDMsIlxcdGF1Il0sWzMsMiwiXFx0YXVeKiJdLFs0LDAsImlkIFxcdGltZXMgXFxldGEiLDAseyJjdXJ2ZSI6LTJ9XSxbNCwyLCJcXHRhdSIsMCx7ImN1cnZlIjoyfV1d
\[
\begin{tikzcd}
@ -682,7 +689,7 @@ Of course there is also a symmetric version of this.
\arrow["\tau", curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}
\]
\item[\ref{S4}] Lastly, consider the following diagram:
\item[\ref{S4}] Lastly, consider the following diagram for the proof by right-stability:
% https://q.uiver.app/#q=WzAsNixbMSwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgS1oiXSxbMSwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIEtZIl0sWzMsMCwiSygoWCBcXHRpbWVzIFkpIFxcdGltZXMgWikiXSxbMywyLCJLKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgSyhZIFxcdGltZXMgWikiXSxbMCwzLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgWiJdLFswLDEsIlxcYWxwaGEiXSxbMiwzLCJLXFxhbHBoYSJdLFswLDIsIlxcdGF1Il0sWzEsNCwiaWQgXFx0aW1lc1xcdGF1Il0sWzQsMywiXFx0YXUiXSxbNSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzUsMywiXFxldGEgXFxjaXJjIFxcYWxwaGEiLDIseyJjdXJ2ZSI6Mn1dXQ==
\[
\begin{tikzcd}
@ -699,17 +706,16 @@ 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\):
\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)
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , h^\sharp \circ \pi_2 \rangle \rangle
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ (id \times h^\sharp) \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , ((\tau + id) \circ dstl \circ (id \times h))^\sharp \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
\\=\;&\tau \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))^\sharp) \circ \alpha
\\=\;&((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))^\sharp \circ \alpha
\\=\;&(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))^\sharp.\tag{\ref{law:uniformity}}
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , {((\tau + id) \circ dstl \circ (id \times h))}^\sharp \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
\\=\;&\tau \circ (id \times {((\tau + id) \circ dstl \circ (id \times h))}^\sharp) \circ \alpha
\\=\;&{((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))}^\sharp \circ \alpha
\\=\;&{(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
\end{itemize}
Thus, strength of \(\mathbf{K}\) has been proven.
@ -739,9 +745,9 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
& \sigma \circ (h^\sharp \times id)
\\=\;&Kswap \circ \tau \circ swap \circ (h^\sharp \times id)
\\=\;&Kswap \circ \tau \circ (id \times h^\sharp) \circ swap
\\=\;&Kswap \circ ((\tau + id) \circ dstl \circ (id \times h))^\sharp \circ swap
\\=\;&(((Kswap \circ \tau) + id) \circ dstl \circ (id \times h))^\sharp \circ swap
\\=\;&((\sigma + id) \circ dstr \circ (h \times id))^\sharp.\tag{\ref{law:uniformity}}
\\=\;&Kswap \circ {((\tau + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
\\=\;&{(((Kswap \circ \tau) + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
\\=\;&{((\sigma + id) \circ dstr \circ (h \times id))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
Let us now proceed with the properties of \(\tau \) and \(\sigma \).
@ -766,16 +772,18 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
\\=\;&\sigma \circ (f^* \times g^*)
\end{alignat*}
\end{itemize}
This concludes the proof.
Thus, the proof has been concluded.
\end{proof}
The following Lemma is central to the proof of commutativity.
\begin{lemma}\label{lem:KCommKey} Given \(f : X \rightarrow KY + Z, g : Z \rightarrow KA + Z\),
\[\tau^* \circ \sigma \circ (((\eta + id) \circ f)^\sharp \times ((\eta + id) \circ g)^\sharp) = \sigma^* \circ \tau \circ (((\eta + id) \circ f)^\sharp \times ((\eta + id) \circ g)^\sharp).\]
\begin{lemma}\label{lem:KCommKey} Given \(f : X \rightarrow KY + X, g : Z \rightarrow KA + Z\),
\[\tau^* \circ \sigma \circ ({((\eta + id) \circ f)}^\sharp \times {((\eta + id) \circ g)}^\sharp) = \sigma^* \circ \tau \circ ({((\eta + id) \circ f)}^\sharp \times {((\eta + id) \circ g)}^\sharp).\]
\end{lemma}
\begin{proof}
Let us abbreviate \(\hat{f} := (\eta + id) \circ f\) and \(\hat{g} := (\eta + id) \circ g\). It suffices to find a \(w : ?\) such that \(\hat{f}^\sharp \circ \pi_1 = [ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\sharp\) and \(\hat{g}^\sharp \circ \pi_2 = [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^* \circ w^\sharp \), then
Let us abbreviate \(\hat{f} := (\eta + id) \circ f\) and \(\hat{g} := (\eta + id) \circ g\). It suffices to find a
\[w : X \times Z \rightarrow K(X \times KA + KY \times Z) + X \times Z\]
such that \(\hat{f}^\sharp \circ \pi_1 = [ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\sharp\) and \(\hat{g}^\sharp \circ \pi_2 = [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^* \circ w^\sharp \), because then
\begin{alignat*}{1}
& \tau^* \circ \sigma \circ (\hat{f}^\sharp \times \hat{g}^\sharp)
\\=\;&\tau^* \circ \sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\sharp \times w^\sharp)
@ -796,11 +804,11 @@ The following Lemma is central to the proof of commutativity.
and by a symmetric argument also
\[\sigma^* \circ \tau \circ (\hat{f}^\sharp \times \hat{g}^\sharp) = ([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ {(id \times \hat{g}^\sharp)])}^* \circ w^\sharp.\]
Note that we are referencing \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity.
Note that we are referencing the equational lifting law established in \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, since we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity, this does not pose a problem.
We are thus left to find such a \(w\), consider
\[w := [ i_1 \circ K i_1 \circ \tau , ((K i_2 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}). \]
\(w\) indeed satisfies the requisite properties, let us check the first property, the second one follows by a symmetric argument. We will show that
\(w\) indeed satisfies the requisite properties, let us check the first property, the second one follows by a symmetric argument. We need to show that
\[[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\sharp = ([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\sharp = \hat{f}^\sharp \circ \pi_1. \]
Indeed,
\begin{alignat*}{1}
@ -836,7 +844,7 @@ The following Lemma is central to the proof of commutativity.
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\sharp,
\end{alignat*}
where \(h = (\pi_1 + ((\pi_1 + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)\) and the application of \ref{law:uniformity} is justified, since
where \(h = (\pi_1 + (\pi_1 + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle) \circ dstr \circ (\hat{f} \times id)\) and the application of \ref{law:uniformity} is justified, since % chktex 2
\begin{alignat*}{1}
& (id + \pi_1) \circ (id + \Delta) \circ h
\\=\;&(\pi_1 + ((\pi_1 \circ [ \pi_1 , \pi_1 \times id ]) \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
@ -850,9 +858,9 @@ The following Lemma is central to the proof of commutativity.
This concludes the proof.
\end{proof}
\begin{theorem}
\begin{lemma}
\(\mathbf{K}\) is a commutative monad.
\end{theorem}
\end{lemma}
\begin{proof} We need to show that \(\tau^* \circ \sigma = \sigma^* \circ \tau : KX \times KY \rightarrow K(X \times Y)\).
Let us proceed by right stability, consider the following diagram.
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJLWCBcXHRpbWVzIEtZIl0sWzMsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzEsMiwiSyhYIFxcdGltZXMgS1kpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMCwzLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdSJdLFswLDIsIlxcaGF0e1xcdGF1fSIsMl0sWzEsMywiXFxoYXR7XFx0YXV9XioiXSxbMiwzLCJcXHRhdV4qIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMywiXFxoYXR7XFx0YXV9IiwyLHsiY3VydmUiOjJ9XV0=
@ -874,10 +882,10 @@ The following Lemma is central to the proof of commutativity.
The diagram commutes since
\[\sigma^* \circ \tau \circ (id \times \eta) = \sigma^* \circ \eta = \sigma \]
and
\[\tau^* \circ \sigma \circ (id \times \eta) = \tau^* \circ K(id \times \eta) \circ \sigma = (\tau \circ {(id \times \eta))}^* \circ \sigma = \sigma.\]
\[\tau^* \circ \sigma \circ (id \times \eta) = \tau^* \circ K(id \times \eta) \circ \sigma = {(\tau \circ (id \times \eta))}^* \circ \sigma = \sigma.\]
We are left to show that both \(\sigma^* \circ \tau \) and \(\tau^* \circ \sigma \) are right iteration preserving. Let \(h : Z \rightarrow KY + Z\), indeed
\[\sigma^* \circ \tau \circ (id \times h^\sharp) = \sigma^* ((\tau + id) \circ dstl \circ (id \times h))^\sharp = (((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))^\sharp. \]
\[\sigma^* \circ \tau \circ (id \times h^\sharp) = \sigma^* {((\tau + id) \circ dstl \circ (id \times h))}^\sharp = {(((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))}^\sharp. \]
Let \(\psi := \tau^* \circ \sigma \) and let us proceed by left stability to show that \(\psi \) is right iteration preserving, consider the following diagram
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
@ -904,50 +912,50 @@ The following Lemma is central to the proof of commutativity.
\\=\;&((\psi + id) \circ dstl \circ (id \times h))^\sharp \circ (\eta \times id).\tag{\ref{law:uniformity}}
\end{alignat*}
We are left to show that both \(\psi \circ (id \times h^\sharp)\) and \(((\psi + id) \circ dstl \circ (id \times h))^\sharp \) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi \circ (id \times h^\sharp)\) is left iteration preserving, since
We are left to show that both \(\psi \circ (id \times h^\sharp)\) and \({((\psi + id) \circ dstl \circ (id \times h))}^\sharp \) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi \circ (id \times h^\sharp)\) is left iteration preserving, since
\begin{alignat*}{1}
& \psi \circ (id \times h^\sharp) \circ (g^\sharp \times id)
\\=\;&\psi \circ (g^\sharp \times id) \circ (id \times h^\sharp)
\\=\;&\tau^* \circ ((\sigma + id) \circ dstr \circ (g \times id))^\sharp \circ (id \times h^\sharp)
\\=\;&((\psi + id) \circ dstr \circ (g \times id))^\sharp \circ (id \times h^\sharp)
\\=\;&(((\psi \circ (id \times h^\sharp)) + id) \circ dstr \circ (g \times id))^\sharp.\tag{\ref{law:uniformity}}
\\=\;&\tau^* \circ {((\sigma + id) \circ dstr \circ (g \times id))}^\sharp \circ (id \times h^\sharp)
\\=\;&{((\psi + id) \circ dstr \circ (g \times id))}^\sharp \circ (id \times h^\sharp)
\\=\;&{(((\psi \circ (id \times h^\sharp)) + id) \circ dstr \circ (g \times id))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
Lastly, we need to show that
\[((\psi + id) \circ dstl \circ (id \times h))^\sharp \circ (g^\sharp \times id) = ((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp.\]
\[{((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (g^\sharp \times id) = {(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp.\]
Note that by~\ref{law:uniformity} the left-hand side can be rewritten as
\[((((\psi + id) \circ dstr \circ (g \times id))^\sharp + id) \circ dstl \circ (id \times h))^\sharp.\]
\[{(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp.\]
Consider now, that
\begin{alignat*}{1}
& ((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp
\\=\;&(((((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))^\sharp
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ ((\eta + id) \circ dstr \circ (g \times id))^\sharp
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ (((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))^\sharp
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&(((\psi^* + id) \circ (\eta + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ ((((\tau \circ (id \times \eta)) + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ (((\tau + id) \circ dstl \circ (id \times ({(\eta + id) \circ h)))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ (\tau \circ (id \times ({(\eta + id) \circ h)^\sharp))}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ K(id \times ((\eta + id) \circ h)^\sharp) \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times ((\eta + id) \circ h)^\sharp) \circ (((\eta + id) \circ g)^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp),
& {(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{(({({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ {((\eta + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ {(((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&{({((\psi^* + id) \circ (\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({((\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({((\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({(((\tau \circ (id \times \eta)) + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({((\tau + id) \circ dstl \circ (id \times ((\eta + id) \circ h)))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {(\tau \circ (id \times {((\eta + id) \circ h)}^\sharp))}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ K(id \times {((\eta + id) \circ h)}^\sharp) \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times {((\eta + id) \circ h)}^\sharp) \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp),
\end{alignat*}
and by a symmetric argument
\begin{alignat*}{1}
& ((((\psi + id) \circ dstr \circ (g \times id))^\sharp + id) \circ dstl \circ (id \times h))^\sharp
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp).
& {(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp).
\end{alignat*}
We are thus done by
\begin{alignat*}{1}
& ((\psi + id) \circ dstl \circ (id \times h))^\sharp \circ (g^\sharp \times id)
\\=\;&((((\psi + id) \circ dstr \circ (g \times id))^\sharp + id) \circ dstl \circ (id \times h))^\sharp\tag{\ref{law:uniformity}}
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp)\tag{\autoref{lem:KCommKey}}
\\=\;&((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp.\tag*{\qedhere}
& {((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (g^\sharp \times id)
\\=\;&{(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp\tag{\ref{law:uniformity}}
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp)\tag{\autoref{lem:KCommKey}}
\\=\;&{(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp.\tag*{\qedhere}
\end{alignat*}
\end{proof}
@ -958,7 +966,7 @@ The following Lemma is central to the proof of commutativity.
\begin{proof}
Since we have already shown commutativity, we are left 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 the 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
The identity follows easily:
\begin{alignat*}{1}
& \tau \circ \Delta \circ \eta
\\=\;&\tau \circ \langle \eta , \eta \rangle
@ -971,8 +979,8 @@ The following Lemma is central to the proof of commutativity.
& \tau \circ \Delta \circ h^{\sharp}
\\=\;&\tau \circ \langle h^{\sharp} , h^{\sharp} \rangle
\\=\;&\tau \circ (id \times h^{\sharp}) \circ \langle h^{\sharp} , id \rangle
\\=\;&((\tau + id) \circ dstl \circ (id \times f))^\sharp \circ \langle h^{\sharp} , id \rangle
\\=\;&(((\tau \circ \Delta) + id) \circ f)^\sharp.\tag{\ref{law:uniformity}}
\\=\;&{((\tau + id) \circ dstl \circ (id \times f))}^\sharp \circ \langle h^{\sharp} , id \rangle
\\=\;&{(((\tau \circ \Delta) + id) \circ f)}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
Note that by monicity of \(dstl^{-1}\) and by~\ref{law:fixpoint}
@ -994,11 +1002,11 @@ The following Lemma is central to the proof of commutativity.
Note that \(\mathbf{K}\) is a pre-Elgot monad by definition and strong pre-Elgot by \autoref{lem:Kstrong}. Let us first show that \(\mathbf{K}\) is the initial pre-Elgot monad.
Given any pre-Elgot monad \(\mathbf{T}\), let us introduce alternative names for the monad operations of \(\mathbf{T}\) and \(\mathbf{K}\) to avoid confusion:
\[\mathbf{T} = (T , \eta^T, \mu^T, {(-)}^{\sharp_T})\]
\[\mathbf{T} = (T , \eta^T, \mu^T)\]
and
\[\mathbf{K} = (K , \eta^K, \mu^T, {(-)}^{\sharp_K}).\]
\[\mathbf{K} = (K , \eta^K, \mu^T).\]
For every \(X \in \obj{\C} \) we define \(¡ = \free{(\eta^T : X \rightarrow TX)} : KX \rightarrow TX \). Note that \(¡\) is the unique iteration preserving morphism that satisfies \(¡ \circ \eta^K = \eta^T\). We are done after showing that \(¡\) is natural and respects the monad multiplication.
For every \(X \in \obj{\C} \) we define \(¡ = \free{(\eta^T : X \rightarrow TX)} : KX \rightarrow TX \). Note that \(¡\) is per definition the unique iteration preserving morphism that satisfies \(¡ \circ \eta^K = \eta^T\). We are done after showing that \(¡\) is natural and respects the monad multiplication.
Let \(f : X \rightarrow Y\). For naturality of \(¡\) it suffices to show
\[¡ \circ Kf = \free{Tf \circ \eta^T} = Tf \circ ¡,\]
@ -1008,7 +1016,7 @@ The following Lemma is central to the proof of commutativity.
& ¡ \circ Kf \circ \eta^K
\\=\;&¡ \circ \eta^K \circ f
\\=\;&\eta^T \circ f
\\=\;&Tf \circ \eta^T
\\=\;&Tf \circ \eta^T.
\end{alignat*}
Let us proceed similarly for showing that \(¡\) respects the monad multiplication, i.e.\ consider
@ -1022,7 +1030,7 @@ The following Lemma is central to the proof of commutativity.
\\=\;&¡.
\end{alignat*}
Thus, \(\mathbf{K}\) is an initial pre-Elgot monad. To show that \(\mathbf{K}\) is also initial strong pre-Elgot, assume that \(\mathbf{T}\) is strong with strength \(\tau^T\) and let us call the strength of \(\mathbf{K}\) \(\tau^K\). We are left to show that \(¡\) respects strength, i.e.\ \( ¡ \circ \tau^K = \tau^T \circ (id \times ¡) : X \times KY \rightarrow T(X \times Y) \). Note that
Thus, \(\mathbf{K}\) is an initial pre-Elgot monad. To show that \(\mathbf{K}\) is also initial strong pre-Elgot, assume that \(\mathbf{T}\) is strong with strength \(\tau^T\) and let us call the strength of \(\mathbf{K}\) \(\tau^K\). We are left to show that \(¡\) respects strength, i.e.\ \( ¡ \circ \tau^K = \tau^T \circ (id \times ¡) : X \times KY \rightarrow T(X \times Y) \). We proceed by right-stability, using:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS1kiXSxbMywwLCJLKFggXFx0aW1lcyBZKSJdLFszLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzEsMiwiWCBcXHRpbWVzIFRZIl0sWzAsMywiWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdV5LIl0sWzEsMiwiwqEiXSxbMCwzLCJpZCBcXHRpbWVzIMKhIiwyXSxbMywyLCJcXHRhdV5UIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMiwiXFxldGFeVCIsMix7ImN1cnZlIjoyfV1d
\[
\begin{tikzcd}[ampersand replacement=\&]
@ -1038,5 +1046,5 @@ The following Lemma is central to the proof of commutativity.
\arrow["{\eta^T}"', curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}
\]
commutes, since \( ¡ \circ \tau^K = \eta^T = \tau^T \circ (id \times \eta^T) = \tau^T \circ (id \times ¡) \circ (id \times \eta^T) \). Using \autoref{rem:proofbystability} we are done, since \(¡ \circ \tau^K\) and \(\tau^T \circ (id \times ¡)\) are both right iteration preserving for the reason that both are composed of (right) iteration preserving morphisms.
The diagram commutes, since \( ¡ \circ \tau^K = \eta^T = \tau^T \circ (id \times \eta^T) = \tau^T \circ (id \times ¡) \circ (id \times \eta^T) \). Now we are done, since \(¡ \circ \tau^K\) and \(\tau^T \circ (id \times ¡)\) are both right iteration preserving because both are composed of (right) iteration preserving morphisms.
\end{proof}