|
|
|
|
@ -4,41 +4,136 @@ In this chapter we will draw on the inherent connection between partiality and i
|
|
|
|
|
\section{Elgot Algebras}
|
|
|
|
|
|
|
|
|
|
\improvement{Add some text}
|
|
|
|
|
\unsure[inline]{Check types etc.}
|
|
|
|
|
\begin{definition}[Unguarded Elgot Algebra]
|
|
|
|
|
\todo[inline]{Definition unguarded Elgot algebra}
|
|
|
|
|
\begin{definition}[Guarded Elgot Algebra]
|
|
|
|
|
\todo[inline]{Definition guarded Elgot algebra}
|
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
|
|
\begin{definition}[Elgot Algebra]
|
|
|
|
|
A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
|
|
|
|
|
\begin{itemize}
|
|
|
|
|
\item An object A
|
|
|
|
|
\item for every \(f : X \rightarrow A + X\) the iteration \(f^\# : X \rightarrow A\), satisfying:
|
|
|
|
|
\item for every \(f : X \rightarrow A + X\) the iteration \(f^\sharp : X \rightarrow A\), satisfying:
|
|
|
|
|
\begin{itemize}
|
|
|
|
|
\item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: \(f^\# = [ id , f ^\# ] \circ f\)
|
|
|
|
|
\item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: \(f^\sharp = [ id , f ^\sharp ] \circ f\)
|
|
|
|
|
\\ for \(f : X \rightarrow A + X\)
|
|
|
|
|
\item \customlabel{law:uniformity}{\textbf{Uniformity}}: \((id + h) \circ f = g \circ h \Rightarrow f ^\# = g^\# \circ h\)
|
|
|
|
|
\item \customlabel{law:uniformity}{\textbf{Uniformity}}: \((id + h) \circ f = g \circ h \Rightarrow f ^\sharp = g^\sharp \circ h\)
|
|
|
|
|
\\ for \(f : X \rightarrow A + X,\; g : Y \rightarrow A + Y,\; h : X \rightarrow Y\)
|
|
|
|
|
\item \customlabel{law:folding}{\textbf{Folding}}: \(((f^\# + id) \circ h)^\# = [ (id + inl) \circ f , inr \circ h ]^\# \)
|
|
|
|
|
\item \customlabel{law:folding}{\textbf{Folding}}: \({((f^\sharp + id) \circ h)}^\sharp = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp \)
|
|
|
|
|
\\ for \(f : X \rightarrow A + X,\; h : Y \rightarrow X + Y\)
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
|
|
\begin{lemma}
|
|
|
|
|
Every Elgot algebra \((A , (-)^\#)\) satisfies the following additional laws
|
|
|
|
|
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional laws
|
|
|
|
|
|
|
|
|
|
\begin{itemize}
|
|
|
|
|
\item \customlabel{law:stutter}{\textbf{Stutter}}: \({(([ h , h ] + id) \circ f)}^\# = {(i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] )}^\# \circ inr\)
|
|
|
|
|
\\ for \(f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A\)
|
|
|
|
|
\item \customlabel{law:diamond}{\textbf{Diamond}}: \({((id + \Delta) \circ f)}^\# = {([ i_1 , ((id + \Delta) \circ f)^\# + id] \circ f)}^\# \)
|
|
|
|
|
\\ for \(f : X \rightarrow A + (X + X)\)
|
|
|
|
|
\item \customlabel{law:compositionality}{\textbf{Compositionality}}: \({((f^\# + id) \circ h)}^\# = {([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\# \circ i_2\)
|
|
|
|
|
\item \customlabel{law:compositionality}{\textbf{Compositionality}}: \({((f^\sharp + id) \circ h)}^\sharp = {([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2\)
|
|
|
|
|
\\ for \(f : X \rightarrow A + X, h : Y \rightarrow X + Y\)
|
|
|
|
|
\item \customlabel{law:stutter}{\textbf{Stutter}}: \({(([ h , h ] + id) \circ f)}^\sharp = {(i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] )}^\sharp \circ inr\)
|
|
|
|
|
\\ for \(f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A\)
|
|
|
|
|
\item \customlabel{law:diamond}{\textbf{Diamond}}: \({((id + \Delta) \circ f)}^\sharp = {([ i_1 , ((id + \Delta) \circ f)^\sharp + id] \circ f)}^\sharp \)
|
|
|
|
|
\\ for \(f : X \rightarrow A + (X + X)\)
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{lemma}
|
|
|
|
|
\begin{proof}
|
|
|
|
|
\todo[inline]{Prove diamond and stutter laws}
|
|
|
|
|
\begin{proof}\;\\
|
|
|
|
|
\begin{itemize}
|
|
|
|
|
\item \ref{law:compositionality}: First, note that \ref{law:folding} can equivalently be reformulated as % chktex 2
|
|
|
|
|
\begin{equation*}
|
|
|
|
|
{((f^\sharp + id) \circ h)}^\sharp = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp \circ i_2, \tag{\textbf{Folding'}}\label{law:folding'}
|
|
|
|
|
\end{equation*}
|
|
|
|
|
since
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& {((f^\sharp + id) \circ h)}^\sharp
|
|
|
|
|
\\=\;&{(f^\sharp + h)}^\sharp \circ h\tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&[f^\sharp , {(f^\sharp + h)}^\sharp \circ h ] \circ i_2
|
|
|
|
|
\\=\;&[ id , {(f^\sharp + h)}^\sharp ] \circ (f^\sharp + h) \circ i_2
|
|
|
|
|
\\=\;&{(f^\sharp + h)}^\sharp \circ i_2 \tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2. \tag{\ref{law:folding}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
Using \ref{law:folding'}, we are left to show that % chktex 2
|
|
|
|
|
\[{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2 = {([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2.\]
|
|
|
|
|
Indeed,
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& {[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2
|
|
|
|
|
\\=\;&[ id , {[ (id + i_1) \circ f , i_2 \circ h]}^\sharp ] \circ [ (id + i_1) \circ f , i_2 \circ h] \circ i_2 \tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&[ id , {[ (id + i_1) \circ f , i_2 \circ h]}^\sharp ] i_2 \circ h
|
|
|
|
|
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ h
|
|
|
|
|
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp [ i_1 , h ] \circ i_2
|
|
|
|
|
\\=\;&{([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2.\tag{\ref{law:uniformity}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
\item \ref{law:stutter}: Note that % chktex 2
|
|
|
|
|
\begin{equation}
|
|
|
|
|
[ h , h ] = {(h + i_1)}^\sharp, \tag{*}\label{stutter-helper}
|
|
|
|
|
\end{equation}
|
|
|
|
|
since
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& {(h + i_1)}^\sharp
|
|
|
|
|
\\=\;&[ id , {(h + i_1)}^\sharp ] \circ (h + i_1) \tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&[ h , {(h + i_1)}^\sharp \circ i_1 ]
|
|
|
|
|
\\=\;&[ h , [ id , {(h + i_1)}^\sharp ] \circ (h + i_1) \circ i_1 ] \tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&[ h , h ].
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
Now we are done by
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& {([ h , h ] + id) \circ f}^\sharp
|
|
|
|
|
\\=\;&{({(h + i_1)}^\sharp + id) \circ f}^\sharp\tag{\ref{stutter-helper}}
|
|
|
|
|
\\=\;&{([(id + i_1) \circ (h + i_1) , i_2 \circ i_2] \circ [ i_1 , f])}^\sharp \circ i_2\tag{\ref{law:compositionality}}
|
|
|
|
|
\\=\;&{([h + i_1 \circ i_1 , i _2 \circ i_2] \circ [ i_1 , f])}^\sharp \circ (i_1 + id) \circ i_2
|
|
|
|
|
\\=\;&{[ i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] \circ f ]}^\sharp \circ i_2. \tag{\ref{law:uniformity}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\item \ref{law:diamond}: Let \(h = [ i_1 \circ i_1 , i_2 + id ] \circ f\) and \(g = (id + \Delta) \circ f\). %chktex 2
|
|
|
|
|
First, note that
|
|
|
|
|
\begin{equation*}
|
|
|
|
|
[ id , g^\sharp ] = {[ i_1 , (id + i_2) \circ g ]}^\sharp, \tag{\(\Asterisk\)}\label{diamond-helper}
|
|
|
|
|
\end{equation*}
|
|
|
|
|
by \ref{law:fixpoint} and \ref{law:uniformity}: % chktex 2
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& [ id , g^\sharp ]
|
|
|
|
|
\\=\;&[ id , [ id , g^\sharp ] \circ g ] \tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&[ id , [ id , {[ i_1 , (id + i_2) \circ g ]}^\sharp \circ i_2 ] \circ g ] \tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&[ id , {[ i_1 , (id + i_2) \circ g ]}^\sharp ] \circ [ i_1 , (id + i_2) \circ g ]
|
|
|
|
|
\\=\;&{[ i_1 , (id + i_2) \circ g ]}^\sharp. \tag{\ref{law:fixpoint}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
Furthermore, by \ref{law:folding}: % chktex 2
|
|
|
|
|
\[{[ (id + i_1) \circ [ i_1 , (id + i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2 = {({[i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2.\]
|
|
|
|
|
|
|
|
|
|
It thus suffices to show that,
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& g^\sharp
|
|
|
|
|
\\=\;&{[ (id + i_1) \circ [ i_1 , (id + i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2
|
|
|
|
|
\\=\;&{({[i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2
|
|
|
|
|
\\=\;&{([ i_1 , g^\sharp + id] \circ f)}^\sharp.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
Indeed,
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& g^\sharp
|
|
|
|
|
\\=\;&g^\sharp \circ [ id , id ] \circ i_2
|
|
|
|
|
\\=\;&{[ (id + i_2) \circ g , f ]}^\sharp \circ i_2\tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&{(([ id , id ] + id) \circ [ (i_1 + i_1) \circ g , (i_2 + id) \circ f ]) }^\sharp \circ i_2
|
|
|
|
|
\\=\;&{[ i_1 , [ id + i_1 , i_2 \circ i_2 ] \circ [ (i_1 + i_1) \circ g , (i_2 + id) \circ f] ]}^\sharp \circ i_2 \circ i_2 \tag{\ref{law:stutter}}
|
|
|
|
|
\\=\;&{[ i_1 , [ [ i_1 , i_2 \circ i_2 \circ i_1 ] \circ g , [ i_2 \circ i_1 , i_2 \circ i_2 ] \circ f] ]}^\sharp \circ i_2 \circ i_2
|
|
|
|
|
\\=\;&{[ i_1 , [ ( id + i_2 \circ i_1) \circ g , i_2 \circ \circ f] ]}^\sharp \circ i_2 \circ i_2
|
|
|
|
|
\\=\;&{ [[ i_1 , (id + i_1 \circ i_2) \circ g ] , i_2 \circ h] }^\sharp \circ [ i_1 \circ i_1 , i_2 + id ] \circ i_2 \circ i_2\tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&{ [[ i_1 , (id + i_1 \circ i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2
|
|
|
|
|
\\=\;&{ [(id + i_1) \circ [ i_1 , (id + i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
and
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& {([ i_1 , g^\sharp + id] \circ f)}^\sharp
|
|
|
|
|
\\=\;&{([i_1 \circ [id , g^\sharp] \circ i_1 , [ id , g^\sharp ] \circ i_2 + id ] \circ f)}^\sharp
|
|
|
|
|
\\=\;&{(([ id , g^\sharp ] + id) \circ h)}^\sharp
|
|
|
|
|
\\=\;&{(([[id , g^\sharp] , [id , g^\sharp] ] + id) \circ (i_2 + id) \circ h)}^\sharp
|
|
|
|
|
\\=\;&{[i_1 \circ [ id , g^\sharp ] , [ [id , g^\sharp] + i_1 , i_2 \circ i_2 ] \circ (i_2 + id) \circ h]}^\sharp \circ i_2 \tag{\ref{law:stutter}}
|
|
|
|
|
\\=\;&{([ id , g^\sharp ] + h)}^\sharp \circ i_2
|
|
|
|
|
\\=\;&{({[ i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2,\tag{\ref{diamond-helper}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
which concludes the proof.
|
|
|
|
|
\qedhere
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\todo[inline]{Mention here that previous lemma implies that unguarded Elgot are id guarded Elgot and diamond gives alternate way of classifying Elgot algebras citing Sergey}
|
|
|
|
|
@ -46,19 +141,19 @@ In this chapter we will draw on the inherent connection between partiality and i
|
|
|
|
|
Morphisms between Elgot algebras that are coherent with respect to the iteration operator are of special interest to us, the following definition classifies them.
|
|
|
|
|
|
|
|
|
|
\begin{definition}[Iteration Preserving Morphisms]
|
|
|
|
|
Let \((A, {(-)}^{\#_a}), (B, {(-)}^{\#_b})\) be two Elgot algebras.
|
|
|
|
|
Let \((A, {(-)}^{\sharp_a}), (B, {(-)}^{\sharp_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}\]
|
|
|
|
|
\[f \circ (id \times h^{\sharp_a}) = ((f + id) \circ dstl \circ (id \times h))^{\sharp_b}\]
|
|
|
|
|
for any \(h : Y \rightarrow A + Y\).
|
|
|
|
|
|
|
|
|
|
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}\]
|
|
|
|
|
\[f \circ (h^{\sharp_a} \times id) = ((f + id) \circ dstr \circ (h \times id))^{\sharp_b}\]
|
|
|
|
|
for any \(h : Y \rightarrow A + Y\).
|
|
|
|
|
|
|
|
|
|
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}\]
|
|
|
|
|
\[f \circ h^{\sharp_a} = {((f + id) \circ h)}^{\sharp_b}\]
|
|
|
|
|
for any \(h : Y \rightarrow A + Y\).
|
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
|
|
@ -70,16 +165,16 @@ The previous definition yields the category of Elgot algebras over a category \(
|
|
|
|
|
\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.
|
|
|
|
|
Let \((A , {(-)}^{\sharp_a}), (B , {(-)}^{\sharp_b}), (C , {(-)}^{\sharp_c})\) be Elgot algebras.
|
|
|
|
|
The identity trivially satisfies
|
|
|
|
|
\[id \circ f^{\#_a} = f^{\#_a} = {((id + id) \circ f)}^{\#_a}\]
|
|
|
|
|
\[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
|
|
|
|
|
\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}
|
|
|
|
|
& 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}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
for any \(h : X \rightarrow A + X\).
|
|
|
|
|
\end{proof}
|
|
|
|
|
@ -87,25 +182,25 @@ The previous definition yields the category of Elgot algebras over a category \(
|
|
|
|
|
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}\).
|
|
|
|
|
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^\# =\;! : X \rightarrow 1\) as the unique morphism into the terminal object. The Elgot algebra laws follow instantly by uniqueness of \(!\). \((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.
|
|
|
|
|
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, {(-)}^{\#_a}) , (B, {(-)}^{\#_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^\# = \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:
|
|
|
|
|
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:
|
|
|
|
|
\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)^{\#_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)^{\sharp_a}\) and \({((\pi_2 + id) \circ f)}^{\sharp_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
|
|
|
|
|
\\ &, [ id , ((\pi_2 + id) \circ f)^{\#_b} ] \circ (\pi_2 + id) \circ f \rangle \tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\#_a} ] \circ f , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\#_b} ] \circ f \rangle
|
|
|
|
|
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\#_a} ] , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\#_b} ] \rangle \circ f
|
|
|
|
|
\\=\;&[ \langle \pi_1 , \pi_2 \rangle , \langle {((\pi_1 + id) \circ f)}^{\#_a} , {((\pi_2 + id) \circ f)}^{\#_b} \rangle ] \circ f
|
|
|
|
|
\\=\;&[ id , \langle {((\pi_1 + id) \circ f)}^{\#_a} , {((\pi_2 + id) \circ f)}^{\#_b} \rangle ] \circ f
|
|
|
|
|
& \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}}
|
|
|
|
|
\\=\;&\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
|
|
|
|
|
\\=\;&[ id , \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle ] \circ f
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\item \textbf{Uniformity}: Let \(f : X \rightarrow (A \times B) + X, g : Y \rightarrow (A \times B) + Y, h : X \rightarrow Y\) and \((id + h) \circ f = g \circ h\).
|
|
|
|
|
Note that this implies:
|
|
|
|
|
@ -114,93 +209,93 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
|
|
|
|
|
\\&(id + h) \circ (\pi_2 + id) \circ f &&= (\pi_2 + id) \circ g \circ h
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
Then,~\ref{law:uniformity} of \({(-)}^{\#_a}\) and \({(-)}^{\#_b}\) with the previous two equations yields:
|
|
|
|
|
Then,~\ref{law:uniformity} of \({(-)}^{\sharp_a}\) and \({(-)}^{\sharp_b}\) with the previous two equations yields:
|
|
|
|
|
\begin{alignat*}{2}
|
|
|
|
|
& \langle {((\pi_1 + id) \circ f)}^{\#_a} , {((\pi_1 + id) \circ f)}^{\#_a} \rangle & & = {((\pi_1 + id) \circ g})^{\#_a} \circ h
|
|
|
|
|
\\&\langle {((\pi_2 + id) \circ f)}^{\#_b} , {((\pi_2 + id) \circ f)}^{\#_b} \rangle &&= {((\pi_2 + id) \circ g)}^{\#_b} \circ h
|
|
|
|
|
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_1 + id) \circ f)}^{\sharp_a} \rangle & & = {((\pi_1 + id) \circ g})^{\sharp_a} \circ h
|
|
|
|
|
\\&\langle {((\pi_2 + id) \circ f)}^{\sharp_b} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle &&= {((\pi_2 + id) \circ g)}^{\sharp_b} \circ h
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
This concludes the proof of:
|
|
|
|
|
\[ \langle {((\pi_1 + id) \circ f)}^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle = \langle {((\pi_1 + id) \circ g)}^{\#_a} , {((\pi_2 + id) \circ g)}^{\#_b} \rangle \circ h \]
|
|
|
|
|
\[ \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , ((\pi_2 + id) \circ f)^{\sharp_b} \rangle = \langle {((\pi_1 + id) \circ g)}^{\sharp_a} , {((\pi_2 + id) \circ g)}^{\sharp_b} \rangle \circ h \]
|
|
|
|
|
\item \textbf{Folding}: Let \(f : X \rightarrow (A \times B) + X, h : Y \rightarrow X + Y\). We need to show:
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \langle {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\#_a} , {((\pi_2 + id) \circ f)}^{\#_b} \rangle + h))}^{\#_a}
|
|
|
|
|
\\&,{((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\#_a} , {((\pi_2 + id) \circ f)}^{\#_b} \rangle + h))}^{\#_b} \rangle
|
|
|
|
|
\\=\;&\langle (\pi_1 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\#_a} , (\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\#_b} \rangle
|
|
|
|
|
& \langle {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_a}
|
|
|
|
|
\\&,{((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_b} \rangle
|
|
|
|
|
\\=\;&\langle (\pi_1 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_a} , (\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_b} \rangle
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
Indeed, the folding laws for \({(-)}^{\#_a}\) and \({(-)}^{\#_b}\) imply
|
|
|
|
|
Indeed, the folding laws for \({(-)}^{\sharp_a}\) and \({(-)}^{\sharp_b}\) imply
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\#_a} , {((\pi_2 + id) \circ f)}^{\#_b} \rangle + h))}^{\#_a}
|
|
|
|
|
\\=\;&{({((\pi_1 + id) \circ f)}^{\#_a} + h)}^{\#_a}
|
|
|
|
|
\\=\;&{[ (id + i_1) \circ (\pi_1 + id) \circ f , i_2 \circ h ]}^{\#_a}\tag{\ref{law:folding}}
|
|
|
|
|
\\=\;&(\pi_1 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\#_a}
|
|
|
|
|
& {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_a}
|
|
|
|
|
\\=\;&{({((\pi_1 + id) \circ f)}^{\sharp_a} + h)}^{\sharp_a}
|
|
|
|
|
\\=\;&{[ (id + i_1) \circ (\pi_1 + id) \circ f , i_2 \circ h ]}^{\sharp_a}\tag{\ref{law:folding}}
|
|
|
|
|
\\=\;&(\pi_1 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_a}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
and
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& {((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\#_a} , {((\pi_2 + id) \circ f)}^{\#_b} \rangle + h))}^{\#_b}
|
|
|
|
|
\\=\;&{(((\pi_2 + id) \circ f)^{\#_b} + h)}^{\#_b}
|
|
|
|
|
\\=\;&{[ (id + i_1) \circ (\pi_2 + id) \circ f , i_2 \circ h ]}^{\#_b}\tag{\ref{law:folding}}
|
|
|
|
|
\\=\;&(\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\#_b}
|
|
|
|
|
& {((\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}
|
|
|
|
|
\\=\;&{[ (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, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_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 : (Z, {(-)}^{\sharp_z}) \rightarrow (X, {(-)}^{\sharp_x}), g : (Z, {(-)}^{\sharp_z}) \rightarrow (Y, {(-)}^{\sharp_y})\):
|
|
|
|
|
|
|
|
|
|
Let \(h : X \rightarrow E + X\) where \(E \in \obj{\elgotalgs{\C}}\). We use the fact that \(f, g\) are iteration preserving to show:
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \langle f , g \rangle \circ (h^{\#_e})
|
|
|
|
|
\\=\;&\langle f \circ (h^{\#_e}) , g \circ (h^{\#_e}) \rangle
|
|
|
|
|
\\=\;&\langle ((f + id) \circ h)^{\#_a} , ((g + id) \circ h)^{\#_b} \rangle
|
|
|
|
|
\\=\;&\langle ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\#_a} , ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\#_b} \rangle
|
|
|
|
|
& \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
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, we have shown that \(\elgotalgs{\C}\) is cartesian if \(\C \) is cartesian.
|
|
|
|
|
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.
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
\begin{lemma}\label{lem:elgotexp}
|
|
|
|
|
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.
|
|
|
|
|
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.
|
|
|
|
|
\end{lemma}
|
|
|
|
|
\begin{proof}
|
|
|
|
|
Take \(f^\# = curry (((eval + id) \circ dstr \circ (f \times id))^{\#_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^\# = curry\;(((eval + id) \circ dstr \circ (f \times id))^{\#_a})\) it suffices to show:
|
|
|
|
|
\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:
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& eval \circ ([ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a}) ] \circ f] \times id)
|
|
|
|
|
\\=\;&eval \circ [ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\#_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))^{\#_a}) \times id ] \circ dstr \circ (f \times id)
|
|
|
|
|
\\=\;&[ eval , ((eval + id) \circ dstr \circ (f \times id))^{\#_a} ] \circ dstr \circ (f \times id)
|
|
|
|
|
\\=\;&[ id , ((eval + id) \circ dstr \circ (f \times id))^{\#_a} ] \circ (eval + id) \circ dstr \circ (f \times id)
|
|
|
|
|
\\=\;&((eval + id) \circ dstr \circ (f \times id))^{\#_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
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) ] \times id
|
|
|
|
|
\\= \;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_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\):
|
|
|
|
|
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \pi_1 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr
|
|
|
|
|
\\=\;&[ \pi_1 , \pi_1 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr
|
|
|
|
|
\\=\;&[ \pi_1 , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \circ \pi_1 ] \circ dstr
|
|
|
|
|
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) ] \circ (\pi_1 + \pi_1) \circ dstr
|
|
|
|
|
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_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*}
|
|
|
|
|
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \pi_2 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr
|
|
|
|
|
\\=\;&[ \pi_2 , \pi_2 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\#_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
|
|
|
|
|
\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^\# = curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a})\) it suffices to show:
|
|
|
|
|
\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:
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& ((eval + id) \circ dstr \circ (f \times id))^{\#_a}
|
|
|
|
|
\\=\;&((eval + id) \circ dstr \circ (g \times id))^{\#_a} \circ (h \times id)\tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\#_a} \times id) \circ (h \times id)
|
|
|
|
|
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\#_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:
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
@ -211,15 +306,15 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\item \textbf{Folding}: Let \(Y, Z \in \obj{C}, f : Y \rightarrow X^A + Y, h : Y \rightarrow Z\).
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& (f^\# + h)^\#
|
|
|
|
|
\\=\;&curry(((eval + id) \circ dstr \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) + h) \times id))^{\#_a})
|
|
|
|
|
\\=\;&curry(((eval + id) \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id) + (h \times id)) \circ dstr)^{\#_a})
|
|
|
|
|
\\=\;&curry(((eval \circ (curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id) + (h \times id)) \circ dstr)^{\#_a})
|
|
|
|
|
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (h \times id)) \circ dstr)^{\#_a})
|
|
|
|
|
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\#_a} + dstr \circ (h \times id)))^{\#_a} \circ dstr)\tag{\ref{law:uniformity}}
|
|
|
|
|
& (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))^{\#_a})\tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&[ (id + i_1) \circ f , i_2 \circ h ]^\#
|
|
|
|
|
\\=\;&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
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\
|
|
|
|
|
The second application of~\ref{law:uniformity} is non-trivial, using epicness of \(dstr^{-1}\):
|
|
|
|
|
@ -236,6 +331,7 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
|
|
|
|
|
\\=\;&[ (eval + i_1) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ]
|
|
|
|
|
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr \circ dstr^{-1}.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\qedhere
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
@ -270,19 +366,21 @@ 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}
|
|
|
|
|
|
|
|
|
|
We will need a notion of stability for \(\mathbf{K}\) to make progress, since we do not assume \(\C \) to be cartesian closed.
|
|
|
|
|
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}, 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=\&]
|
|
|
|
|
\[
|
|
|
|
|
\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}\]
|
|
|
|
|
\end{tikzcd}
|
|
|
|
|
\]
|
|
|
|
|
commutes.
|
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
|
|
@ -291,30 +389,32 @@ 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}, 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=\&]
|
|
|
|
|
\[
|
|
|
|
|
\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}\]
|
|
|
|
|
\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} 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\).
|
|
|
|
|
\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\).
|
|
|
|
|
|
|
|
|
|
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},
|
|
|
|
|
& \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},
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
|
|
|
|
|
|
|
|
|
|
@ -346,10 +446,10 @@ A symmetrical variant of the previous definition is sometimes useful.
|
|
|
|
|
\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}}
|
|
|
|
|
& 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}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
|
|
|
|
|
|
|
|
|
|
@ -364,15 +464,13 @@ A symmetrical variant of the previous definition is sometimes useful.
|
|
|
|
|
This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows symmetrically.
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
In a less general setting stability indeed follows automatically.
|
|
|
|
|
|
|
|
|
|
\todo[inline]{Fix proof, replace free object operator, fix references.}
|
|
|
|
|
In a less general setting stability would indeed follow automatically.
|
|
|
|
|
|
|
|
|
|
\begin{theorem}\label{thm:stability}
|
|
|
|
|
In a cartesian closed category every free Elgot algebra is stable.
|
|
|
|
|
In a Cartesian closed category every free Elgot algebra is stable.
|
|
|
|
|
\end{theorem}
|
|
|
|
|
\begin{proof}
|
|
|
|
|
Let \(\C\) be cartesian closed and let \((KX, (-)^\#, \free{(-)})\) be a free Elgot algebra on some \(X \in \obj{\C}\).
|
|
|
|
|
Let \(\C\) be Cartesian closed and let \((KX, {(-)}^\sharp, \free{(-)})\) 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\).
|
|
|
|
|
We will now verify that this does indeed satisfy the requisite properties, i.e.
|
|
|
|
|
@ -384,17 +482,15 @@ In a less general setting stability indeed follows automatically.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
and for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\):
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& eval \circ (\free{curry\;f} \times id) \circ (h^{\#_a} \times id)
|
|
|
|
|
\\=\;&eval \circ ((\free{curry\;f} \circ h^{\#_a}) \times id)
|
|
|
|
|
\\=\;&eval \circ (curry(((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\#_b})) \times id)
|
|
|
|
|
\\=\;&((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\#_b}
|
|
|
|
|
\\=\;&((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))^{\#_b}
|
|
|
|
|
\\=\;&((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))^{\#_b}
|
|
|
|
|
\\=\;&(((eval \circ (\free{curry\;f} \times id)) + id) \circ dstr \circ (h \times id))^{\#_b}.
|
|
|
|
|
& 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}.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
\unsure[inline]{Maybe prove that curry is injective in preliminaries.}
|
|
|
|
|
|
|
|
|
|
Lastly, we need to check uniqueness of \(\ls{f}\). Let us consider a left iteration preserving morphism \(g : KY \times X \rightarrow A\) that satisfies \(g \circ (\eta \times id) = f\). Since \(curry\) is an injective mapping it suffices to show that
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& curry\;\ls{f}
|
|
|
|
|
@ -404,17 +500,15 @@ In a less general setting stability indeed follows automatically.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
Where the last step is the only non-trivial one. Since \(\free{curry\;f}\) is a unique iteration preserving morphism satisfying \(\free{curry\;f} \circ \eta = curry\;f\), we are left to show that \(g\) is also iteration preserving and satisfies the same property.
|
|
|
|
|
|
|
|
|
|
\unsure[inline]{Maybe prove helper lemmas about exponentials in preliminaries, like subst, beta and eta.}
|
|
|
|
|
|
|
|
|
|
Indeed,
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& curry\;g \circ h^{\#}
|
|
|
|
|
\\=\;&curry\;(g \circ (h^{\#} \times id))
|
|
|
|
|
\\=\;&curry\;(((g + id) \circ dstr \circ (h \times id))^{\#_a})
|
|
|
|
|
\\=\;&curry\;((((eval \circ (curry\; g \times id)) + id) \circ dstr \circ (h \times id))^{\#_a})
|
|
|
|
|
\\=\;&curry\;(((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))^{\#_a})
|
|
|
|
|
\\=\;&curry\;(((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))^{\#_a})
|
|
|
|
|
\\=\;&curry\;(((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))^{\#_a})
|
|
|
|
|
& 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})
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\), and
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
@ -428,11 +522,12 @@ In a less general setting stability indeed follows automatically.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
Let us first introduce a proof principle similar to \autoref{rem:coinduction}.
|
|
|
|
|
Let us first introduce a proof principle similar to the one introduced in \autoref{rem:coinduction}.
|
|
|
|
|
\begin{remark}[Proof by right-stability]~\label{rem:proofbystability}
|
|
|
|
|
Given two morphisms \(g, h : X \times KY \rightarrow A\) where \(X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}\). To show that \(g = h\), it suffices to show that \(g\) and \(h\) are right iteration preserving and there exists a morphism \(f : X \times Y \rightarrow A\) such that
|
|
|
|
|
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJBIl0sWzAsMiwiWCBcXHRpbWVzIFkiXSxbMCwxLCJnIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImgiLDIseyJvZmZzZXQiOjF9XSxbMiwxLCJmIiwyXSxbMiwwLCJpZCBcXHRpbWVzIFxcZXRhIl1d
|
|
|
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
|
|
|
\[
|
|
|
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
|
|
|
{X \times KY} \&\& A \\
|
|
|
|
|
\\
|
|
|
|
|
{X \times Y}
|
|
|
|
|
@ -440,14 +535,16 @@ Let us first introduce a proof principle similar to \autoref{rem:coinduction}.
|
|
|
|
|
\arrow["h"', shift right, from=1-1, to=1-3]
|
|
|
|
|
\arrow["f"', from=3-1, to=1-3]
|
|
|
|
|
\arrow["{id \times \eta}", from=3-1, to=1-1]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
\end{tikzcd}
|
|
|
|
|
\]
|
|
|
|
|
commutes.
|
|
|
|
|
\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 : KX \times Y \rightarrow A\) where \(X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}\). To show that \(g = h\), it suffices to show that \(g\) and \(h\) are left iteration preserving and there exists a morphism \(f : X \times Y \rightarrow A\) such that
|
|
|
|
|
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJLWCBcXHRpbWVzIFkiXSxbMiwwLCJBIl0sWzAsMiwiWCBcXHRpbWVzIFkiXSxbMCwxLCJnIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImgiLDIseyJvZmZzZXQiOjF9XSxbMiwxLCJmIiwyXSxbMiwwLCJcXGV0YSBcXHRpbWVzIGlkIl1d
|
|
|
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
|
|
|
\[
|
|
|
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
|
|
|
{KX \times Y} \&\& A \\
|
|
|
|
|
\\
|
|
|
|
|
{X \times Y}
|
|
|
|
|
@ -455,7 +552,8 @@ Of course there is also a symmetric version of this.
|
|
|
|
|
\arrow["h"', shift right, from=1-1, to=1-3]
|
|
|
|
|
\arrow["f"', from=3-1, to=1-3]
|
|
|
|
|
\arrow["{\eta \times id}", from=3-1, to=1-1]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
\end{tikzcd}
|
|
|
|
|
\]
|
|
|
|
|
commutes.
|
|
|
|
|
\end{remark}
|
|
|
|
|
|
|
|
|
|
@ -469,7 +567,8 @@ Of course there is also a symmetric version of this.
|
|
|
|
|
|
|
|
|
|
Naturality of \(\tau \) follows by:
|
|
|
|
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
\[
|
|
|
|
|
\begin{tikzcd}
|
|
|
|
|
& {A \times KB} && {X \times KY} \\
|
|
|
|
|
\\
|
|
|
|
|
& {K(A \times B)} && {K(X \times Y)} \\
|
|
|
|
|
@ -480,14 +579,15 @@ Of course there is also a symmetric version of this.
|
|
|
|
|
\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}\]
|
|
|
|
|
\end{tikzcd}
|
|
|
|
|
\]
|
|
|
|
|
|
|
|
|
|
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^\#)
|
|
|
|
|
\\=\;&\tau \circ (f \times ((Kg + id) \circ h)^\#)
|
|
|
|
|
\\=\;&((\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)))^\# \circ (f \times id)
|
|
|
|
|
\\=\;&(((\tau \circ (f \times Kg)) + id) \circ dstl \circ (id \times h))^\#.\tag{\ref{law:uniformity}}
|
|
|
|
|
& \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}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
% where uniformity is justified by
|
|
|
|
|
@ -498,14 +598,14 @@ Of course there is also a symmetric version of this.
|
|
|
|
|
|
|
|
|
|
% Both sides of the identity are right iteration preserving, since for any \(Z \in \obj{\C}\) and \(h : Z \rightarrow KY + Z\):
|
|
|
|
|
% \begin{alignat*}{1}
|
|
|
|
|
% &K(f \times g) \circ \tau \circ (id \times h^\#)
|
|
|
|
|
% \\=\;&K(f \times g) \circ ((\tau + id) \circ dstl \circ (id \times h))^\#
|
|
|
|
|
% \\=\;&(((K(f \times g) \circ \tau) + id) \circ dstl \circ (id \times h))^\#
|
|
|
|
|
% &K(f \times g) \circ \tau \circ (id \times h^\sharp)
|
|
|
|
|
% \\=\;&K(f \times g) \circ ((\tau + id) \circ dstl \circ (id \times h))^\sharp
|
|
|
|
|
% \\=\;&(((K(f \times g) \circ \tau) + id) \circ dstl \circ (id \times h))^\sharp
|
|
|
|
|
% \end{alignat*}
|
|
|
|
|
% and
|
|
|
|
|
% \begin{alignat*}{1}
|
|
|
|
|
% &\tau \circ (f \times Kg) \circ (id \times h^\#)
|
|
|
|
|
% \\=\;&\tau \circ (f \times (Kg \circ h)^\#)
|
|
|
|
|
% &\tau \circ (f \times Kg) \circ (id \times h^\sharp)
|
|
|
|
|
% \\=\;&\tau \circ (f \times (Kg \circ h)^\sharp)
|
|
|
|
|
% \\=\;&
|
|
|
|
|
% \end{alignat*}
|
|
|
|
|
|
|
|
|
|
@ -564,14 +664,14 @@ Of course there is also a symmetric version of this.
|
|
|
|
|
|
|
|
|
|
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^\#)
|
|
|
|
|
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle \circ (id \times h^\#)
|
|
|
|
|
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , h^\# \circ \pi_2 \rangle \rangle
|
|
|
|
|
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ (id \times h^\#) \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))^\# \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
|
|
|
|
|
\\=\;&\tau \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))^\#) \circ \alpha
|
|
|
|
|
\\=\;&((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))^\# \circ \alpha
|
|
|
|
|
\\=\;&(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))^\#.\tag{\ref{law:uniformity}}
|
|
|
|
|
& \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}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{proof}
|
|
|
|
|
@ -597,12 +697,12 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
and for any \(h : Z \rightarrow KX + Z\)
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \sigma \circ (h^\# \times id)
|
|
|
|
|
\\=\;&Kswap \circ \tau \circ swap \circ (h^\# \times id)
|
|
|
|
|
\\=\;&Kswap \circ \tau \circ (id \times h^\#) \circ swap
|
|
|
|
|
\\=\;&Kswap \circ ((\tau + id) \circ dstl \circ (id \times h))^\# \circ swap
|
|
|
|
|
\\=\;&(((Kswap \circ \tau) + id) \circ dstl \circ (id \times h))^\# \circ swap
|
|
|
|
|
\\=\;&((\sigma + id) \circ dstr \circ (h \times id))^\#.\tag{\ref{law:uniformity}}
|
|
|
|
|
& \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}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
Let us now proceed with the properties of \(\tau \) and \(\sigma \).
|
|
|
|
|
@ -632,84 +732,68 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
|
|
|
|
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)^\# \times ((\eta + id) \circ g)^\#) = \sigma^* \circ \tau \circ (((\eta + id) \circ f)^\# \times ((\eta + id) \circ g)^\#).\]
|
|
|
|
|
\[\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}^\# \circ \pi_1 = [ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\#\) and \(\hat{g}^\# \circ \pi_2 = [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^* \circ w^\# \), then
|
|
|
|
|
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
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \tau^* \circ \sigma \circ (\hat{f}^\# \times \hat{g}^\#)
|
|
|
|
|
\\=\;&\tau^* \circ \sigma \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\# \times w^\#)
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ \sigma \circ (id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\# \times w^\#)
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ \sigma \circ (w^\# \times w^\#)
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ \tau \circ \Delta \circ w^\#
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ K\langle \eta , id \rangle \circ w^\#\tag{\ref{thm:Klifting}}
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ K\langle id , \eta \rangle \circ w^\#
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K\langle id , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle \circ w^\#
|
|
|
|
|
\\=\;&\tau^* \circ {(\sigma \circ \langle[ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle)}^* \circ w^\#
|
|
|
|
|
\\=\;&\tau^* \circ {(\sigma \circ [\langle \hat{f}^\# \circ \pi_1 , \eta \circ \pi_2 \rangle , \langle \eta \circ \pi_1 , \hat{g}^\# \circ \pi_2 \rangle])}^* \circ w^\#
|
|
|
|
|
\\=\;&{(\tau^* \circ \sigma \circ [\hat{f}^\# \times \eta , \eta \times \hat{g}^\#])}^* \circ w^\#
|
|
|
|
|
\\=\;&([\tau^* \circ \sigma \circ (\hat{f}^\# \times \eta) , \tau^* \circ \sigma \circ {(\eta \times \hat{g}^\#)])}^* \circ w^\#
|
|
|
|
|
\\=\;&([\tau^* \circ K(id \times \eta) \circ \sigma \circ (\hat{f}^\# \times id) , \tau^* \circ \eta \circ {(id \times \hat{g}^\#)])}^* \circ w^\#
|
|
|
|
|
\\=\;&([\sigma \circ (\hat{f}^\# \times id) , \tau \circ {(id \times \hat{g}^\#)])}^* \circ w^\#,
|
|
|
|
|
& \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)
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ \sigma \circ (id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\sharp \times w^\sharp)
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ \sigma \circ (w^\sharp \times w^\sharp)
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ \tau \circ \Delta \circ w^\sharp
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^*
|
|
|
|
|
\\&\hphantom{\tau^* }\circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ K\langle \eta , id \rangle \circ w^\sharp\tag{\autoref{thm:Klifting}}
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ K\langle id , \eta \rangle \circ w^\sharp
|
|
|
|
|
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K\langle id , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle \circ w^\sharp
|
|
|
|
|
\\=\;&\tau^* \circ {(\sigma \circ \langle[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle)}^* \circ w^\sharp
|
|
|
|
|
\\=\;&\tau^* \circ {(\sigma \circ [\langle \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_2 \rangle , \langle \eta \circ \pi_1 , \hat{g}^\sharp \circ \pi_2 \rangle])}^* \circ w^\sharp
|
|
|
|
|
\\=\;&{(\tau^* \circ \sigma \circ [\hat{f}^\sharp \times \eta , \eta \times \hat{g}^\sharp])}^* \circ w^\sharp
|
|
|
|
|
\\=\;&([\tau^* \circ \sigma \circ (\hat{f}^\sharp \times \eta) , \tau^* \circ \sigma \circ {(\eta \times \hat{g}^\sharp)])}^* \circ w^\sharp
|
|
|
|
|
\\=\;&([\tau^* \circ K(id \times \eta) \circ \sigma \circ (\hat{f}^\sharp \times id) , \tau^* \circ \eta \circ {(id \times \hat{g}^\sharp)])}^* \circ w^\sharp
|
|
|
|
|
\\=\;&([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ {(id \times \hat{g}^\sharp)])}^* \circ w^\sharp,
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
\todo[inline]{Full proofs or `symmetric' enough?}
|
|
|
|
|
and by a symmetric argument also
|
|
|
|
|
\[\sigma^* \circ \tau \circ (\hat{f}^\# \times \hat{g}^\#) = ([\sigma \circ (\hat{f}^\# \times id) , \tau \circ {(id \times \hat{g}^\#)])}^* \circ w^\#.\]
|
|
|
|
|
% \begin{alignat*}{1}
|
|
|
|
|
% &\sigma^* \circ \tau \circ (\hat{f}^\# \times \hat{g}^\#)
|
|
|
|
|
% \\=\;&\sigma^* \circ \tau \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\# \times w^\#)
|
|
|
|
|
% \\=\;&\sigma^* \circ (\tau \circ {(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))}^* \circ \tau \circ ([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ (w^\# \times w^\#)
|
|
|
|
|
% \\=\;&\sigma^* \circ (\tau \circ {(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))}^* \circ K([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ \tau \circ (w^\# \times w^\#)
|
|
|
|
|
% \\=\;&\sigma^* \circ (\tau \circ {(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))}^* \circ K([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ \tau \circ \Delta \circ w^\#\tag{\ref{thm:Klifting}}
|
|
|
|
|
% \\=\;&\sigma^* \circ (\tau \circ {(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))}^* \circ K([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \times id) \circ K\langle \eta , id \rangle \circ w^\#
|
|
|
|
|
% \\=\;&\sigma^* \circ (\tau \circ {(id \times [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]))}^* \circ K\langle[ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , id\rangle \circ w^\#
|
|
|
|
|
% \\=\;&\sigma^* \circ {(\tau \circ \langle [ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle)}^* \circ w^\#
|
|
|
|
|
% \\=\;&\sigma^* \circ {(\tau \circ \langle [ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\# \circ \pi_2 , \eta \circ \pi_2 ]\rangle)}^* \circ w^\#
|
|
|
|
|
% \\=\;&\sigma^* \circ {(\tau \circ [ \hat{f}^\# \times \eta , \eta \times \hat{g}^\# ])}^* \circ w^\#
|
|
|
|
|
% \\=\;&([ \sigma^* \circ \tau \circ (\hat{f}^\# \times \eta) , \sigma^* \circ \tau \circ {(\eta \times \hat{g}^\#) ])}^* \circ w^\#
|
|
|
|
|
% \\=\;&([ \sigma^* \circ \eta \circ (\hat{f}^\# \times id) , \sigma^* \circ K(\eta \times id) \circ \tau \circ {(id \times \hat{g}^\#) ])}^* \circ w^\#
|
|
|
|
|
% \\=\;&([ \sigma \circ (\hat{f}^\# \times id) , \tau \circ {(id \times \hat{g}^\#) ])}^* \circ w^\#.
|
|
|
|
|
% \end{alignat*}
|
|
|
|
|
\[\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.
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
\[[ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\# = ([ i_1 \circ \pi_1 , (\hat{f}^\# \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\# = \hat{f}^\# \circ \pi_1. \]
|
|
|
|
|
\[[ \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}
|
|
|
|
|
& [ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\#
|
|
|
|
|
\\=\;&(([ \hat{f}^\# \circ \pi_1 , \eta \circ \pi_1 ]^* + id) \circ w)^\#
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\# \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\# \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times (\eta + id)) \circ (id \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\# \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ ((id \times \eta) + id) \circ dstl \circ (id \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\# \circ \pi_1)}^* \circ \tau \circ (id \times \eta) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ \hat{f}^\# \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \hat{f} \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#\tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \pi_1 \circ (\hat{f} \times id) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ ((\hat{f} \times id) + (\hat{f} \times id)) \circ dstl \circ (id \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ (\pi_1 + \pi_1) \circ dstr , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ (dstr + dstr) \circ dstl \circ (\hat{f} \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\#] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ [ i_1 + i_1 , i_2 + i_2 ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
|
|
|
|
|
\\=\;&([ [ i_1 \circ [id , \hat{f}^\#] \circ i_1 \circ \pi_1 , i_1 \circ K\pi_1 \circ \sigma ] , [ i_1 \circ [id , \hat{f}^\#] \circ i_2 \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
|
|
|
|
|
\\=\;&([ [ i_1 \circ \pi_1 , i_1 \circ \pi_1 ] , [ i_1 \circ \hat{f}^\# \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ [ \pi_1 , \pi_1 ] , (\hat{f}^\# \circ \pi_1 + id) ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , (\hat{f}^\# \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\#
|
|
|
|
|
& [ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\sharp
|
|
|
|
|
\\=\;&(([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* + id) \circ w)^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times (\eta + id)) \circ (id \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ ((id \times \eta) + id) \circ dstl \circ (id \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau \circ (id \times \eta) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ \hat{f}^\sharp \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \hat{f} \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp\tag{\ref{law:fixpoint}}
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 \circ (\hat{f} \times id) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ ((\hat{f} \times id) + (\hat{f} \times id)) \circ dstl \circ (id \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) \circ dstr , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ (dstr + dstr) \circ dstl \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ [ i_1 + i_1 , i_2 + i_2 ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\\=\;&([ [ i_1 \circ [id , \hat{f}^\sharp] \circ i_1 \circ \pi_1 , i_1 \circ K\pi_1 \circ \sigma ] , [ i_1 \circ [id , \hat{f}^\sharp] \circ i_2 \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\\=\;&([ [ i_1 \circ \pi_1 , i_1 \circ \pi_1 ] , [ i_1 \circ \hat{f}^\sharp \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ [ \pi_1 , \pi_1 ] , (\hat{f}^\sharp \circ \pi_1 + id) ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\sharp
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
and
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \hat{f}^\# \circ \pi_1
|
|
|
|
|
\\=\;&((id + \Delta) \circ h)^\# \tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&([ i_1 , ((id + \Delta) \circ h)^\# + id] \circ h)^\# \tag{\ref{law:diamond}}
|
|
|
|
|
\\=\;&([ i_1 , (\hat{f}^\# \circ \pi_1) + id ] \circ h)^\# \tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \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))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ ((\pi_1 \times id) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ \langle \pi_1 , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 \circ (id \times g) , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ (id \times g) ] \circ dstr \circ (\hat{f} \times id))^\#
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\#,
|
|
|
|
|
& \hat{f}^\sharp \circ \pi_1
|
|
|
|
|
\\=\;&((id + \Delta) \circ h)^\sharp \tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&([ i_1 , ((id + \Delta) \circ h)^\sharp + id] \circ h)^\sharp \tag{\ref{law:diamond}}
|
|
|
|
|
\\=\;&([ i_1 , (\hat{f}^\sharp \circ \pi_1) + id ] \circ h)^\sharp \tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \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))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ ((\pi_1 \times id) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ \langle \pi_1 , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\sharp
|
|
|
|
|
\\=\;&([ i_1 \circ \pi_1 \circ (id \times g) , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ (id \times g) ] \circ dstr \circ (\hat{f} \times id))^\sharp
|
|
|
|
|
\\=\;&([ 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
|
|
|
|
|
@ -732,7 +816,8 @@ The following Lemma is central to the proof of commutativity.
|
|
|
|
|
\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=
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
\[
|
|
|
|
|
\begin{tikzcd}
|
|
|
|
|
& {KX \times KY} && {K(KX \times Y)} \\
|
|
|
|
|
\\
|
|
|
|
|
& {K(X \times KY)} && {K(X \times Y)} \\
|
|
|
|
|
@ -743,7 +828,8 @@ The following Lemma is central to the proof of commutativity.
|
|
|
|
|
\arrow["{\tau^*}"', from=3-2, to=3-4]
|
|
|
|
|
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
|
|
|
|
|
\arrow["{\sigma}"', curve={height=12pt}, from=4-1, to=3-4]
|
|
|
|
|
\end{tikzcd}\]
|
|
|
|
|
\end{tikzcd}
|
|
|
|
|
\]
|
|
|
|
|
|
|
|
|
|
The diagram commutes since
|
|
|
|
|
\[\sigma^* \circ \tau \circ (id \times \eta) = \sigma^* \circ \eta = \sigma \]
|
|
|
|
|
@ -751,75 +837,77 @@ The following Lemma is central to the proof of commutativity.
|
|
|
|
|
\[\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^\#) = \sigma^* ((\tau + id) \circ dstl \circ (id \times h))^\# = (((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))^\#. \]
|
|
|
|
|
\[\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=
|
|
|
|
|
\[\begin{tikzcd}
|
|
|
|
|
\[
|
|
|
|
|
\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["{id \times h^\sharp}", from=2-1, to=1-5]
|
|
|
|
|
\arrow["{((\psi + id) \circ dstl \circ (id \times h))^\sharp}"', 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}\]
|
|
|
|
|
\arrow["{\tau \circ (id \times h^\sharp)}"', from=4-1, to=2-5]
|
|
|
|
|
\end{tikzcd}
|
|
|
|
|
\]
|
|
|
|
|
which commutes, since
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \psi \circ (id \times h^\#) \circ (\eta \times id)
|
|
|
|
|
\\=\;&\psi \circ (\eta \times id) \circ (id \times h^\#)
|
|
|
|
|
\\=\;&\tau^* \circ \eta \circ (id \times h^\#)
|
|
|
|
|
\\=\;&\tau \circ (id \times h^\#)
|
|
|
|
|
\\=\;&((\tau + id) \circ dstl \circ (id \times h))^\#
|
|
|
|
|
\\=\;&((\psi + id) \circ dstl \circ (id \times h))^\# \circ (\eta \times id).\tag{\ref{law:uniformity}}
|
|
|
|
|
& \psi \circ (id \times h^\sharp) \circ (\eta \times id)
|
|
|
|
|
\\=\;&\psi \circ (\eta \times id) \circ (id \times h^\sharp)
|
|
|
|
|
\\=\;&\tau^* \circ \eta \circ (id \times h^\sharp)
|
|
|
|
|
\\=\;&\tau \circ (id \times h^\sharp)
|
|
|
|
|
\\=\;&((\tau + id) \circ dstl \circ (id \times h))^\sharp
|
|
|
|
|
\\=\;&((\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^\#)\) and \(((\psi + id) \circ dstl \circ (id \times h))^\# \) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi \circ (id \times h^\#)\) 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^\#) \circ (g^\# \times id)
|
|
|
|
|
\\=\;&\psi \circ (g^\# \times id) \circ (id \times h^\#)
|
|
|
|
|
\\=\;&\tau^* \circ ((\sigma + id) \circ dstr \circ (g \times id))^\# \circ (id \times h^\#)
|
|
|
|
|
\\=\;&((\psi + id) \circ dstr \circ (g \times id))^\# \circ (id \times h^\#)
|
|
|
|
|
\\=\;&(((\psi \circ (id \times h^\#)) + id) \circ dstr \circ (g \times id))^\#.\tag{\ref{law:uniformity}}
|
|
|
|
|
& \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}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
Lastly, we need to show that
|
|
|
|
|
\[((\psi + id) \circ dstl \circ (id \times h))^\# \circ (g^\# \times id) = ((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#.\]
|
|
|
|
|
Note that by \ref{law:uniformity} the left-hand side can be rewritten as
|
|
|
|
|
\[((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\#.\]
|
|
|
|
|
\[((\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.\]
|
|
|
|
|
|
|
|
|
|
Consider now, that
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& ((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#
|
|
|
|
|
\\=\;&(((((\psi + id) \circ dstl \circ {(id \times h))^\#)}^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))^\#
|
|
|
|
|
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\#)}^* \circ ((\eta + id) \circ dstr \circ (g \times id))^\#
|
|
|
|
|
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\#)}^* \circ (((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))^\#
|
|
|
|
|
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\#)}^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&(((\psi^* + id) \circ (\eta + id) \circ dstl \circ {(id \times h))^\#)}^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ {(id \times h))^\#)}^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ {(id \times h))^\#)}^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ ((((\tau \circ (id \times \eta)) + id) \circ dstl \circ {(id \times h))^\#)}^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ (((\tau + id) \circ dstl \circ (id \times ({(\eta + id) \circ h)))^\#)}^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ (\tau \circ (id \times ({(\eta + id) \circ h)^\#))}^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ \tau^* \circ K(id \times ((\eta + id) \circ h)^\#) \circ \sigma \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times ((\eta + id) \circ h)^\#) \circ (((\eta + id) \circ g)^\# \times id)
|
|
|
|
|
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#),
|
|
|
|
|
& ((((\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))^\# + id) \circ dstl \circ (id \times h))^\#
|
|
|
|
|
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#).
|
|
|
|
|
& ((((\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))^\# \circ (g^\# \times id)
|
|
|
|
|
\\=\;&((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\#\tag{\ref{law:uniformity}}
|
|
|
|
|
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#)
|
|
|
|
|
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#)\tag{\ref{lem:KCommKey}}
|
|
|
|
|
\\=\;&((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#.
|
|
|
|
|
& ((\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.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
@ -840,22 +928,22 @@ The following Lemma is central to the proof of commutativity.
|
|
|
|
|
|
|
|
|
|
For iteration preservation of \(\tau \circ \Delta \) consider \(Z \in \obj{\C}\) and \(h : Z \rightarrow KX + Z\), then
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& \tau \circ \Delta \circ h^{\#}
|
|
|
|
|
\\=\;&\tau \circ \langle h^{\#} , h^{\#} \rangle
|
|
|
|
|
\\=\;&\tau \circ (id \times h^{\#}) \circ \langle h^{\#} , id \rangle
|
|
|
|
|
\\=\;&((\tau + id) \circ dstl \circ (id \times f))^\# \circ \langle h^{\#} , id \rangle
|
|
|
|
|
\\=\;&(((\tau \circ \Delta) + id) \circ f)^\#.\tag{\ref{law:uniformity}}
|
|
|
|
|
& \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}}
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
|
|
|
|
|
Note that by monicity of \(dstl^{-1}\) and by~\ref{law:fixpoint}
|
|
|
|
|
\[(\Delta + \langle f^\# , id \rangle) \circ f = dstl \circ \langle f^\# , f \rangle. \]
|
|
|
|
|
The application of \ref{law:uniformity} is then justified by
|
|
|
|
|
\[(\Delta + \langle f^\sharp , id \rangle) \circ f = dstl \circ \langle f^\sharp , f \rangle. \]
|
|
|
|
|
The application of~\ref{law:uniformity} is then justified by
|
|
|
|
|
\begin{alignat*}{1}
|
|
|
|
|
& (id + \langle f^\# , id \rangle) \circ ((\tau \circ \Delta) + id) \circ f
|
|
|
|
|
\\=\;&((\tau \circ \Delta) + \langle f^\# , id \rangle) \circ f
|
|
|
|
|
\\=\;&(\tau + id) \circ (\Delta + \langle f^\# , id \rangle) \circ f
|
|
|
|
|
\\=\;&(\tau + id) \circ dstl \circ \langle f^\# , f \rangle
|
|
|
|
|
\\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\# , id \rangle.
|
|
|
|
|
& (id + \langle f^\sharp , id \rangle) \circ ((\tau \circ \Delta) + id) \circ f
|
|
|
|
|
\\=\;&((\tau \circ \Delta) + \langle f^\sharp , id \rangle) \circ f
|
|
|
|
|
\\=\;&(\tau + id) \circ (\Delta + \langle f^\sharp , id \rangle) \circ f
|
|
|
|
|
\\=\;&(\tau + id) \circ dstl \circ \langle f^\sharp , f \rangle
|
|
|
|
|
\\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\sharp , id \rangle.
|
|
|
|
|
\end{alignat*}
|
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
|
@ -866,9 +954,9 @@ 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, {(-)}^{\#_T})\]
|
|
|
|
|
\[\mathbf{T} = (T , \eta^T, \mu^T, {(-)}^{\sharp_T})\]
|
|
|
|
|
and
|
|
|
|
|
\[\mathbf{K} = (K , \eta^K, \mu^T, {(-)}^{\#_K}).\]
|
|
|
|
|
\[\mathbf{K} = (K , \eta^K, \mu^T, {(-)}^{\sharp_K}).\]
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
