|
|
|
|
@ -1,4 +1,4 @@
|
|
|
|
|
\chapter{Iteration Algebras and Monads}\label{chp:iteration}
|
|
|
|
|
\chapter{Iteration Algebras and Monads}
|
|
|
|
|
In this chapter we will draw on the inherent connection between recursion and iteration to establish a partiality monad in a general setting without axioms that comes from previous results in the research on iteration theories.
|
|
|
|
|
\section{Elgot Algebras}
|
|
|
|
|
|
|
|
|
|
@ -38,7 +38,7 @@ A morphism between Elgot algebras $h : (A, (-)^{\#_a}) \rightarrow (B, (-)^{\#_a
|
|
|
|
|
The laws concerning $id$ and composition follow directly since they hold in $\mathcal{C}$.
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
We can form products and exponentials of Elgot algebras in a canonical way, for products this is even stronger:
|
|
|
|
|
\improvement{Add some text}
|
|
|
|
|
|
|
|
|
|
\begin{lemma}
|
|
|
|
|
If $\mathcal{C}$ is a cartesian category, so is $\mathit{Elgot}(\mathcal{C})$.
|
|
|
|
|
@ -54,13 +54,12 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
|
|
|
|
|
The product diagram of $A \times B$ in $\mathcal{C}$ then also holds in $\mathit{Elgot}(\mathcal{C})$, we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism $\langle f , g \rangle$ is iteration preserving for any $f : (Z, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_y})$, which follows since $f$ and $g$ are iteration preserving.
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\begin{lemma}\label{lem:elgotexp}
|
|
|
|
|
Given $X \in \obj{C}$ and $(A, (-)^{\#_a}) \in \vert\mathit{Elgot}(\mathcal{C})\vert$. The exponential $X^A$ (if it exists) can be equipped with an Elgot algebra structure.
|
|
|
|
|
\improvement{Add some text}
|
|
|
|
|
\todo[inline]{add Exponentials}
|
|
|
|
|
|
|
|
|
|
\begin{lemma}
|
|
|
|
|
|
|
|
|
|
\end{lemma}
|
|
|
|
|
\begin{proof}
|
|
|
|
|
Take $f^\# = curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ for any $f : Z \rightarrow A^X + Z$.
|
|
|
|
|
The \textbf{Fixpoint}, \textbf{Uniformity} and \textbf{Folding} laws for $(A^X, (-)^\#)$ follow by the laws of $(A, (-)^{\#_a})$ and some rewriting using properties of distributive categories.
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\section{Pre-Elgot Monads}
|
|
|
|
|
|
|
|
|
|
@ -78,8 +77,6 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
|
|
|
|
|
\change[inline]{be more concrete with types here}
|
|
|
|
|
\end{remark}
|
|
|
|
|
|
|
|
|
|
\todo[inline]{Category of (strong) pre-Elgot monads, introduce category of monads in preliminaries}
|
|
|
|
|
|
|
|
|
|
\section{The Initial Pre-Elgot Monad}
|
|
|
|
|
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial pre-Elgot monad.
|
|
|
|
|
|
|
|
|
|
@ -93,10 +90,10 @@ In this section we will study the monad that arises from existence of all free E
|
|
|
|
|
To show that $\mathbf{K}$ is strong we will need a notion of stability:
|
|
|
|
|
|
|
|
|
|
\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 \mathit{Elgot}(\mathcal{C})$ and $f : X \times Y \rightarrow A$ there exists a unique $f^{\sharp_r} : X \times KY \rightarrow A$ satisfying:
|
|
|
|
|
Let $KY$ be a free Elgot algebra on $Y \in \obj{C}$. We call $KY$ \textit{right-stable} if for every $A \in \mathit{Elgot}(\mathcal{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}
|
|
|
|
|
&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}.
|
|
|
|
|
\end{definition}
|
|
|
|
|
@ -104,10 +101,10 @@ To show that $\mathbf{K}$ is strong we will need a notion of stability:
|
|
|
|
|
We get the following dual definition:
|
|
|
|
|
|
|
|
|
|
\begin{definition}[Left-Stable Free Elgot Algebra]\label{def:leftstablefreeelgot}
|
|
|
|
|
Let $KY$ be a free Elgot algebra on $Y \in \obj{C}$. We call $KY$ \textit{left-stable} if for every $A \in \mathit{Elgot}(\mathcal{C})$ and $f : Y \times X \rightarrow A$ there exists a unique $f^{\sharp_l} : KY \times X \rightarrow A$ satisfying:
|
|
|
|
|
Let $KY$ be a free Elgot algebra on $Y \in \obj{C}$. We call $KY$ \textit{left-stable} if for every $A \in \mathit{Elgot}(\mathcal{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}
|
|
|
|
|
&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}.
|
|
|
|
|
\end{definition}
|
|
|
|
|
@ -125,178 +122,19 @@ We get the following dual definition:
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
We will usually refer to right-stable free Elgot algebras as just stable Elgot algebras and omit the index of the operator.
|
|
|
|
|
We will usually refer to right-stable free Elgot algebras as just stable Elgot algebras.
|
|
|
|
|
|
|
|
|
|
Stability of $KX$ expresses that it somehow behaves like it would in a cartesian closed category, the following theorem should then follow trivially:
|
|
|
|
|
\todo[inline]{proof that KX stable in CCC}
|
|
|
|
|
|
|
|
|
|
\begin{theorem}
|
|
|
|
|
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$.
|
|
|
|
|
|
|
|
|
|
We will show that $KX$ is left-stable, i.e. given $X \in \obj{C}, A \in \vert\mathit{Elgot}(\mathcal{C})\vert$ and $f : Y \times X \rightarrow A$ we define
|
|
|
|
|
$f^{\sharp_l} := eval \circ (\llbracket curry\;f \rrbracket \times id)$.
|
|
|
|
|
Note that we are using the universal property of a free object over $\textit{Elgot}(\mathcal{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 preversing which follows from \ref{sharpl2}.
|
|
|
|
|
TODO
|
|
|
|
|
\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.
|
|
|
|
|
\todo[inline]{proof that K is strong and commutative}
|
|
|
|
|
|
|
|
|
|
Before proving strength, we will introduce a proof principle similar to remark~\ref{rem:coinduction}.
|
|
|
|
|
\todo[inline]{proof that K is equational lifting}
|
|
|
|
|
|
|
|
|
|
\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 \elgotobj{C}$ to show that $g = h$ it suffices to find a morphism $f : X \times Y \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpr1} and \ref{sharpr2}.
|
|
|
|
|
\end{remark}
|
|
|
|
|
|
|
|
|
|
Of course there is also a symmetric version of this:
|
|
|
|
|
|
|
|
|
|
\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 \elgotobj{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}.
|
|
|
|
|
\end{remark}
|
|
|
|
|
|
|
|
|
|
\begin{theorem}
|
|
|
|
|
$\mathbf{K}$ is a strong monad.
|
|
|
|
|
\end{theorem}
|
|
|
|
|
\begin{proof}
|
|
|
|
|
We define strength as $\tau : (\eta : X \times Y \rightarrow K(X \times Y))^\sharp : X \times KY \rightarrow K(X \times Y)$
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
% For naturality of $\tau$, i.e. $\tau \circ (f \times Kg) = K(f \times g) \circ \tau$ for $f : A \rightarrow X, g : B \rightarrow Y$ we use:
|
|
|
|
|
For naturality of $\tau$ we use:
|
|
|
|
|
|
|
|
|
|
% % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIFxcdGltZXMgS0IiXSxbMiwwLCJLKFggXFx0aW1lcyBZKSJdLFswLDIsIkEgXFx0aW1lcyBCIl0sWzAsMSwiXFx0YXUgXFxjaXJjIChmIFxcdGltZXMgS2cpIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsIksoZlxcdGltZXMgZykgXFxjaXJjIFxcdGF1IiwyLHsib2Zmc2V0IjoxfV0sWzIsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzIsMSwiXFxldGEgXFxjaXJjIEsoZiBcXHRpbWVzIGcpIiwyXV0=
|
|
|
|
|
% \[\begin{tikzcd}
|
|
|
|
|
% {A \times KB} && {K(X \times Y)} \\
|
|
|
|
|
% \\
|
|
|
|
|
% {A \times B}
|
|
|
|
|
% \arrow["{\tau \circ (f \times Kg)}", shift left, from=1-1, to=1-3]
|
|
|
|
|
% \arrow["{K(f\times g) \circ \tau}"', shift right, from=1-1, to=1-3]
|
|
|
|
|
% \arrow["{id \times \eta}"', from=3-1, to=1-1]
|
|
|
|
|
% \arrow["{\eta \circ K(f \times g)}"', from=3-1, to=1-3]
|
|
|
|
|
% \end{tikzcd}\]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
& {A \times KB} && {X \times KY} \\
|
|
|
|
|
\\
|
|
|
|
|
& {K(A \times B)} && {K(X \times Y)} \\
|
|
|
|
|
{A \times B}
|
|
|
|
|
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
|
|
|
|
|
\arrow["\tau"', from=1-2, to=3-2]
|
|
|
|
|
\arrow["{K(f\times g)}"', from=3-2, to=3-4]
|
|
|
|
|
\arrow["{f \times Kg}", from=1-2, to=1-4]
|
|
|
|
|
\arrow["\tau", from=1-4, to=3-4]
|
|
|
|
|
\arrow["{\eta \circ (f \times g)}"', curve={height=12pt}, from=4-1, to=3-4]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
The strength laws are proven similarly:
|
|
|
|
|
|
|
|
|
|
\begin{itemize}
|
|
|
|
|
\item[\ref{S1}]
|
|
|
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
{X \times KY} && {K(X\times Y)} \\
|
|
|
|
|
\\
|
|
|
|
|
{X \times Y} && KY
|
|
|
|
|
\arrow["\tau", from=1-1, to=1-3]
|
|
|
|
|
\arrow["{K\pi_2}", from=1-3, to=3-3]
|
|
|
|
|
\arrow["{\pi_2}"', from=1-1, to=3-3]
|
|
|
|
|
\arrow["{id \times \eta}"', from=3-1, to=1-1]
|
|
|
|
|
\arrow["{\eta \circ \pi_2}"', from=3-1, to=3-3]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
\todo{this is more general than S1}
|
|
|
|
|
|
|
|
|
|
\item[\ref{S2}]
|
|
|
|
|
This is an instance of \ref{sharpr1}.
|
|
|
|
|
\item[\ref{S3}]
|
|
|
|
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS0tZIl0sWzMsMCwiWCBcXHRpbWVzIEtZIl0sWzMsMiwiSyhYXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFswLDMsIlggXFx0aW1lcyBLWSJdLFswLDEsImlkIFxcdGltZXMgXFxtdSIsMl0sWzEsMiwiXFx0YXUiLDJdLFswLDMsIlxcdGF1Il0sWzMsMiwiXFx0YXVeKiJdLFs0LDAsImlkIFxcdGltZXMgXFxldGEiLDAseyJjdXJ2ZSI6LTJ9XSxbNCwyLCJcXHRhdSIsMCx7ImN1cnZlIjoyfV1d
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
& {X \times KKY} && {X \times KY} \\
|
|
|
|
|
\\
|
|
|
|
|
& {K(X \times KY)} && {K(X\times Y)} \\
|
|
|
|
|
{X \times KY}
|
|
|
|
|
\arrow["{id \times \mu}"', from=1-2, to=1-4]
|
|
|
|
|
\arrow["\tau"', from=1-4, to=3-4]
|
|
|
|
|
\arrow["\tau", from=1-2, to=3-2]
|
|
|
|
|
\arrow["{\tau^*}", from=3-2, to=3-4]
|
|
|
|
|
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
|
|
|
|
|
\arrow["\tau", curve={height=12pt}, from=4-1, to=3-4]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
\item[\ref{S4}]
|
|
|
|
|
% https://q.uiver.app/#q=WzAsNixbMSwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgS1oiXSxbMSwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIEtZIl0sWzMsMCwiSygoWCBcXHRpbWVzIFkpIFxcdGltZXMgWikiXSxbMywyLCJLKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgSyhZIFxcdGltZXMgWikiXSxbMCwzLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgWiJdLFswLDEsIlxcYWxwaGEiXSxbMiwzLCJLXFxhbHBoYSJdLFswLDIsIlxcdGF1Il0sWzEsNCwiaWQgXFx0aW1lc1xcdGF1Il0sWzQsMywiXFx0YXUiXSxbNSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzUsMywiXFxldGEgXFxjaXJjIFxcYWxwaGEiLDIseyJjdXJ2ZSI6Mn1dXQ==
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
& {(X \times Y) \times KZ} && {K((X \times Y) \times Z)} \\
|
|
|
|
|
\\
|
|
|
|
|
& {X \times Y \times KY} & {X \times K(Y \times Z)} & {K(X \times Y \times Z)} \\
|
|
|
|
|
{(X \times Y) \times Z}
|
|
|
|
|
\arrow["\alpha", from=1-2, to=3-2]
|
|
|
|
|
\arrow["K\alpha", from=1-4, to=3-4]
|
|
|
|
|
\arrow["\tau", from=1-2, to=1-4]
|
|
|
|
|
\arrow["{id \times\tau}", from=3-2, to=3-3]
|
|
|
|
|
\arrow["\tau", from=3-3, to=3-4]
|
|
|
|
|
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
|
|
|
|
|
\arrow["{\eta \circ \alpha}"', curve={height=12pt}, from=4-1, to=3-4]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\change[inline]{Use sigma instead of hat(tau)}
|
|
|
|
|
|
|
|
|
|
\begin{theorem}
|
|
|
|
|
$\mathbf{K}$ is a commutative monad.
|
|
|
|
|
\end{theorem}
|
|
|
|
|
\begin{proof}
|
|
|
|
|
We use remark~\ref{rem:proofbystability} again:
|
|
|
|
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJLWCBcXHRpbWVzIEtZIl0sWzMsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzEsMiwiSyhYIFxcdGltZXMgS1kpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMCwzLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdSJdLFswLDIsIlxcaGF0e1xcdGF1fSIsMl0sWzEsMywiXFxoYXR7XFx0YXV9XioiXSxbMiwzLCJcXHRhdV4qIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMywiXFxoYXR7XFx0YXV9IiwyLHsiY3VydmUiOjJ9XV0=
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
& {KX \times KY} && {K(KX \times Y)} \\
|
|
|
|
|
\\
|
|
|
|
|
& {K(X \times KY)} && {K(X \times Y)} \\
|
|
|
|
|
{KX \times Y}
|
|
|
|
|
\arrow["\tau", from=1-2, to=1-4]
|
|
|
|
|
\arrow["{\hat{\tau}}"', from=1-2, to=3-2]
|
|
|
|
|
\arrow["{\hat{\tau}^*}", from=1-4, to=3-4]
|
|
|
|
|
\arrow["{\tau^*}"', from=3-2, to=3-4]
|
|
|
|
|
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
|
|
|
|
|
\arrow["{\hat{\tau}}"', curve={height=12pt}, from=4-1, to=3-4]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
The proofs for \ref{sharpr1} and the proof that $\hat{\tau}^* \circ \tau$ is right iteration preserving are straightforward and can be looked up in the formalization.
|
|
|
|
|
The proof that $\tau^* \circ \hat{\tau}$ is right iteration preserving is non-trivial, so we will look at it in more detail:
|
|
|
|
|
Let $Z \in \obj{C}, h : Z \rightarrow KY + Z$ and let us introduce a definition for brevity: $\psi = \tau^* \circ \hat{\tau}$. We now use remark~\ref{rem:proofbyleftstability} to show that $\psi$ is right iteration preserving:
|
|
|
|
|
|
|
|
|
|
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
&&&& {KX \times KY} \\
|
|
|
|
|
{KX \times Z} &&&& {K(X \times Y)} \\
|
|
|
|
|
\\
|
|
|
|
|
{X \times Z}
|
|
|
|
|
\arrow["\psi", from=1-5, to=2-5]
|
|
|
|
|
\arrow["{id \times h^\#}", from=2-1, to=1-5]
|
|
|
|
|
\arrow["{((\psi + id) \circ dstl \circ (id \times h))^\#}"', from=2-1, to=2-5]
|
|
|
|
|
\arrow["{\eta \times id}", from=4-1, to=2-1]
|
|
|
|
|
\arrow["{\tau \circ (id \times h^\#)}"', from=4-1, to=2-5]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
\change[inline]{Be more specific}
|
|
|
|
|
\todo[inline]{introduce Diamond and Stutter laws}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\begin{theorem}
|
|
|
|
|
$\mathbf{K}$ is an equational lifting monad.
|
|
|
|
|
\end{theorem}
|
|
|
|
|
|
|
|
|
|
\begin{proof}
|
|
|
|
|
\todo[inline]{proof that K is equational lifting}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\begin{theorem}
|
|
|
|
|
$\mathbf{K}$ is the initial (strong) pre-Elgot monad.
|
|
|
|
|
\end{theorem}
|
|
|
|
|
\begin{proof}
|
|
|
|
|
$\mathbf{K}$ is by definition a pre-Elgot monad, we are left to show that it is the initial one.
|
|
|
|
|
\todo[inline]{proof that K is initial strong pre-Elgot}
|
|
|
|
|
\end{proof}
|
|
|
|
|
\todo[inline]{proof that K is initial strong pre-Elgot}
|