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

Work on proofs

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-25 21:40:23 +01:00
parent 5f479bf4f8
commit da4223e011
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
5 changed files with 321 additions and 194 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt vendored
View file

@ -7,3 +7,12 @@
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QWe call a morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q guarded if there exists an \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagram commutes: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QIt suffices to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, because then follows: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We prove this by coinduction using: [inline]Change name of morphism &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q[inline]Make this more explicit The first step in both equations can be proven by monicity of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and then using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the dual diagram for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the last step holds generally for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QFirst we need to show naturality of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, i.e. we need to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q The needed coalgebra is shown in this diagram: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Next we check the strength laws: [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] To show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q we do coinduction using the following coalgebra: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] We don't need coinduction to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but we need a small helper lemma: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QFirst we need to show naturality of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, i.e. we need to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q The coalgebra for coinduction is: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We write \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to abbreviate the rather long coalgebra, i.e. in this diagram \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q&&&&&&& &&&&&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then follows from this diagram.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QSince \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a final coalgebra we get the following proof principle: Given two morphisms \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q it suffices to show that there exists a coalgebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagrams commute: &&&&&& &&&&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Uniqueness of the coalgebra morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then gives us that indeed \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QFirst we need to show naturality of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, i.e. we need to show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q The coalgebra for coinduction is: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We write \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to abbreviate the used coalgebra, i.e. in this diagram \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QNext we check the strength laws: [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] To show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q we do coinduction using the following coalgebra: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q [\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q] We don't need coinduction to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, but we need a small helper lemma: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QIt suffices to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, because then follows: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We prove this by coinduction using: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q[inline]Move this remark to the beginning of proof The first step in both equations can be proven by monicity of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and then using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the dual diagram for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QTo show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q it suffices to show that there exists a coalgebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagrams commute: &&&&&& &&&&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Uniqueness of the coalgebra morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then results in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}

7
thesis/main.pyg Normal file
View file

@ -0,0 +1,7 @@
mutual
data Delay (A : Set) : Set where
now : A → Delay A
later : Delay′ A → Delay A
record Delay′ (A : Set) : Set where
coinductive
field force : Delay A

2
thesis/src/01_preliminaries.tex
View file

@ -381,7 +381,7 @@ For programmers a second equivalent definition is more useful:
A Kleisli triple on a category $\C$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the Kleisli lifting, where the following laws hold:
\begin{alignat*}{2}
&\eta_X^* &&= id_{FX} \tag*{(K1)}\label{K1}\\
&\eta_X \circ f^* &&= f \tag*{(K2)}\label{K2}\\
&f^* \circ \eta_X &&= f \tag*{(K2)}\label{K2}\\
&f^* \circ g* &&= (f \circ g^*)^* \tag*{(K3)}\label{K3}
\end{alignat*}
\end{definition}

496
thesis/src/03_partiality-monads.tex
View file

