{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QGiven a functor \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a (H-)guarded Elgot algebra consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a H-algebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying the following axioms: law:guardedfixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardeduniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardedcompositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QAn Elgot monad consists of A monad \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Naturality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Codiagonal: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid function, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QGiven a function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the lifted function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is defined as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QConsider, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a setoid function that maps every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"IF_IS","sentence":"^\\QNow, consider the following function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which tries running two computations and returns the one that finished first: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QLastly, consider the function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which adds a number of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q constructors in front of a value and is given by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QConsider another setoid function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QNext, let us consider functions for counting steps of computations, first regard \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which returns the number of steps a terminating computation has to take and is defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QConsider \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"IF_IS","sentence":"^\\QFurthermore, consider the setoid function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Now, by coinduction we can easily follow that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
@ -177,7 +177,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\]
\end{definition}
\begin{lemma}
\begin{proposition}
Every exponential object \(X^Y\) satisfies the following properties:
\begin{enumerate}
@ -185,7 +185,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\item\(curry(eval \circ(f \times id))= f\) for any \(f : X \times Y \rightarrow Z\)
\item\(curry\;f \circ g = curry(f \circ(g \times id))\) for any \(f : X \times Y \rightarrow Z, g : A \rightarrow X\)
\end{enumerate}
\end{lemma}
\end{proposition}
\begin{proof}
\begin{enumerate}
\item Let \(f, g : X \times Y \rightarrow Z\) and \(curry\;f = curry\;g\), then indeed
@ -394,8 +394,8 @@ This yields the category of programs for a Kleisli triple that is called the Kle
The laws of categories then follow from the Kleisli triple laws.
\end{definition}
\begin{theorem}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
\end{theorem}
\begin{proposition}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
\end{proposition}
\begin{proof}
The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out.
@ -505,10 +505,10 @@ to establish some notation and then describe how to obtain a monad via existence
\]
\end{definition}
\begin{theorem}\label{thm:freemonad}
\begin{proposition}\label{thm:freemonad}
Let \(U : \C\rightarrow\D\) be a forgetful functor.
If for every \(X \in\obj{\D}\) a free object \(FX \in\obj{C}\) exists then \((X \mapsto UFX, \eta : X \rightarrow UFX, \free{(f : X \rightarrow UFY)} : UFX \rightarrow UFY)\) is a Kleisli triple on \(\D\).
@ -21,23 +21,15 @@ To ensure that programs are partial, we recall the following notion by Cockett a
\begin{definition}[Restriction Structure]
A restriction structure on a category \(\mathcal{C}\) is a mapping \(dom : \mathcal{C}(X, Y)\rightarrow\mathcal{C}(X , X)\) with the following properties:
for any \(X, Y, Z \in\vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z\).
\end{definition}
\begin{lemma}
For any \(f : X \rightarrow Y\) the restriction morphism \(\tdom f\) is idempotent.
\end{lemma}
\begin{proof}
This follows by~\ref{R3} and~\ref{R1}:
\[\tdom f \circ\tdom f =\tdom(f \circ\tdom f)=\tdom f\tag*{\qedhere}\]
\end{proof}
The idempotent morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
The morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
\[
(\tdom f)(x) = \begin{cases}
@ -55,7 +47,7 @@ That is, \(\tdom f\) is only defined on values where \(f\) is defined and for th
For a suitable defined partiality monad \(T\) the Kleisli category \(\C^T\) should be a restriction category.
Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
Lastly, we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
The other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness.
@ -131,20 +123,20 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
\end{tikzcd}
\]
This is easily proven by pre-composing with \(i_1\) and \(i_2\):
This is easily proven by pre-composing with \(i_1\) and \(i_2\), indeed
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_2) \circ\langle i_2 , id \rangle
\\=\;&(id\;+\;!) \circ i_2 \circ\langle i_2 , id \rangle
\\=\;&i_2 \;\circ\; ! \circ\langle i_2 , id \rangle
\\=\;&i_2 \;\circ\; !\tag*{\qedhere}
\\=\;&i_2 \;\circ\; !.\tag*{\qedhere}
\end{alignat*}
\end{proof}
@ -152,7 +144,7 @@ In the setting of classical mathematics this monad is therefore sufficient for m
\section{The Delay Monad}
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow D\;X\) and \(later : D\;X \rightarrow D\;X\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} or~\cite{delay}, for a type theoretical study of this monad.
This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} for a type theoretical study of this monad.
Categorically we obtain the delay monad by the final F-coalgebras \(DX =\nu A. X + A\), which we assume to exist. In this section we will show that these final F-coalgebras indeed yield a monad that is strong and commutative.
Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} the coalgebra structure \(out : DX \rightarrow X + DX\) is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: \(out^{-1}=[ now , later ] : X + DX \rightarrow DX\).
@ -225,14 +217,13 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
\\=\;&(id + \coalg{\alpha}\circ i_2) \circ out
\end{alignat*}
Let us verify that \(f^*\) indeed satisfies the requisite property:
\begin{alignat*}{1}
& out \circ\coalg{\alpha}\circ i_1
\\=\;&(id + \coalg{\alpha}) \circ\alpha\circ i_1
\\=\;&(id + \coalg{\alpha}) \circ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out
\\=\;&[ [ (id + \coalg{\alpha}) \circ i_1 , (id + \coalg{\alpha}) \circ i_2 \circ i_2 ] \circ out \circ f , (id + \coalg{\alpha}) \circ i_2 \circ i_1 ] \circ out
\\=\;&[ [ i_1 , i_2 \circ\coalg{\alpha}\circ i_2 ] \circ out \circ f , i_2 \circ\coalg{\alpha}\circ i_1 ] \circ out
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out.
\end{alignat*}
We are left to check uniqueness of \(f^*\). Let \(g : DX \rightarrow DY\) and \(out \circ g =[ out \circ f , i_2\circ g ]\circ out\).
@ -245,39 +236,39 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
\\=\;&[ [ [ i_1 , i_2 \circ [g , id] \circ i_2 ] \circ out \circ f , i_2 \circ [g , id] \circ i_1 ] \circ out , (id + [g , id] \circ i_2) \circ out ]
\\=\;&[ [ [ (id + [g , id]) \circ i_1 , (id + [g , id]) \circ i_2 \circ i_2 ] \circ out \circ f , (id + [g , id]) \circ i_2 \circ i_1 ] \circ out
\\\;&, (id + [g , id]) \circ (id + i_2) \circ out ]
\\=\;&(id + [g , id]) \circ [ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]
\\=\;&(id + [g , id]) \circ [ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ].
\end{alignat*}
Thus, \([ g , id ]=\coalg{\alpha}\) by uniqueness of \(\coalg{\alpha}\).
It follows:\[g =[ g , id ]\circ i_1=\;\coalg{\alpha}\circ i_1= f^*\]
\item[\ref{D3}] This follows immediately since \(\tau\) is the unique coalgebra morphism from \((X \times DY, dstl \circ(id \times out))\) into the terminal coalgebra \((D(X \times Y) , out)\).
It follows that indeed\[g =[ g , id ]\circ i_1=\;\coalg{\alpha}\circ i_1= f^*.\]
\item[\ref{D3}] Take \(\tau :=\coalg{dstl \circ(id \times out)} : X \times DY \rightarrowD(X \times Y)\), the requisite property then follows by definition.
\qedhere
\end{itemize}
\end{proof}
\begin{lemma}
The following properties follow from \autoref{lem:delay}:
\begin{proof} These identities follow by use of \autoref{lem:delay}:
\begin{itemize}
\item[1.] Note that definitionally: \(Df ={(now \circ f)}^*\) for any \(f : X \rightarrow TY\). The statement is then simply a consequence of~\ref{D1} and~\ref{D2}:
\begin{alignat*}{1}
& out \circ Df
\\=\;&out \circ{(now \circ f)}^*
\\=\;&[ out \circ now \circ f , i_2 \circ{(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
\\=\;&(f + Df) \circ out\tag*{\ref{D1}}
\\=\;&(f + Df) \circ out.\tag*{\ref{D1}}
\end{alignat*}
\item[2.] By uniqueness of \(f^*\) it suffices to show:
\begin{alignat*}{1}
& out \circ [ f , {(later \circ f)}^* ] \circ out
\\=\;&[ out \circ f , out \circ{(later \circ f)}^* ] \circ out
\\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ{(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
\\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D1}}
\\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out.\tag*{\ref{D1}}
\end{alignat*}
\item[3.]
These equations follow by monicity of \(out\):
@ -290,7 +281,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
\\=\;&i_2 \circ f^*\tag*{\ref{D1}}
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
\\=\;&out \circ f^* \circ later \tag*{\ref{D2}}
\\=\;&out \circ f^* \circ later.\tag*{\ref{D2}}
\end{alignat*}
\end{itemize}
Thus, the postulated properties have been proven.
@ -300,7 +291,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
\(\mathbf{D}=(D, now, {(-)}^*)\) is a Kleisli triple.
\end{theorem}
\begin{proof}
We will now use the properties proven in Corollary~\ref{lem:delay} to prove the Kleisli triple laws:
We will now use the properties proven in \autoref{lem:delay} to prove the Kleisli triple laws:
\begin{itemize}
\item[\ref{K1}]
By uniqueness of \(now^*\) it suffices to show that \(out \circ id =[ out \circ now , i_2\circ id ]\circ out\) which instantly follows by~\ref{D1}.
@ -309,7 +300,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
& out \circ f^* \circ now
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ now\tag*{\ref{D2}}
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_1\tag*{\ref{D1}}
\\=\;&out \circ f
\\=\;&out \circ f.
\end{alignat*}
\item[\ref{K3}] Let \(f : Y \rightarrow Z, g : X \rightarrow Z\) to show \(f^*\circ g^*={(f^*\circ g)}^*\) by uniqueness of \({(f^*\circ g)}^*\) it suffices to show:
\begin{alignat*}{1}
@ -317,7 +308,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ g^*\tag*{\ref{D2}}
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ [ out \circ g , i_2 \circ g^* ] \circ out\tag*{\ref{D2}}
\\=\;&[ [ out \circ f , i_2 \circ f^* ] \circ out \circ g , i_2 \circ f^* \circ g^* ] \circ out
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out\tag*{\ref{D2}}
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out.\tag*{\ref{D2}}
\end{alignat*}
\end{itemize}
This concludes the proof.
@ -386,19 +377,18 @@ Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}
\arrow["{\pi_2 + id}", from=1-3, to=1-4]
\end{tikzcd}
\]
\item[\ref{S2}] We don't need coinduction to show \(\tau\circ(id \times now)= now\), but we need a small helper lemma:
\item[\ref{S2}] We don't need coinduction to show \(\tau\circ(id \times now)= now\), but we will first need to establish
\begin{equation*}
\tau\circ (id \times out^{-1}) = out^{-1}\circ (id + \tau) \circ dstl \tag*{(\(\ast\))}\label{helper}
\tau\circ (id \times out^{-1}) = out^{-1}\circ (id + \tau) \circ dstl,\tag*{(\(\ast\))}\label{helper}
\end{equation*}
which is a direct consequence of~\ref{D3}.
With this the proof is straightforward:
With this we are done by
\begin{alignat*}{1}
&\tau\circ (id \times now) \\
=\;&\tau\circ (id \times out^{-1}) \circ (id \times i_1) \\
=\;& out^{-1}\circ (id + \tau) \circ dstl \circ (id \times i_1)\tag*{\ref*{helper}}\\
=\;& now
=\;& now.
\end{alignat*}
where the last step follows by \(dstl \circ(id \times i_1)= i_1\).
\item[\ref{S3}] We need to check \(\tau^*\circ\tau=\tau\circ(id \times id^*)\), the coalgebra for coinduction is:
@ -521,27 +511,28 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
Using \autoref{cor:solution} it suffices to show that both \(\tau^*\circ\sigma\) and \(\sigma^*\circ\tau\) are solutions of some guarded morphism \(g\).
Let \(w =(dstr + dstr)\circ dstl \circ(out \times out)\) and take
\[g = out^{-1}\circ[ i_1+ D i_1\circ\sigma , i_2\circ[ D i_1\circ\tau , later \circ now \circ i_2]]\circ w\]
\[g = out^{-1}\circ[ i_1+ D i_1\circ\sigma , i_2\circ[ D i_1\circ\tau , later \circ now \circ i_2]]\circ w.\]
\(g\) is trivially guarded by \([ id + D i_1\circ\sigma , i_2\circ[ D i_1\circ\tau , later \circ now \circ i_2]]\circ w\).
We are left to show that both \(\tau^*\circ\sigma\) and \(\sigma^*\circ\tau\) are solutions of \(g\). Consider:
We are left to show that both \(\tau^*\circ\sigma\) and \(\sigma^*\circ\tau\) are solutions of \(g\). Consider
\[\tau^*\circ\sigma= out^{-1}\circ[ id +\sigma , i_2\circ[\tau , later \circ\tau^*\circ\sigma]]\circ w ={[ now , \tau^*\circ\sigma]}^*\circ g \]
\[\sigma^*\circ\tau= out^{-1}\circ[ id +\sigma , i_2\circ[\tau , later \circ\sigma^*\circ\tau]]\circ w ={[ now , \sigma^*\circ\tau]}^*\circ g \]
\[\tau^*\circ\sigma= out^{-1}\circ[ id +\sigma , i_2\circ[\tau , later \circ\tau^*\circ\sigma]]\circ w ={[ now , \tau^*\circ\sigma]}^*\circ g, \]
and
\[\sigma^*\circ\tau= out^{-1}\circ[ id +\sigma , i_2\circ[\tau , later \circ\sigma^*\circ\tau]]\circ w ={[ now , \sigma^*\circ\tau]}^*\circ g. \]
The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\):
The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\)
\begin{alignat*}{1}
& out \circ{[ now , f ]}^* \circ out^{-1}\circ [ i_1 + D i_1 \circ\sigma , i_2 \circ [ D i_1 \circ\tau , later \circ now \circ i_2 ] ] \circ w
\\=\;& [ out \circ [ now , f ] , i_2 \circ{[ now , f ]}^* ] \circ [ i_1 + D i_1 \circ\sigma , i_2 \circ [ D i_1 \circ\tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}}
\\=\;& [ id + \sigma , i_2 \circ{[ now , f]}^* \circ [ D i_1 \circ\tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D1}}
\\=\;& [ id + \sigma , i_2 \circ [ \tau , {[ now , f]}^* \circ later \circ now \circ i_2 ] ] \circ w
\\=\;& [ id + \sigma , i_2 \circ [ \tau , {[ later \circ now , later \circ f]}^* \circ now \circ i_2 ] ] \circ w
\\=\;& [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w
\\=\;& [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w.
\end{alignat*}
Let us now check the first step in the equation for \(\sigma^*\circ\tau\), the same step for \(\tau^*\circ\sigma\) is then symmetric.
Again we proceed by monicity of \(out\):
Again, we proceed by monicity of \(out\), which yields
\begin{alignat*}{1}
& out \circ\sigma^* \circ\tau
\\=\;&[ out \circ\sigma , i_2 \circ\sigma^* ] \circ out \circ\tau\tag*{\ref{D2}}
@ -557,18 +548,17 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
\\=\;&[ (id + \sigma), i_2 \circ{(out^{-1}\circ (id + \sigma))}^* \circ [D i_1 \circ\tau , D i_2 \circ\tau]] \circ (dstr + dstr) \circ dstl \circ (out \times out)
\\=\;&[ (id + \sigma), i_2 \circ [{(out^{-1}\circ i_1)}^* \circ\tau , {(out^{-1}\circ i_2 \circ\sigma)}^* \circ\tau]] \circ w
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , {(later \circ\sigma)}^* \circ\tau]] \circ w \tag*{\ref{K1}}
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ\sigma^* \circ\tau]] \circ w
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ\sigma^* \circ\tau]] \circ w,
@ -40,8 +40,11 @@ The previous intuition gives rise to the following simpler definition that has b
\end{itemize}
\end{definition}
In this setting the simpler \ref{law:folding} axiom replaces the sophisticated \ref{law:guardedcompositionality} axiom. % chktex 2
Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the \ref{law:folding} and \ref{law:guardedcompositionality} axioms are equivalent, which is illustrated by the following Lemma. % chktex 2
Note that the \ref{law:uniformity} axiom requires an identity to be proven, before it can be applied. % chktex 2
However, we will omit these proofs in most parts of the thesis, since they mostly follow by simple rewriting on (co)products, the full proofs can be looked up in the accompanying formalization. % chktex 36
Now, in this setting the simpler \ref{law:folding} axiom replaces the sophisticated \ref{law:guardedcompositionality} axiom. % chktex 2
Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the \ref{law:folding} and \ref{law:guardedcompositionality} axioms are equivalent, which is partly illustrated by the following Lemma. % chktex 2
\begin{lemma}
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional axioms
@ -51,7 +54,7 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
\\ for any \(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 any \(f : X \rightarrow(Y + Y)+ X, h : Y \rightarrow A\),
Let us also consider the special case where \(X =1\).
@ -176,46 +179,46 @@ Let us now consider morphisms that are coherent with respect to the iteration op
for any \(h : Y \rightarrow A + Y\).
\end{definition}
The previous definition yields the category of Elgot algebras over a category \(\C\) and iteration preserving morphisms between these algebras. We call this category \(\elgotalgs{\C}\).
We will now study the category of Elgot algebras and iteration preserving morphisms that we call \(\elgotalgs{\C}\). Let us introduce notation for morphisms between Elgot algebras: we denote an Elgot algebra morphism \(f : (A , {(-)}^{\sharp_a})\rightarrow(B,{(-)}^{\sharp_b})\) as \(f : A \hookrightarrow B\), where we omit stating the iteration operator.
\begin{lemma}
\begin{lemma}\label{lem:elgotalgscat}
\(\elgotalgs{\C}\) is a category.
\end{lemma}
\begin{proof}
It suffices to show that the identity morphism in \(\C\) is iteration preserving and the composite of two iteration preserving morphisms is also iteration preserving.
Let \((A , {(-)}^{\sharp_a}), (B , {(-)}^{\sharp_b}), (C , {(-)}^{\sharp_c})\) be Elgot algebras.
Products and exponentials of Elgot algebras can be formed in a canonical way.
Products and exponentials of Elgot algebras can be formed in a canonical way, which is illustrated by the following two Lemmas.
\begin{lemma}\label{lem:elgotalgscat}
\begin{lemma}\label{lem:elgotalgscart}
If \(\C\) is a Cartesian category, so is \(\elgotalgs{\C}\).
\end{lemma}
\begin{proof}
Let \(1\) be the terminal object of \(\C\). Given \(f : X \rightarrow1+ X\) we define the iteration \(f^\sharp=\;! : X \rightarrow1\) 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 \rightarrow1\) extends to a morphism between Elgot algebras by uniqueness. % chktex 40
Let \((A, {(-)}^{\sharp_a}) , (B, {(-)}^{\sharp_b})\in\vert\elgotalgs{\C}\vert\) and \(A \times B\) be the product of \(A\) and \(B\) in \(\C\). Given \(f : X \rightarrow(A \times B)+ X\) we define the iteration as:
\[f^\sharp=\langle((\pi_1+ id)\circ f)^{\sharp_a} , {((\pi_2+ id)\circ f)}^{\sharp_b}\rangle : X \rightarrow A \times B\]
Next we show that \((A \times B, {(-)}^\sharp)\) is indeed an Elgot algebra:
Let \(A, B\in\vert\elgotalgs{\C}\vert\) and \(A \times B\) be the product of \(A\) and \(B\) in \(\C\). Given \(f : X \rightarrow(A \times B)+ X\) we define the iteration as:
\[f^\sharp=\langle{((\pi_1+ id)\circ f)}^{\sharp_a} , {((\pi_2+ id)\circ f)}^{\sharp_b}\rangle : X \rightarrow A \times B\]
Now, we show that \(A \times B\) indeed constitutes an Elgot algebra:
\begin{itemize}
\item\textbf{Fixpoint}: Let \(f : X \rightarrow(A \times B)+ X\). The requisite equation follows by the fixpoint identities of \(((\pi_1+ id)\circ f)^{\sharp_a}\) and \({((\pi_2+ id)\circ f)}^{\sharp_b}\):
\item\textbf{Fixpoint}: Let \(f : X \rightarrow(A \times B)+ X\). The requisite equation follows by the fixpoint identities of \({((\pi_1+ id)\circ f)}^{\sharp_a}\) and \({((\pi_2+ id)\circ f)}^{\sharp_b}\):
\\=\;&{[ (id + i_1) \circ (\pi_2 + id) \circ f , i_2 \circ h ]}^{\sharp_b}\tag{\ref{law:folding}}
\\=\;&(\pi_2 + id) \circ{[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_b}
\end{alignat*}
which concludes the proof of the folding law.
\end{itemize}
The product diagram of \(A \times B\) in \(\C\) then also holds in \(\elgotalgs{\C}\), we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism \(\langle f , g \rangle\) is iteration preserving for any \(f : (Z, {(-)}^{\sharp_z})\rightarrow(X, {(-)}^{\sharp_x}), g : (Z, {(-)}^{\sharp_z})\rightarrow(Y, {(-)}^{\sharp_y})\):
The product diagram of \(A \times B\) in \(\C\) then also holds in \(\elgotalgs{\C}\), we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism \(\langle f , g \rangle\) is iteration preserving for any \(f : C \hookrightarrow A, g : C \rightarrow B\) where \(C \in\obj{\elgotalgs{\C}}\).
Let \(h : X \rightarrowE + X\) where \(E \in\obj{\elgotalgs{\C}}\). We use the fact that \(f, g\) are iteration preserving to show:
Let \(h : X \rightarrowC + X\). We use the fact that \(f\) and \(g\) are iteration preserving to show:
\begin{alignat*}{1}
&\langle f , g \rangle\circ (h^{\sharp_e})
\\=\;&\langle f \circ (h^{\sharp_e}) , g \circ (h^{\sharp_e}) \rangle
\\=\;&\langle{((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_a} , {((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_b}\rangle
\end{alignat*}
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, we have shown that \(A \times B\) extends to a product in \(\elgotalgs{\C}\) and therefore \(\elgotalgs{\C}\) is Cartesian, assuming that\(\C\) is Cartesian.
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, it follows that \(A \times B\) extends to a product in \(\elgotalgs{\C}\) and therefore \(\elgotalgs{\C}\) is Cartesian, if\(\C\) is Cartesian.
\end{proof}
\begin{lemma}\label{lem:elgotexp}
Given \(X \in\obj{\C}\) and \((A, {(-)}^{\sharp_a})\in\vert\elgotalgs{\C}\vert\). The exponential \(X^A\) (if it exists) can be equipped with an Elgot algebra structure.
Given \(X \in\obj{\C}\) and \(A \in\obj{\elgotalgs{\C}}\). The exponential \(X^A\) (if it exists) can be equipped with an Elgot algebra structure.
\end{lemma}
\begin{proof}
Take \(f^\sharp= curry (((eval + id)\circ dstr \circ(f \times id))^{\sharp_a})\) as the iteration of some \(f : Z \rightarrow A^X + Z\).
Take \(f^\sharp= curry ({((eval + id)\circ dstr \circ(f \times id))}^{\sharp_a})\) as the iteration of some \(f : Z \rightarrow A^X + Z\).
\begin{itemize}
\item\textbf{Fixpoint}: Let \(f : Y \rightarrow X^A + Y\) with \(Y \in\obj{C}\). By uniqueness of \(f^\sharp= curry\;(((eval + id)\circ dstr \circ(f \times id))^{\sharp_a})\) it suffices to show:
\item\textbf{Fixpoint}: Let \(f : Y \rightarrow X^A + Y\). We need to show that \(f^\sharp=[ id , f^\sharp]\circ f\), which follows by uniqueness of \[f^\sharp= curry\;({((eval + id)\circ dstr \circ(f \times id))}^{\sharp_a})\] and
\item\textbf{Uniformity}: Let \(Y, Z \in\obj{C}, f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z\) and \((id + h)\circ f = g \circ h\). By uniqueness of \(f^\sharp= curry(((eval + id)\circ dstr \circ(f \times id))^{\sharp_a})\) it suffices to show:
\item\textbf{Uniformity}: Let \(f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z\) and \((id + h)\circ f = g \circ h\). Again, by uniqueness of \(f^\sharp= curry({((eval + id)\circ dstr \circ(f \times id))}^{\sharp_a})\) it suffices to show:
\\=\;&{((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))}^{\sharp_a}.\tag{\ref{law:uniformity}}
\end{alignat*}
Note that the second application of~\ref{law:uniformity} is non-trivial, using epicness of \(dstr^{-1}\):
\begin{alignat*}{1}
& (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ dstr^{-1}
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_1 \times id)
@ -354,7 +361,7 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
\end{proof}
\section{The Initial (Strong) Pre-Elgot Monad}
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial strong pre-Elgot monad.
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial strong pre-Elgot monad. Starting in this section we will now omit indices of the iteration operator of Elgot algebras for the sake of readability.
Let us first recall the following notion that was introduced in~\cite{elgotmonad} and reformulated in~\cite{uniformelgot}.
\begin{definition}[Elgot Monad]
@ -367,13 +374,13 @@ Let us first recall the following notion that was introduced in~\cite{elgotmonad
\\ for any \(f : X \rightarrow T(Y + X)\),
\item\textbf{Uniformity}: \(f \circ h = T(id + h)\) implies \(f^\dag\circ g = g^\dag\)
\\ for any \(f : X \rightarrow T(Y + X), g : Z \rightarrow T(Y + Z), h : Z \rightarrow X\),
\item\textbf{Naturality}: \(g^*\circ f^\dag={({[(Ti_1\circ g , \eta\circ i_2]}^*\circ f)}^\dag\)
\item\textbf{Naturality}: \(g^*\circ f^\dag={({[Ti_1\circ g , \eta\circ i_2]}^*\circ f)}^\dag\)
\\ for any \(f : X \rightarrow T(Y + X), g : Y \rightarrow TZ\),
If the monad \(\mathbf{T}\) is strong with strength \(\tau\) and \(\tau\circ(id \times f^\dag)={(Tdstl \circ\tau\circ(id \times f)}^\dag\) for any \(f : X \rightarrow T(Y+X)\), then \(\mathbf{T}\) is a strong Elgot monad.
If the monad \(\mathbf{T}\) is strong with strength \(\tau\) and \(\tau\circ(id \times f^\dag)={(Tdstl \circ\tau\circ(id \times f))}^\dag\) for any \(f : X \rightarrow T(Y+X)\), then \(\mathbf{T}\) is a strong Elgot monad.
\end{definition}
We regard Elgot monads as minimal semantic structures for interpreting side-effecting while loops, as has been argued in~\cite{goncharov2018unguarded, goncharov2017unifying}.
@ -382,7 +389,7 @@ The following notion has been introduced in~\cite{uniformelgot} as a weaker appr
\begin{definition}[Pre-Elgot Monad]
A monad \(\mathbf{T}\) is called pre-Elgot if every \(TX\) extends to an Elgot algebra such that for every \(f : X \rightarrow TY\) the Kleisli lifting \(f^* : TX \rightarrow TY\) is iteration preserving.
If \(\mathbf{T}\) is additionally strong and the strength \(\tau\) is right iteration preserving we call it strong pre-Elgot.
If the monad \(\mathbf{T}\) is additionally strong and the strength \(\tau\) is right iteration preserving we call \(\mathbf{T}\) strong pre-Elgot.
\end{definition}
(Strong) pre-Elgot monads form a subcategory of \(\monads{\C}\) where objects are (strong) pre-Elgot monads and morphisms between pre-Elgot monads are natural transformations \(\alpha\) as in \autoref{def:monadmorphism} such that additionally each \(\alpha_X\) is iteration preserving. Similarly, morphisms between strong pre-Elgot monads are natural transformations \(\alpha\) as in \autoref{def:strongmonadmorphism} such that each \(\alpha_X\) is iteration preserving. We call these categories \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) respectively.
@ -443,16 +450,16 @@ A symmetrical variant of the previous definition is sometimes useful.
\begin{lemma}
Definitions~\ref{def:rightstablefreeelgot} and~\ref{def:leftstablefreeelgot} are equivalent in the sense that they imply each other.
\end{lemma}
\begin{proof} Let \((KY, {(-)}^{\sharp_y})\) be a left stable free Elgot algebra on \(Y \in\obj{\C}\). Furthermore, let \(A\in\elgotalgs{\C}, X \in\obj{\C}, f : Y \times X \rightarrow A\).
\begin{proof} Let \(KY\) be a left stable free Elgot algebra on \(Y \in\obj{\C}\). Furthermore, let \(A\) be an Elgot algebra and \(X \in\obj{\C}, f : Y \times X \rightarrow A\).
We take \(\rs{f} :=\ls{f \circ swap}\circ swap\), which is indeed right iteration preserving, since
\begin{alignat*}{1}
&\rs{f}\circ (id \times h^{\sharp_y})
\\=\;&\ls{f \circ swap}\circ swap \circ (id \times h^{\sharp_y})
This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows symmetrically.
This concludes one direction of the proof, the other direction follows symmetrically.
\end{proof}
In a less general setting stability would indeed follow automatically.
\begin{theorem}\label{thm:stability}
\begin{lemma}\label{thm:stability}
In a Cartesian closed category every free Elgot algebra is stable.
\end{theorem}
\end{lemma}
\begin{proof}
Let \(\C\) be Cartesian closed and let \((KX, {(-)}^\sharp, \free{(-)})\) be a free Elgot algebra on some \(X \in\obj{\C}\).
Let \(\C\) be Cartesian closed and let \(KX\) be a free Elgot algebra on some \(X \in\obj{\C}\).
To show left stability of \(KX\) we define \(\ls{f} := eval \circ(\free{curry\;f}\times id)\) for any \(X \in\obj{\C}, A \in\vert\elgotalgs{\C}\vert\), and \(f : Y \times X \rightarrow A\).
To show left stability of \(KX\) we define \(\ls{f} := eval \circ(\free{curry\;f}\times id)\) for any \(X \in\obj{\C}\), \(A \in\vert\elgotalgs{\C}\vert\), and \(f : Y \times X \rightarrow A\).
We will now verify that this does indeed satisfy the requisite properties, i.e.
Lastly, we need to check uniqueness of \(\ls{f}\). Let us consider a left iteration preserving morphism \(g : KY \times X \rightarrow A\) that satisfies \(g \circ(\eta\times id)= f\). Since \(curry\) is an injective mapping it suffices to show that
@ -540,13 +547,13 @@ In a less general setting stability would indeed follow automatically.
for any \(Z \in\obj{\C}, h : Z \rightarrow KY + Z\), and
\begin{alignat*}{1}
@ -555,7 +562,7 @@ In a less general setting stability would indeed follow automatically.
\\=\;&curry\;f
\end{alignat*}
This completes the proof.
Which completes the proof.
\end{proof}
For the rest of this chapter we will assume every \(KX\) to exist and be stable. Under these assumptions we show that \(\mathbf{K}\) is an equational lifting monad and in fact the initial strong pre-Elgot monad.
@ -599,9 +606,9 @@ Of course there is also a symmetric version of this.
\(\mathbf{K}\) is a strong monad.
\end{lemma}
\begin{proof}
We define strength as \(\tau=\rs{(\eta : X \times Y \rightarrow K(X \times Y))} : X \times KY \rightarrow K(X \times Y)\). Note that \(\tau\) is right iteration preserving by definition and \(\tau\circ(id \times\eta)=\eta\).
We define strength as \(\tau=\rs{(\eta : X \times Y \rightarrow K(X \times Y))} : X \times KY \rightarrow K(X \times Y)\). Note that by definition \(\tau\) is right iteration preserving and \(\tau\circ(id \times\eta)=\eta\).
Most of the requisite proofs will be done by right-stability, i.e.\ to prove an identity we need to give a unifying morphism such that the requisite diagram commutes, and we need to show that both sides of the identity are right iteration preserving. The proofs of commutativity follow by easy rewriting and are thus deferred to the formalization. The proofs of right iteration preservation follow in most cases instantly since the morphisms are composed of (right) iteration preserving morphisms but in non-trivial cases we will give the full proof.
Most of the requisite proofs will be done by right-stability using \autoref{rem:proofbystability}, i.e.\ to prove an identity we need to give a unifying morphism such that the requisite diagram commutes, and we need to show that both sides of the identity are right iteration preserving. The proofs of commutativity follow by easy rewriting and are thus deferred to the formalization. The proofs of right iteration preservation follow in most cases instantly since the morphisms are composed of (right) iteration preserving morphisms but in non-trivial cases we will give the full proof.
@ -650,7 +657,7 @@ Of course there is also a symmetric version of this.
Let us now check the strength laws.
\begin{itemize}
\item[\ref{S1}] Note that for \(K\pi_2\circ\tau=\pi_2\) holds more generally for any \(X, Y \in\obj{\C}\), instead of just for \(X =1\):
\item[\ref{S1}] Note that for \(\mathbf{K}\), the identity \(K\pi_2\circ\tau=\pi_2\) holds more generally for any \(X, Y \in\obj{\C}\), instead of just for \(X =1\), proven by right-stability, using:
\\=\;&\tau\circ (id \times{((\tau + id) \circ dstl \circ (id \times h))}^\sharp) \circ\alpha
\\=\;&{((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))}^\sharp\circ\alpha
\\=\;&{(((\tau\circ (id \times\tau) \circ\alpha) + id) \circ dstl \circ (id \times h))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
\end{itemize}
Thus, strength of \(\mathbf{K}\) has been proven.
@ -720,8 +726,8 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
\begin{corollary}
\(\sigma\) is left iteration preserving and satisfies \(\sigma\circ(\eta\times id)=\eta\) and the following properties of \(\tau\) and \(\sigma\) hold.
Let us abbreviate \(\hat{f} :=(\eta+ id)\circ f\) and \(\hat{g} :=(\eta+ id)\circ g\). It suffices to find a \(w : ?\) such that \(\hat{f}^\sharp\circ\pi_1=[\hat{f}^\sharp\circ\pi_1 , \eta\circ\pi_1]^*\circ w^\sharp\) and \(\hat{g}^\sharp\circ\pi_2=[\hat{g}^\sharp\circ\pi_2 , \eta\circ\pi_2]^*\circ w^\sharp\), then
Let us abbreviate \(\hat{f} :=(\eta+ id)\circ f\) and \(\hat{g} :=(\eta+ id)\circ g\). It suffices to find a
\[w : X \times Z \rightarrow K(X \times KA + KY \times Z)+ X \times Z\]
such that \(\hat{f}^\sharp\circ\pi_1={[\hat{f}^\sharp\circ\pi_1 , \eta\circ\pi_1]}^*\circ w^\sharp\) and \(\hat{g}^\sharp\circ\pi_2={[\hat{g}^\sharp\circ\pi_2 , \eta\circ\pi_2]}^*\circ w^\sharp\), because then
Note that we are referencing \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity.
Note that we are referencing the equational lifting law established in \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, since we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity, this does not pose a problem.
where \(h =(\pi_1+((\pi_1+(\pi_1\times id))\circ dstl \circ\langle id , g \circ\pi_2\rangle))\circ dstr \circ(\hat{f}\times id)\) and the application of \ref{law:uniformity} is justified, since
where \(h =(\pi_1+(\pi_1+(\pi_1\times id))\circ dstl \circ\langle id , g \circ\pi_2\rangle)\circ dstr \circ(\hat{f}\times id)\) and the application of \ref{law:uniformity} is justified, since% chktex 2
\begin{alignat*}{1}
& (id + \pi_1) \circ (id + \Delta) \circ h
\\=\;&(\pi_1 + ((\pi_1 \circ [ \pi_1 , \pi_1 \times id ]) \circ dstl \circ\langle id , g \circ\pi_2 \rangle)) \circ dstr \circ (\hat{f}\times id)
@ -850,9 +858,9 @@ The following Lemma is central to the proof of commutativity.
This concludes the proof.
\end{proof}
\begin{theorem}
\begin{lemma}
\(\mathbf{K}\) is a commutative monad.
\end{theorem}
\end{lemma}
\begin{proof} We need to show that \(\tau^*\circ\sigma=\sigma^*\circ\tau : KX \times KY \rightarrow K(X \times Y)\).
Let us proceed by right stability, consider the following diagram.
Let \(\psi :=\tau^*\circ\sigma\) and let us proceed by left stability to show that \(\psi\) is right iteration preserving, consider the following diagram
We are left to show that both \(\psi\circ(id \times h^\sharp)\) and \(((\psi+ id)\circ dstl \circ(id \times h))^\sharp\) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi\circ(id \times h^\sharp)\) is left iteration preserving, since
We are left to show that both \(\psi\circ(id \times h^\sharp)\) and \({((\psi+ id)\circ dstl \circ(id \times h))}^\sharp\) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi\circ(id \times h^\sharp)\) is left iteration preserving, since
\begin{alignat*}{1}
&\psi\circ (id \times h^\sharp) \circ (g^\sharp\times id)
\\=\;&\psi\circ (g^\sharp\times id) \circ (id \times h^\sharp)
@ -958,7 +966,7 @@ The following Lemma is central to the proof of commutativity.
\begin{proof}
Since we have already shown commutativity, we are left to show that \(\tau\circ\Delta= K \langle\eta , id \rangle\). Note that \(K \langle\eta , id \rangle=\free{\eta\circ\langle\eta , id \rangle}\), which is the unique Elgot algebra morphism satisfying \(K \langle\eta , id \rangle\circ\eta=\eta\circ\langle\eta , id \rangle\). It thus suffices to show that \(\tau\circ\Delta\) satisfies the same identity and is iteration preserving.
The identity follows easily
The identity follows easily:
\begin{alignat*}{1}
&\tau\circ\Delta\circ\eta
\\=\;&\tau\circ\langle\eta , \eta\rangle
@ -971,8 +979,8 @@ The following Lemma is central to the proof of commutativity.
Note that by monicity of \(dstl^{-1}\) and by~\ref{law:fixpoint}
@ -994,11 +1002,11 @@ The following Lemma is central to the proof of commutativity.
Note that \(\mathbf{K}\) is a pre-Elgot monad by definition and strong pre-Elgot by \autoref{lem:Kstrong}. Let us first show that \(\mathbf{K}\) is the initial pre-Elgot monad.
Given any pre-Elgot monad \(\mathbf{T}\), let us introduce alternative names for the monad operations of \(\mathbf{T}\) and \(\mathbf{K}\) to avoid confusion:
For every \(X \in\obj{\C}\) we define \(¡ =\free{(\eta^T : X \rightarrow TX)} : KX \rightarrow TX \). Note that \(¡\) is the unique iteration preserving morphism that satisfies \(¡ \circ\eta^K =\eta^T\). We are done after showing that \(¡\) is natural and respects the monad multiplication.
For every \(X \in\obj{\C}\) we define \(¡ =\free{(\eta^T : X \rightarrow TX)} : KX \rightarrow TX \). Note that \(¡\) is per definition the unique iteration preserving morphism that satisfies \(¡ \circ\eta^K =\eta^T\). We are done after showing that \(¡\) is natural and respects the monad multiplication.
Let \(f : X \rightarrow Y\). For naturality of \(¡\) it suffices to show
@ -1008,7 +1016,7 @@ The following Lemma is central to the proof of commutativity.
& ¡ \circ Kf \circ\eta^K
\\=\;&¡ \circ\eta^K \circ f
\\=\;&\eta^T \circ f
\\=\;&Tf \circ\eta^T
\\=\;&Tf \circ\eta^T.
\end{alignat*}
Let us proceed similarly for showing that \(¡\) respects the monad multiplication, i.e.\ consider
@ -1022,7 +1030,7 @@ The following Lemma is central to the proof of commutativity.
\\=\;&¡.
\end{alignat*}
Thus, \(\mathbf{K}\) is an initial pre-Elgot monad. To show that \(\mathbf{K}\) is also initial strong pre-Elgot, assume that \(\mathbf{T}\) is strong with strength \(\tau^T\) and let us call the strength of \(\mathbf{K}\)\(\tau^K\). We are left to show that \(¡\) respects strength, i.e.\ \( ¡ \circ\tau^K =\tau^T \circ(id \times ¡) : X \times KY \rightarrow T(X \times Y)\). Note that
Thus, \(\mathbf{K}\) is an initial pre-Elgot monad. To show that \(\mathbf{K}\) is also initial strong pre-Elgot, assume that \(\mathbf{T}\) is strong with strength \(\tau^T\) and let us call the strength of \(\mathbf{K}\)\(\tau^K\). We are left to show that \(¡\) respects strength, i.e.\ \( ¡ \circ\tau^K =\tau^T \circ(id \times ¡) : X \times KY \rightarrow T(X \times Y)\). We proceed by right-stability, using:
commutes, since \( ¡ \circ\tau^K =\eta^T =\tau^T \circ(id \times\eta^T)=\tau^T \circ(id \times ¡)\circ(id \times\eta^T)\). Using \autoref{rem:proofbystability} we are done, since \(¡ \circ\tau^K\) and \(\tau^T \circ(id \times ¡)\) are both right iteration preserving for the reason that both are composed of (right) iteration preserving morphisms.
The diagram commutes, since \( ¡ \circ\tau^K =\eta^T =\tau^T \circ(id \times\eta^T)=\tau^T \circ(id \times ¡)\circ(id \times\eta^T)\). Now we are done, since \(¡ \circ\tau^K\) and \(\tau^T \circ(id \times ¡)\) are both right iteration preserving because both are composed of (right) iteration preserving morphisms.
@ -12,11 +12,11 @@ We will now introduce the category that the rest of the chapter will take place
For brevity, we will not use the tuple notation most of the time, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
\begin{definition}[Setoid Function]
A function on setoids \(A\) and \(B\) is a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid functions as \(A \leadsto B\).
A function on setoids \(A\) and \(B\) is a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid functions as \(A ⇝ B\).
\end{definition}
Let us now consider the function space setoid, which is of special interest, since it defines a notion of equality between functions.
\begin{definition}[Function Space Setoid]
Given two setoids \(A\) and \(B\). The function space setoid on these setoids is defined as \((A \leadsto B, \doteq)\) or just \(A \leadsto B\), where \(\doteq\) is point wise equality on setoid functions.
Given two setoids \(A\) and \(B\). The function space setoid on these setoids is defined as \((A ⇝ B, \doteq)\) or just \(A ⇝ B\), where \(\doteq\) is point wise equality on setoid functions.
\end{definition}
Setoids together with setoid functions form a category that we will call \(\setoids\). Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
@ -94,7 +94,7 @@ Setoids together with setoid functions form a category that we will call \(\seto
\(\setoids\) is Cartesian closed.
\end{proposition}
\begin{proof}
Let \(A\) and \(B\) be two setoids. The function space setoid \(A \leadsto B\) is an exponential object of \(A\) and \(B\), together with the functions \(curry\) and \(eval\) defined in the following listing.
Let \(A\) and \(B\) be two setoids. The function space setoid \(A ⇝ B\) is an exponential object of \(A\) and \(B\), together with the functions \(curry\) and \(eval\) defined in the following listing.
\begin{minted}{agda}
curry : ∀ {a b c}{A : Set a}{B : Set b}{C : Set c}
→ (C × A → B) → C → A → B
@ -168,7 +168,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
\begin{proof}
We need to show that for every setoid \(A\) the resulting setoid \(\dbtilde{D}\;A\) can be extended to an Elgot algebra.
Let \(X\) be a setoid and \(f : X \leadsto\dbtilde{D}\;A + X\) be a setoid function, we define \(f^\sharp : X \leadsto\dbtilde{D}\;A\) point wise:
Let \(X\) be a setoid and \(f : X ⇝\dbtilde{D}\;A + X\) be a setoid function, we define \(f^\sharp : X ⇝\dbtilde{D}\;A\) point wise:
\[
f^\sharp\;x :=
\begin{cases}
@ -189,7 +189,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
\case{}\(f\;x = i_2\;a\)
\[ f^\sharp\;x \approx later (f^{\sharp}\;a)\approx f^\sharp\;a \approx[ id , f^\sharp](i_2\;a)\approx[ id , f^\sharp](f\;x)\]
\end{mycase}
\item\ref{law:uniformity}: Let \(Y\) be a setoid and \(g : Y \leadsto\dbtilde{D}\;A + Y, h : X \leadsto Y\) be setoid functions, such that \((id + h)\circ f \doteq g \circ h\). We need to show that \(f^\sharp\;x \approx g^\sharp(h\;x)\), for any \(x : X\). Let us proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h)\circ f \doteq g \circ h\), we only need to consider two cases: % chktex 2
\item\ref{law:uniformity}: Let \(Y\) be a setoid and \(g : Y ⇝ \dbtilde{D}\;A + Y, h : X ⇝ Y\) be setoid functions, such that \((id + h)\circ f \doteq g \circ h\). We need to show that \(f^\sharp\;x \approx g^\sharp(h\;x)\), for any \(x : X\). Let us proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h)\circ f \doteq g \circ h\), we only need to consider two cases: % chktex 2
\begin{mycase}
\case{}\(f\;x = i_1\;a\) and \(g (h\;x)= i_1\;b\)\\
Consider that \((id + h)\circ f \doteq g \circ h\) on \(x\) yields \(i_1\; a \overset{+}{=} i_1\; b\) and thus \(a \approx b\). Then indeed,
@ -199,7 +199,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
\item\ref{law:folding}: Let \(Y\) be a setoid and \(h : Y \leadsto X + Y\) a setoid function, we need to show that \({(f^\sharp+ h)}^\sharp\;z \approx{[(id + i_1)\circ f , i_2\circ h ]}^\sharp\;z\) for any \(z : X + Y\). % chktex 2
\item\ref{law:folding}: Let \(Y\) be a setoid and \(h : Y ⇝ X + Y\) a setoid function, we need to show that \({(f^\sharp+ h)}^\sharp\;z \approx{[(id + i_1)\circ f , i_2\circ h ]}^\sharp\;z\) for any \(z : X + Y\). % chktex 2
Let us first establish the following fact
\[f^\sharp\;c \approx{[(id + i_1)\circ f , i_2\circ h ]}^\sharp(i_1\;c)\qquad\text{for any } c : X, \tag{*}\label{folding-helper}\]
which follows by case distinction on \(f\;c\) and coinduction:
@ -249,7 +249,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a setoid \(Z\), we can discretize \(Z\) by replacing the equivalence relation with propositional equality, yielding \(\disc{Z} :=(Z, \equiv)\). Now, the following corollary describes how to transform an iteration on \(\dbtilde{D}\;A\) into an iteration on \(\tilde{D}\;A\).
\begin{corollary}\label{cor:discretize}
Given a setoid function \(g : X \leadsto\dbtilde{D}\;A + X\). There exists a setoid function \(\bar{g} : \disc{X}\leadsto\tilde{D}\;A +\disc{X}\) such that \(g^\sharp\;x \sim\bar{g}^{\tilde{\sharp}}\;x\) for any \(x : X\).
Given a setoid function \(g : X ⇝\dbtilde{D}\;A + X\). There exists a setoid function \(\bar{g} : \disc{X}⇝\tilde{D}\;A +\disc{X}\) such that \(g^\sharp\;x \sim\bar{g}^{\tilde{\sharp}}\;x\) for any \(x : X\).
\end{corollary}
\begin{proof}
It is clear that propositional equality implies strong bisimilarity and thus \(\bar{g}\) is a setoid function that behaves as \(g\) does but with a different type profile.
@ -267,20 +267,20 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
Every \(\dbtilde{D}\;A\) can be equipped with a free Elgot algebra structure.
\end{theorem}
\begin{proof}
We build on \autoref{lem:Delgot}, it thus suffices to show that for any setoid \(A\), the Elgot algebra \((\dbtilde{D}\;A, {(-)}^\sharp)\) together with the setoid function \(now : A \leadsto\dbtilde{D}\;A\) is a free such algebra.
Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid function \(f : A \leadsto B\). We need to define an Elgot algebra function \(\free{f} : \dbtilde{D}\;A \leadsto B\). Consider \(g : \tilde{D}\;A \leadsto B +\tilde{D}\;A\) defined by
We build on \autoref{lem:Delgot}, it thus suffices to show that for any setoid \(A\), the Elgot algebra \((\dbtilde{D}\;A, {(-)}^\sharp)\) together with the setoid function \(now : A ⇝\dbtilde{D}\;A\) is a free such algebra.
Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid function \(f : A ⇝ B\). We need to define an Elgot algebra function \(\free{f} : \dbtilde{D}\;A ⇝ B\). Consider \(g : \tilde{D}\;A ⇝ B +\tilde{D}\;A\) defined by
\[g\;x =
\begin{cases}
i_1(f\;a) &\text{if } x = now\;a \\
i_2\;a &\text{if } x = later\;a
\end{cases}\]
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f}= g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}.
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A ⇝ B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f}= g^{\sharp_b} : \dbtilde{D}\;A ⇝ B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}.
Instead, we will continue with the proof. Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid function \(h : X \leadsto\dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b}(h^\sharp\;x)\overset{B}{=}{((g^{\sharp_b}+ id)\circ h)}^{\sharp_b}\;x\) for any \(x : X\). Using \autoref{cor:discretize} we will proceed to show
Instead, we will continue with the proof. Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid function \(h : X ⇝\dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b}(h^\sharp\;x)\overset{B}{=}{((g^{\sharp_b}+ id)\circ h)}^{\sharp_b}\;x\) for any \(x : X\). Using \autoref{cor:discretize} we will proceed to show
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid function \(id : \disc{X}\leadsto X\), and thus the second step can be reduced to \({((g^{\sharp_b}+ id)\circ\bar{h})}^{\sharp_b}\;x \overset{B}{=}{((g^{\sharp_b}+ id)\circ h)}^{\sharp_b}(id\;x)\). % chktex 2
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid function \(id : \disc{X}⇝ X\), and thus the second step can be reduced to \({((g^{\sharp_b}+ id)\circ\bar{h})}^{\sharp_b}\;x \overset{B}{=}{((g^{\sharp_b}+ id)\circ h)}^{\sharp_b}(id\;x)\). % chktex 2
For the first step consider
\begin{alignat*}{1}
& g^{\sharp_b} (h^\sharp\;x)
@ -291,15 +291,15 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
\end{alignat*}
Thus, \(g^{\sharp_b}\) is an Elgot algebra function. We are left to check that \(g^{\sharp_b}\) satisfies the requisite properties of free objects. First, note that \(g^{\sharp_b}\circ now \doteq[ id , g^\sharp_b ]\circ g \circ now \doteq f\) by \ref{law:fixpoint} and the definition of \(g\). % chktex 2
Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra functions \(e, h : \dbtilde{D}\;A \leadsto B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra functions \(e, h : \dbtilde{D}\;A ⇝ B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
First, note that the identity function can be extended to the following conversion setoid function \(conv : \tilde{D}\;A \leadsto\dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid function \(o : \tilde{D}\;A \leadsto\tilde{D}\;A +\tilde{D}\;A\) defined by
First, note that the identity function can be extended to the following conversion setoid function \(conv : \tilde{D}\;A ⇝\dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid function \(o : \tilde{D}\;A ⇝\tilde{D}\;A +\tilde{D}\;A\) defined by
\[o\;x :=\begin{cases}
i_1(now\;z) &\text{if } x = now\;z \\
i_2\;z &\text{if } x = later\;z
\end{cases}\]
Now, by coinduction we can easily follow that
\[x \approx{((conv + id)\circ o)}^\sharp\;x \qquad\text{for any } x : D\;A.\tag{\(\Asterisk\)}\label{uniq-helper}\]
\[x \approx{((conv + id)\circ o)}^\sharp\;x \qquad\text{for any } x : D\;A.\tag{\(∗\)}\label{uniq-helper}\]
Let us now return to the proof of uniqueness. We proceed by
\begin{alignat*}{1}
@ -380,7 +380,7 @@ Lastly, consider the function \(\iota : A \times \mathbb{N} \rightarrow D\;A\),
later(\iota\;(a, m)) &\text{if } n = m + 1
\end{cases}\]
Trivially, \(\iota\) can be extended to a setoid function \(\iota : A \times\mathbb{N}\leadsto\tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality.
Trivially, \(\iota\) can be extended to a setoid function \(\iota : A \times\mathbb{N}⇝\tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality.
Let us state two facts about \(\Delta\), the proofs can again be found in the formalization.
\begin{corollary}\label{cor:delta}
\(\Delta\) satisfies the following properties:
@ -393,7 +393,7 @@ Let us state two facts about \(\Delta\), the proofs can again be found in the fo
Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
\begin{corollary}\label{cor:respects}
The setoid function \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\) defined in \autoref{thm:Dfreeelgot} respects weak bisimilarity, thus yielding \(\free{f}= g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\).
The setoid function \(g^{\sharp_b} : \tilde{D}\;A ⇝ B\) defined in \autoref{thm:Dfreeelgot} respects weak bisimilarity, thus yielding \(\free{f}= g^{\sharp_b} : \dbtilde{D}\;A ⇝ B\).
\end{corollary}
\begin{proof}
Let \(x, y : D\;A\) such that \(x \approx y\). Recall that by \autoref{cor:race}\(x \approx y\) implies \(p: race\;x\;y \lesssim y\) and symmetrically \(q: race\;y\;x \lesssim x\), now, using Corollaries~\ref{cor:race} and~\ref{cor:delta}:
@ -419,7 +419,7 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
Which leaves us to find suitable \(g_1, g_2 : \tilde{D}(A \times\mathbb{N})\leadsto B +\tilde{D}(A \times\mathbb{N})\). Consider,
Which leaves us to find suitable \(g_1, g_2 : \tilde{D}(A \times\mathbb{N})⇝ B +\tilde{D}(A \times\mathbb{N})\). Consider,
\[g_1\;p :=\begin{cases}
i_1(f\;x) &\text{if } p = now\;(x, zero) \\
i_2(\tilde{D}o (\iota\;(x,n))) &\text{if } p = now\;(x, n + 1) \\
@ -430,11 +430,11 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
i_1(f\;x) &\text{if } p = now\;(x , n) \\
i_2\;q &\text{if } p = later\;q
\end{cases}\]
where \(o : A \leadsto A \times\mathbb{N}\) is a setoid function that maps every \(z : A\) to \((z , 0) : A \times\mathbb{N}\). The applications of \ref{law:uniformity} are then justified by the definitions of \(g_1\) and \(g_2\) as well as the fact that \(\iota\circ o \doteq now\). % chktex 2
where \(o : A ⇝ A \times\mathbb{N}\) is a setoid function that maps every \(z : A\) to \((z , 0) : A \times\mathbb{N}\). The applications of \ref{law:uniformity} are then justified by the definitions of \(g_1\) and \(g_2\) as well as the fact that \(\iota\circ o \doteq now\). % chktex 2
We are thus done after showing that \(g_1^{\sharp_b}\;z \overset{B}{=} g_2^{\sharp_b}\;z\).
Consider another setoid function
\[g_3 : \tilde{D}(A \times\mathbb{N})\leadsto B +\tilde{D}(A \times\mathbb{N})+\tilde{D}(A \times\mathbb{N}),\]
\[g_3 : \tilde{D}(A \times\mathbb{N})⇝ B +\tilde{D}(A \times\mathbb{N})+\tilde{D}(A \times\mathbb{N}),\]
defined by
\[g_3\;p :=\begin{cases}
i_1(f\;x) &\text{if } p = now\;(x, 0) \\
@ -474,7 +474,7 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
\end{alignat*}
Where
\[{((id +[ id , id])\circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,n)))\overset{B}{=} f\;y \tag{\(\Asterisk\)}\label{finalhelper}\]
\[{((id +[ id , id])\circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,n)))\overset{B}{=} f\;y \tag{\(∗\)}\label{finalhelper}\]