@ -22,10 +22,10 @@ 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:
\begin{alignat*}{1}
f \circ (\tdom f) &= f\tag*{(R1)}\label{R1}\\
(\tdom f) \circ (\tdom g) &= (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2}\\
\tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3}\\
(\tdom h) \circ f &= f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4}
f \circ (\tdom f) & = f\tag*{(R1)}\label{R1} \\
(\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2} \\
\tdom(g \circ (\tdom f)) & = (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3} \\
(\tdom h) \circ f & = f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4}
\end{alignat*}
for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
\end{definition}
@ -42,10 +42,10 @@ To ensure that programs are partial, we recall the following notion by Cockett a
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:
\[
(\tdom f)(x) = \begin{cases}
x & \text{if } f(x) \text{ is defined}\\
\text{undefined} & \text{else}
\end{cases}
(\tdom f)(x) = \begin{cases}
x & \text{if } f(x) \text{ is defined} \\
\text{undefined} & \text{else}
\end{cases}
\]
That is, $\tdom f$ is only defined on values where $f$ is defined and for those values it behaves like the identity function.
@ -64,13 +64,13 @@ Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which ca
A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ==
\[\begin{tikzcd}
TX && {TX \times TX} \\
\\
&& {T(TX \times X)}
\arrow["\Delta", from=1-1, to=1-3]
\arrow["\tau", from=1-3, to=3-3]
\arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
\end{tikzcd}\]
TX && {TX \times TX} \\
\\
&& {T(TX \times X)}
\arrow["\Delta", from=1-1, to=1-3]
\arrow["\tau", from=1-3, to=3-3]
\arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
\end{tikzcd}\]
where $\Delta : X \rightarrow X \times X$ is the diagonal morphism.
\end{definition}
@ -92,27 +92,27 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
Naturality of $\tau$ follows by naturality of $dstl$:
\begin{alignat*}{1}
&(id + !) \circ dstl \circ (id \times (f + id))\\
= \;&(id + !) \circ ((id \times f) + (id \times id)) \circ dstl\\
= \;&((id \times f) + !) \circ dstl\\
= \;&((id \times f) + id) \circ (id + !) \circ dstl
& (id + !) \circ dstl \circ (id \times (f + id)) \\
= \; & (id + !) \circ ((id \times f) + (id \times id)) \circ dstl \\
= \; & ((id \times f) + !) \circ dstl \\
= \; & ((id \times f) + id) \circ (id + !) \circ dstl
\end{alignat*}
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.
We are left to check the equational lifting law:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ==
\[\begin{tikzcd}
{X+1} &&& {(X+1)\times(X+1)} \\
\\
&&& {((X+1)\times X) +((X+1)\times 1)} \\
\\
&&& {((X+1)\times X)+1}
\arrow["\Delta", from=1-1, to=1-4]
\arrow["dstl", from=1-4, to=3-4]
\arrow["{id+\;!}", from=3-4, to=5-4]
\arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4]
\end{tikzcd}\]
{X+1} &&& {(X+1)\times(X+1)} \\
\\
&&& {((X+1)\times X) +((X+1)\times 1)} \\
\\
&&& {((X+1)\times X)+1}
\arrow["\Delta", from=1-1, to=1-4]
\arrow["dstl", from=1-4, to=3-4]
\arrow["{id+\;!}", from=3-4, to=5-4]
\arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4]
\end{tikzcd}\]
By pre-composing with $i_1$ and $i_2$ it suffices to show that
\[i_1 \circ \langle i_1 , id \rangle = (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle\]
and
@ -128,14 +128,14 @@ In the setting of classical mathematics this monad is therefore sufficient for m
\section{The Delay Monad}
\todo[inline]{Take introduction from setoids chapter and put it here!}
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
This monad is usually defined by the two coinductive constructors $now$ and $later$, where $now$ is for lifting a value to a computation and $later$ intuitively delays a computation by one time unit:
\todo[inline]{Explain convention of double lines vs single lines ==> remove double lines here!!}
\[\mprset{fraction={===}}
\inferrule {x : X} {now\; x : DX}\hskip 2cm
\inferrule {c : DX} {later\; c : DX}\]
\inferrule {x : X} {now\; x : DX}\hskip 2cm
\inferrule {c : DX} {later\; c : DX}\]
Categorically we obtain this monad by the final coalgebras $DX = \nu A. X + A$, which we assume to exist. In this section we will show that $\mathbf{D}$ is a strong and commutative monad.
@ -145,60 +145,61 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
\label{col:delay}
The following conditions hold:
\begin{itemize}
\item There exists a unit morphism $now : X \rightarrow DX$ for any DX, satisfying
\begin{equation*}
out \circ now = i_1 \tag*{(D1)}\label{D1}
\end{equation*}
\item There exists a unit morphism $now : X \rightarrow DX$ for any DX, satisfying
\begin{equation*}
out \circ now = i_1 \tag*{(D1)}\label{D1}
\end{equation*}
\item For any $f : X \rightarrow DY$ there exists a unique morphism $f^* : DX \rightarrow DY$ satisfying:
\begin{equation*}
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIlggKyBEWCJdLFswLDEsIkRZIl0sWzMsMSwiWSArIERZIl0sWzAsMSwib3V0Il0sWzAsMiwiZl4qIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywib3V0Il0sWzEsMywiWyBvdXQgXFxjaXJjIGYgLCBpXzIgXFxjaXJjIGZeKiBdIl1d
\begin{tikzcd}
DX &&& {X + DX} \\
DY &&& {Y + DY}
\arrow["out", from=1-1, to=1-4]
\arrow["{f^*}", dashed, from=1-1, to=2-1]
\arrow["out", from=2-1, to=2-4]
\arrow["{[ out \circ f , i_2 \circ f^* ]}", from=1-4, to=2-4]
\end{tikzcd}\tag*{(D2)}\label{D2}
\end{equation*}
\begin{equation*}
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIlggKyBEWCJdLFswLDEsIkRZIl0sWzMsMSwiWSArIERZIl0sWzAsMSwib3V0Il0sWzAsMiwiZl4qIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywib3V0Il0sWzEsMywiWyBvdXQgXFxjaXJjIGYgLCBpXzIgXFxjaXJjIGZeKiBdIl1d
\begin{tikzcd}
DX &&& {X + DX} \\
DY &&& {Y + DY}
\arrow["out", from=1-1, to=1-4]
\arrow["{f^*}", dashed, from=1-1, to=2-1]
\arrow["out", from=2-1, to=2-4]
\arrow["{[ out \circ f , i_2 \circ f^* ]}", from=1-4, to=2-4]
\end{tikzcd}\tag*{(D2)}\label{D2}
\end{equation*}
\item There exists a unique morphism $\tau : X \times DY \rightarrow D(X \times Y)$ satisfying:
\begin{equation*}
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
\begin{tikzcd}[ampersand replacement=\&]
{X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
{D(X \times Y)} \&\&\&\& {X \times Y + D(X \times Y)}
\arrow["\tau", dashed, from=1-1, to=2-1]
\arrow["{id \times out}", from=1-1, to=1-3]
\arrow["dstl", from=1-3, to=1-5]
\arrow["{id +\tau}"', from=1-5, to=2-5]
\arrow["out", from=2-1, to=2-5]
\end{tikzcd}\tag*{(D3)}\label{D3}
\end{equation*}
\begin{equation*}
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
\begin{tikzcd}[ampersand replacement=\&]
{X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
{D(X \times Y)} \&\&\&\& {X \times Y + D(X \times Y)}
\arrow["\tau", dashed, from=1-1, to=2-1]
\arrow["{id \times out}", from=1-1, to=1-3]
\arrow["dstl", from=1-3, to=1-5]
\arrow["{id +\tau}"', from=1-5, to=2-5]
\arrow["out", from=2-1, to=2-5]
\end{tikzcd}\tag*{(D3)}\label{D3}
\end{equation*}
\end{itemize}
\end{proposition}
\begin{proof}
We will make use of the fact that every $DX$ is a final coalgebra:
\begin{itemize}
\begin{itemize}
\item[\ref{D1}] This follows by definition of $now$.
\item[\ref{D2}] We define $f^* = \;! \circ i_1$, where $!$ is the unique coalgebra morphism in this diagram:
\todo[inline]{Use other name than '!' for unique morphism => semantic brackets!}
\item[\ref{D2}] We define $f^* = \;\coalg{\alpha} \circ i_1$, where $\coalg{\alpha}$ is the unique coalgebra morphism in this diagram:
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBpXzEgLCBpXzIgXFxjaXJjIGlfMiBdIFxcY2lyYyAob3V0IFxcY2lyYyBmKSAsIGlfMiBcXGNpcmMgaV8xIF0gXFxjaXJjIG91dCAsIChpZCArIGlfMikgXFxjaXJjIG91dCBdIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsImlkICsgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
\[\begin{tikzcd}
DX \\
{DX + DY} &&&&&&& {Y + (DX + DY)} \\
DY &&&&&&& {Y + DY}
\arrow["{[ [ [ i_1 , i_2 \circ i_2 ] \circ (out \circ f) , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]}", from=2-1, to=2-8]
\arrow["{i_1}", from=1-1, to=2-1]
\arrow["{!}", dashed, from=2-1, to=3-1]
\arrow["out", from=3-1, to=3-8]
\arrow["{id + !}", dashed, from=2-8, to=3-8]
\end{tikzcd}\]
$out \circ f^* = [ out \circ f , i_2 \circ f^* ] \circ out$ then follows from this diagram.
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIDo9IFsgWyBbIGlfMSAsIGlfMiBcXGNpcmMgaV8yIF0gXFxjaXJjIChvdXQgXFxjaXJjIGYpICwgaV8yIFxcY2lyYyBpXzEgXSBcXGNpcmMgb3V0ICwgKGlkICsgaV8yKSBcXGNpcmMgb3V0IF0iXSxbMiwwLCJpXzEiXSxbMCwzLCJcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzMsNCwib3V0Il0sWzEsNCwiaWQgKyBcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
DX \\
{DX + DY} \&\&\&\&\&\&\& {Y + (DX + DY)} \\
DY \&\&\&\&\&\&\& {Y + DY}
\arrow["{\alpha := [ [ [ i_1 , i_2 \circ i_2 ] \circ (out \circ f) , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]}", from=2-1, to=2-8]
\arrow["{i_1}", from=1-1, to=2-1]
\arrow["{\coalg{\alpha}}", dashed, from=2-1, to=3-1]
\arrow["out", from=3-1, to=3-8]
\arrow["{id + \coalg{\alpha}}", dashed, from=2-8, to=3-8]
\end{tikzcd}\]
$out \circ f^* = [ out \circ f , i_2 \circ f^* ] \circ out$ then follows from this diagram.
We are left to check uniqueness. Let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$.
Then $[ g , id ] : DX + DY \rightarrow DY$\improvement{details of why it is coalgebra morphism} is a coalgebra morphism and thus $[ g , id ] =\;!$ by uniqueness of $!$.
It follows: \[g = [ g , id ] \circ i_1 =\;! \circ i_1 = f^*\]
\improvement{Details of why it is coalgebra morphism}
We are left to check uniqueness. Let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$.
Then $[ g , id ] : DX + DY \rightarrow DY$ is a coalgebra morphism and 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)$.
\end{itemize}
\end{proof}
@ -210,34 +211,43 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
We will now use the properties proven in Corollary~\ref{col: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}.
\item[\ref{K2}] Let $f : X \rightarrow DY$. We use the fact that $out$ is monic and the following equation:
\[out \circ f^* \circ now \overset{\ref{D2}}{=} [ out \circ f , i_2 \circ f^* ] \circ out \circ now \overset{\ref{D1}}{=} out \circ f \]
\item[\ref{K3}] Using uniqueness of $(h^* \circ g)^*$ we need to show $out \circ h^* \circ g^* = [ out \circ h^* \circ g , i_2 \circ h^* \circ g^* ] \circ out$ which follows by multiple uses of \ref{D2}.
\todo[inline]{More details probably for both K2 and K3}
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}.
\item[\ref{K2}] Let $f : X \rightarrow DY$. We proceed by monicity of $out$:
\begin{alignat*}{1}
&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
\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}
&out \circ f^* \circ g^*
\\=\;&[ 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}}
\end{alignat*}
\end{itemize}
\end{proof}
Since $(DX, out)$ is a final coalgebra we get the following proof principle:
Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ yields the following proof principle:
\begin{remark}[Proof by coinduction]
\label{rem:coinduction}
Given two morphisms $f, g : X \rightarrow DY$, to show that $f = g$ it suffices to show that there exists a coalgebra structure $\alpha : X \rightarrow Y + X$ such that the following diagrams commute:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCIsMl1d
\[\begin{tikzcd}
X && {Y + X} && X && {Y + X} \\
DY && {Y + DY} && DY && {Y + DY}
\arrow["out", from=2-1, to=2-3]
\arrow["\alpha", from=1-1, to=1-3]
\arrow["f", from=1-1, to=2-1]
\arrow["{id + f}", from=1-3, to=2-3]
\arrow["\alpha", from=1-5, to=1-7]
\arrow["g", from=1-5, to=2-5]
\arrow["{id + g}", from=1-7, to=2-7]
\arrow["out"', from=2-5, to=2-7]
\end{tikzcd}\]
Uniqueness of the coalgebra morphism $! : (X, \alpha) \rightarrow (DY, out)$ then gives us that indeed $f = g$.
Given two morphisms $f, g : X \rightarrow DY$. To show that $f = g$ it suffices to show that there exists a coalgebra structure $\alpha : X \rightarrow Y + X$ such that the following diagrams commute:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
X \&\& {Y + X} \&\& X \&\& {Y + X} \\
DY \&\& {Y + DY} \&\& DY \&\& {Y + DY}
\arrow["out", from=2-1, to=2-3]
\arrow["\alpha", from=1-1, to=1-3]
\arrow["f", from=1-1, to=2-1]
\arrow["{id + f}", from=1-3, to=2-3]
\arrow["\alpha", from=1-5, to=1-7]
\arrow["g", from=1-5, to=2-5]
\arrow["{id + g}", from=1-7, to=2-7]
\arrow["out", from=2-5, to=2-7]
\end{tikzcd}\]
Uniqueness of the coalgebra morphism $\coalg{\alpha} : (X, \alpha) \rightarrow (DY, out)$ then results in $f = g$.
\end{remark}
\begin{theorem}
@ -246,113 +256,167 @@ Since $(DX, out)$ is a final coalgebra we get the following proof principle:
\begin{proof}
Most of the following proofs are done via coinduction (Remark~\ref{rem:coinduction}). We will only give the requisite coalgebra structure. The proofs that the diagrams commute can be looked up in the Agda formalization.
First we need to show naturality of $\tau$, i.e. we need to show that
First we need to show naturality of $\tau$, i.e. we need to show that
\[\tau \circ (f \times (now \circ g)^*) = (now \circ (f \times g))^* \circ \tau\]
The needed coalgebra is shown in this diagram:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwyLCJEKEFcXHRpbWVzIEIpIl0sWzQsMiwiQVxcdGltZXMgQiArIEQoQSBcXHRpbWVzIEIpIl0sWzEsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzIsMCwiWCBcXHRpbWVzIFkgKyBYIFxcdGltZXMgRFkiXSxbNCwwLCJBIFxcdGltZXMgQiArIFggXFx0aW1lcyBEWSJdLFsxLDIsIm91dCJdLFswLDMsImlkIFxcdGltZXMgb3V0Il0sWzMsNCwiZHN0bCJdLFswLDEsIiEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNCw1LCJmIFxcdGltZXMgZyArIGlkIl0sWzUsMiwiaWQgKyAhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}
{X \times DY} & {X \times (Y + DY)} & {X \times Y + X \times DY} && {A \times B + X \times DY} \\
\\
{D(A\times B)} &&&& {A\times B + D(A \times B)}
\arrow["out", from=3-1, to=3-5]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["{!}", dashed, from=1-1, to=3-1]
\arrow["{f \times g + id}", from=1-3, to=1-5]
\arrow["{id + !}", dashed, from=1-5, to=3-5]
\end{tikzcd}\]
The coalgebra for coinduction is:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwyLCJEKEFcXHRpbWVzIEIpIl0sWzQsMiwiQVxcdGltZXMgQiArIEQoQSBcXHRpbWVzIEIpIl0sWzEsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzIsMCwiWCBcXHRpbWVzIFkgKyBYIFxcdGltZXMgRFkiXSxbNCwwLCJBIFxcdGltZXMgQiArIFggXFx0aW1lcyBEWSJdLFsxLDIsIm91dCJdLFswLDMsImlkIFxcdGltZXMgb3V0Il0sWzMsNCwiZHN0bCJdLFswLDEsIlxcY29hbGd7LX0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNCw1LCJmIFxcdGltZXMgZyArIGlkIl0sWzUsMiwiaWQgKyBcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
{X \times DY} \& {X \times (Y + DY)} \& {X \times Y + X \times DY} \&\& {A \times B + X \times DY} \\
\\
{D(A\times B)} \&\&\&\& {A\times B + D(A \times B)}
\arrow["out", from=3-1, to=3-5]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["{\coalg{-}}", dashed, from=1-1, to=3-1]
\arrow["{f \times g + id}", from=1-3, to=1-5]
\arrow["{id + \coalg{-}}", dashed, from=1-5, to=3-5]
\end{tikzcd}\]
We write $\coalg{-}$ to abbreviate the used coalgebra, i.e. in this diagram $\coalg{-} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}$
Next we check the strength laws:
\begin{itemize}
\item[\ref{S1}] To show that $(now \circ \pi_2)^* \circ \tau = \pi_2$ we do coinduction using the following coalgebra:
% https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFszLDAsIlggKyAxIFxcdGltZXMgRFgiXSxbMywxLCJYICsgRFgiXSxbMSwwLCIxIFxcdGltZXMgWCArIERYIl0sWzIsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyAhIl0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
\[\begin{tikzcd}
{1 \times DX} & {1 \times X + DX} & {1 \times X + 1 \times DX} & {X + 1 \times DX} \\
DX &&& {X + DX}
\arrow["out", from=2-1, to=2-4]
\arrow["{!}", dashed, from=1-1, to=2-1]
\arrow["{id + !}", from=1-4, to=2-4]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["{\pi_2 + id}", from=1-3, to=1-4]
\end{tikzcd}\]
% https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFszLDAsIlggKyAxIFxcdGltZXMgRFgiXSxbMywxLCJYICsgRFgiXSxbMSwwLCIxIFxcdGltZXMgWCArIERYIl0sWzIsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyBcXGNvYWxney19Il0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
{1 \times DX} \& {1 \times X + DX} \& {1 \times X + 1 \times DX} \& {X + 1 \times DX} \\
DX \&\&\& {X + DX}
\arrow["out", from=2-1, to=2-4]
\arrow["{\coalg{-}}", dashed, from=1-1, to=2-1]
\arrow["{id + \coalg{-}}", from=1-4, to=2-4]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\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:
\begin{equation*}
\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:
\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
\end{alignat*}
where the last step follows since $dstl \circ (id \times i_1) = i_1$.
\begin{equation*}
\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:
\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
\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:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXDshIiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
\[\begin{tikzcd}
{X \times DDY} & {X \times (DY + DDY)} & {X \times DY + X \times DDY} \\
&& {X \times Y + X \times DDY} \\
{D(X\times Y)} && {X \times Y + D(X \times Y)}
\arrow["{!}", dashed, from=1-1, to=3-1]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["out", from=3-1, to=3-3]
\arrow["{id + \;!}"', from=2-3, to=3-3]
\arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3]
\end{tikzcd}\]
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXGNvYWxney19IiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
{X \times DDY} \& {X \times (DY + DDY)} \& {X \times DY + X \times DDY} \\
\&\& {X \times Y + X \times DDY} \\
{D(X\times Y)} \&\& {X \times Y + D(X \times Y)}
\arrow["{\coalg{-}}", dashed, from=1-1, to=3-1]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["out", from=3-1, to=3-3]
\arrow["{id + \coalg{-}}"', from=2-3, to=3-3]
\arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3]
\end{tikzcd}\]
\item[\ref{S4}] To show $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ by coinduction we take the coalgebra:
% https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzEsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMiwwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXDshIiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
\[\begin{tikzcd}
{(X \times Y) \times DZ} & {(X \times Y) \times (Z+ DZ)} & {(X\times Y) \times Z + (X \times Y) \times DZ} \\
&& {X \times Y \times Z + (X \times Y) \times DZ} \\
{D(X \times Y \times Z)} && {X \times Y \times Z + D(X \times Y \times Z)}
\arrow["{!}", dashed, from=1-1, to=3-1]
\arrow["out", from=3-1, to=3-3]
\arrow["{id +\;!}"', from=2-3, to=3-3]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3]
\end{tikzcd}\]
% https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzEsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMiwwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiXFxjb2FsZ3stfSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXGNvYWxney19IiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
{(X \times Y) \times DZ} \& {(X \times Y) \times (Z+ DZ)} \& {(X\times Y) \times Z + (X \times Y) \times DZ} \\
\&\& {X \times Y \times Z + (X \times Y) \times DZ} \\
{D(X \times Y \times Z)} \&\& {X \times Y \times Z + D(X \times Y \times Z)}
\arrow["{\coalg{-}}", dashed, from=1-1, to=3-1]
\arrow["out", from=3-1, to=3-3]
\arrow["{id +\coalg{-}}"', from=2-3, to=3-3]
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3]
\end{tikzcd}\]
\end{itemize}
\end{proof}
To show that $\mathbf{D}$ is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
To prove that $\mathbf{D}$ is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
\begin{definition}
We call a morphism $g : X \rightarrow D (Y + X)$ \textit{guarded} if there exists an $h : X \rightarrow Y + D(Y+X)$ such that the following diagram commutes:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
X \&\&\& {D (Y +X)} \\
{Y + D(Y+X)} \&\&\& {(Y + X) + D(Y + X)}
\arrow["g", from=1-1, to=1-4]
\arrow["out", from=1-4, to=2-4]
\arrow["{i_1 + id}"', from=2-1, to=2-4]
\arrow["h"', from=1-1, to=2-1]
\end{tikzcd}\]
X \&\&\& {D (Y +X)} \\
{Y + D(Y+X)} \&\&\& {(Y + X) + D(Y + X)}
\arrow["g", from=1-1, to=1-4]
\arrow["out", from=1-4, to=2-4]
\arrow["{i_1 + id}"', from=2-1, to=2-4]
\arrow["h"', from=1-1, to=2-1]
\end{tikzcd}\]
\end{definition}
\begin{corollary}[Solution Theorem]
\label{cor:solution}
Let $g : X \rightarrow D(Y + X)$ be guarded. \textit{Solutions} of g are unique, i.e. given two morphisms $f, i : X \rightarrow DY$ then
$f = [ now , f ]^* \circ g$ and $i = [ now , i ]^* \circ g$ already implies $f = i$.
$f = [ now , f ]^* \circ g$ and $i = [ now , i ]^* \circ g$ already implies $f = i$.
\end{corollary}
\begin{proof}
Let $g : X \rightarrow D(Y + X)$ be guarded by $h : X \rightarrow Y + D(Y+X)$ and $f, i : X \rightarrow DY$ be solutions of g.
It suffices to show $[ now , f ]^* = [ now , i ]^*$, because then follows:
\[f = [ now , f ]^* \circ g = [ now , i ]^* \circ g = i\]
We prove this by coinduction using:
\change[inline]{Change name of morphism}
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcOyEiXSxbMiwwLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
{D(Y + X)} \& {(Y + X) + D(Y+X)} \&\& {Y + D(Y+X)} \\
DY \&\&\& {Y + DY}
\arrow["out", from=2-1, to=2-4]
\arrow["out", from=1-1, to=1-2]
\arrow["{[ [ i_1 , h ] , i_2 ]}", from=1-2, to=1-4]
\arrow["{id + \;!}", from=1-4, to=2-4]
\arrow["{!}", dashed, from=1-1, to=2-1]
\end{tikzcd}\]
{D(Y + X)} \& {(Y + X) + D(Y+X)} \&\& {Y + D(Y+X)} \\
DY \&\&\& {Y + DY}
\arrow["out", from=2-1, to=2-4]
\arrow["out", from=1-1, to=1-2]
\arrow["{[ [ i_1 , h ] , i_2 ]}", from=1-2, to=1-4]
\arrow["{id + \coalg{-}}", from=1-4, to=2-4]
\arrow["{\coalg{-}}", dashed, from=1-1, to=2-1]
\end{tikzcd}\]
\end{proof}
Let us record some facts that we will use to prove commutativity of $\mathbf{D}$:
\begin{corollary}
The following two properties hold:
\begin{alignat*}{1}
&out \circ Df = (f + Df) \circ out
\\&later \circ f^* = (later \circ f)^* = f^* \circ later
\end{alignat*}
As well as these properties of $\tau$ and $\sigma$:
\begin{alignat*}{2}
& out \circ \tau & & = (id + \tau) \circ dstl \circ (id \times out)\tag*{($\tau_1$)}\label{tau1}
\\&out \circ \sigma &&= (id + \sigma) \circ dstr \circ (out \times id)\tag*{($\sigma_1$)}\label{sigma1}
\\&\tau \circ (id \times out^{-1}) &&= out^{-1} \circ (id + \tau) \circ dstl\tag*{($\tau_2$)}\label{tau2}
\\& \sigma \circ (out^{-1} \times id) &&= out^{-1} \circ (id + \sigma) \circ dstr\tag*{($\sigma_2$)}\label{sigma2}
\end{alignat*}
\end{corollary}
\begin{proof}
Let us start with the first two properties:
\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}}
\end{alignat*}
\begin{alignat*}{1}
&(later \circ f)^*
% ... TODO
\\=\;&later \circ f^*
% ... TODO
\\=\;&f^* \circ later
\end{alignat*}
\begin{itemize}
\item[\ref{tau1}] This is just \ref{D3} restated.
\item[\ref{sigma1}]
\todo[inline]{What to do about out-law?}
\begin{alignat*}{1}
& out \circ Dswap \circ \tau \circ swap
\\=\;&(swap + Dswap) \circ out \circ \tau \circ swap
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ (id \times out) \circ swap \tag*{\ref{tau1}}
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ swap \circ (out \times id)
\\=\;&(swap + Dswap) \circ (id + \tau) \circ (swap + swap) \circ dstr \circ (out \times id)
\\=\;&(id + \sigma) \circ dstr \circ (out \times id)
\end{alignat*}
\item[\ref{tau2}]
\item[\ref{sigma2}]
\end{itemize}
\end{proof}
\begin{theorem}
@ -361,7 +425,7 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
\begin{proof}
Using corollary~\ref{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
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$ 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$.
@ -370,19 +434,65 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
\[\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 \]
\change[inline]{Make this more explicit}
The last step in both equations holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$ by 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
\end{alignat*}
\todo[inline]{The second to last step uses that $f^* \circ later = (later \circ f)^*$ this should be proven somewhere and referenced here.}
\todo[inline]{The fact that $f^* \circ Dg = (f \circ g)^*$ should be mentioned somewhere (in preliminaries!)}
\change[inline]{Move this remark to the beginning of proof}
The first step in both equations can be proven by monicity of $out$ and then using \ref{D3} and the dual diagram for $\sigma$ which is a direct consequence of \ref{D3}:
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgK0QoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzAsMSwiXFxoYXR7XFx0YXV9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywib3V0Il0sWzIsMywiaWQgKyBcXGhhdHtcXHRhdX0iLDJdLFswLDQsImlkIFxcdGltZXMgb3V0Il0sWzQsMiwiZHN0bCJdXQ==
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgK0QoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzAsMSwiXFxzaWdtYSJdLFsxLDMsIm91dCJdLFsyLDMsImlkICsgXFxoYXR7XFx0YXV9IiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDIsImRzdGwiXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
{X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
{D(X \times Y)} \&\&\&\& {X \times Y +D(X \times Y)}
\arrow["{\sigma}", dashed, from=1-1, to=2-1]
\arrow["out", from=2-1, to=2-5]
\arrow["{id + \sigma}"', from=1-5, to=2-5]
\arrow["{id \times out}", from=1-1, to=1-3]
\arrow["dstl", from=1-3, to=1-5]
\end{tikzcd}\]
the last step holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$.
{X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
{D(X \times Y)} \&\&\&\& {X \times Y +D(X \times Y)}
\arrow["\sigma", from=1-1, to=2-1]
\arrow["out", from=2-1, to=2-5]
\arrow["{id + \hat{\tau}}"', from=1-5, to=2-5]
\arrow["{id \times out}", from=1-1, to=1-3]
\arrow["dstl", from=1-3, to=1-5]
\end{tikzcd}\]
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$:
\begin{alignat*}{1}
& out \circ \sigma^* \circ \tau
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ (id + \tau) \circ dstl \circ (id \times out)\tag*{\ref{D3}}
\\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ dstl \circ (id \times out)\tag*{(outsigma)}
\\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ ((out^{-1} \times id) + (out^{-1} \times id)) \circ dstl \circ (out \times out)
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ \tau \circ (out^{-1} \times id)] \circ dstl \circ (out \times out)
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ D(out^{-1} \times id) \circ \tau] \circ dstl \circ (out \times out)
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (\sigma \times (out^{-1} \times id))^* \circ \tau] \circ dstl \circ (out \times out)
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma) \circ dstr)^* \circ \tau] \circ dstl \circ (out \times out)\tag*{($\sigma$)}
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ Ddstr \circ \tau] \circ dstl \circ (out \times out)
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ [D i_1 \circ \tau , D i_2 \circ \tau] \circ dstr] \circ dstl \circ (out \times out)\tag*{\ref{Dcomm-helper}}
\\=\;&[ (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 \tag*{(later)}
\end{alignat*}
where
\[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\]
follows by the fact that $dstr^{-1}$ is epic:
\begin{alignat*}{1}
& Ddstr \circ \tau \circ dstr^{-1}
\\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ]
\\=\;&[ Ddstr \circ D(i_1 \times id) \circ \tau , Ddstr \circ D(i_2 \times id) \circ \tau ]
\\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ]
\end{alignat*}
\todo[inline]{Add $dstl-i_1$ etc. to preliminaries as corollary!}
\end{proof}
\improvement[inline]{Elaborate more?}

1
thesis/src/04_iteration.tex
View file

@ -111,6 +111,7 @@ In this section we will study the monad that arises from existence of all free E
If every $X \in \obj{\C}$ extends to a free Elgot algebra $KX$ we get a monad $\mathbf{K}$.
\end{lemma}
\begin{proof}
\todo[inline]{Maybe this can even be proven without adjunction, show that free objects yield a Kleisli triple!}
\todo[inline]{Proof in preliminaries}
Existence of all free objects in $\elgotalgs{\C}$ yields an adjunction between $\C$ and $\elgotalgs{\C}$ that in turn gives us a monad on $\C$.
\end{proof}