leonv/bsc-consolidated
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

add agda refs

Browse source
This commit is contained in:
Leon Vatthauer 2024-07-17 17:38:21 +02:00
parent 34003081dd
commit c435da1c06
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
9 changed files with 172 additions and 1852 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -18,6 +18,7 @@ agda/public/
.#*
*~
_minted-main/
main.pdf
# AUTOGENERATED
# All wildcards below this marker are used to remove generated files in
# 'make clean'

BIN
img/agda.pdf Normal file
View file

Binary file not shown.

BIN
main.pdf
View file

Binary file not shown.

25
main.tex
View file

@ -1,7 +1,9 @@
\documentclass[a4paper,11pt,numbers=noenddot]{scrbook}
\documentclass[a4paper,10pt,numbers=noenddot,twocolumn]{scrbook}
\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
\KOMAoptions{twoside=false}
\usepackage[top=2cm,lmargin=0.5in,rmargin=0.5in,bottom=3cm,hmarginratio=1:1]{geometry}
\usepackage[ngerman, english]{babel}
\usepackage[moderate, title=tight, bibliography=tight, margins=tight]{savetrees}
\babeltags{german=ngerman}
% \usepackage{mathabx}
% \usepackage{amssymb}
@ -197,25 +199,16 @@
\begin{document}
\pagestyle{plain}
\input{src/titlepage}%
\chapter*{Disclaimer}
{\begin{german}
Ich versichere, dass ich die Arbeit ohne fremde Hilfe und ohne Benutzung anderer als der angegebenen Quellen angefertigt habe und dass die Arbeit in gleicher oder ähnlicher Form noch keiner anderen Prüfungsbehörde vorgelegen hat und von dieser als Teil einer Prüfungsleistung angenommen wurde.
Alle Ausführungen, die wörtlich oder sinngemäß übernommen wurden, sind als solche gekennzeichnet.
\vspace{5em}
Erlangen, \foreignlanguage[date]{ngerman}{\today{}} \rule{7cm}{1pt}\\
\phantom{Erlangen, \today{}} \theauthor{}
\end{german}}
% \chapter*{Licensing}
% \doclicenseThis{}
\include{src/00_abstract}
\twocolumn[\include{src/00_abstract}]
\tableofcontents
% \listoftodos\
\newcommand{\agda}{{\raisebox{-0.075cm}{\includegraphics[height=1em]{img/agda.pdf}}}}
\newcommand{\agdaref}[1]{\href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/#1.html}{\agda}}
\newcommandx{\unsure}[2][1=]{\todo[inline,linecolor=red,backgroundcolor=red!25,bordercolor=red,#1]{#2}}
\newcommandx{\change}[2][1=]{\todo[linecolor=blue,backgroundcolor=blue!25,bordercolor=blue,#1]{#2}}
\newcommandx{\info}[2][1=]{\todo[inline,linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}}
@ -236,7 +229,7 @@
\include{src/04_partiality-monads}
\include{src/05_iteration}
\include{src/06_setoids}
\include{src/07_conclusion}
\twocolumn[\include{src/07_conclusion}]
\appendix

302
src/02_preliminaries.tex
View file

@ -5,25 +5,34 @@ In this chapter we will introduce notation that will be used throughout the thes
We write \(\obj{\C}\) for the objects of a category \( \C \), \(id_X\) for the identity morphism on \(X\), \((-) \circ (-)\) for the composition of morphisms and \(\C(X,Y)\) for the set of morphisms between \(X\) and \(Y\).
We will also sometimes omit indices of the identity and of natural transformations in favor of readability.
\section{Distributive and Cartesian Closed Categories}
\section{Distributive Categories}
Let us first introduce notation for binary (co)products by giving their usual diagrams: % chktex 36
% https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
% https://q.uiver.app/#q=WzAsNCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
\[
\begin{tikzcd}
A && {A \times B} && B && A && {A + B} && B \\
A && {A \times B} && B \\
\\
&& C &&&&&& C
&& C
\arrow["{\pi_1}"', from=1-3, to=1-1]
\arrow["{\pi_2}", from=1-3, to=1-5]
\arrow["g"', from=3-3, to=1-5]
\arrow["f", from=3-3, to=1-1]
\arrow["{\exists! \langle f , g \rangle}"', dashed, from=3-3, to=1-3]
\arrow["{i_1}", from=1-7, to=1-9]
\arrow["{i_2}"', from=1-11, to=1-9]
\arrow["f"', from=1-7, to=3-9]
\arrow["g", from=1-11, to=3-9]
\arrow["{\exists ! [f , g]}", dashed, from=1-9, to=3-9]
\arrow["g"', from=3-3, to=1-5]
\end{tikzcd}
\]
% https://q.uiver.app/#q=WzAsNCxbMiwwLCJBICsgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFsxLDAsImlfMSJdLFsyLDAsImlfMiIsMl0sWzEsMywiZiIsMl0sWzIsMywiZyJdLFswLDMsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
\[
\begin{tikzcd}
A && {A + B} && B \\
\\
&& C
\arrow["{i_1}", from=1-1, to=1-3]
\arrow["f"', from=1-1, to=3-3]
\arrow["{\exists ! [f , g]}"{description}, from=1-3, to=3-3]
\arrow["{i_2}"', from=1-5, to=1-3]
\arrow["g", from=1-5, to=3-3]
\end{tikzcd}
\]
@ -33,7 +42,7 @@ We write \(1\) for the terminal object together with the unique morphism \(! : A
Categories with finite products (i.e.\ binary products and a terminal object) are also called Cartesian and categories with finite coproducts (i.e.\ binary coproducts and an initial object) are called coCartesian.
\begin{definition}[Distributive Category]~\label{def:distributive}
\begin{definition}[Distributive Category (\agdaref{Categories.Category.Distributive})]~\label{def:distributive}
A Cartesian and coCartesian category \(\C \) is called distributive if the canonical (left) distributivity morphism \(dstl^{-1}\) is an isomorphism:
% https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
\[
@ -64,40 +73,33 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
where \(swap := \langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A\).
\end{remark}
\begin{proposition}
\begin{proposition}[\agdaref{Categories.Category.Distributive.Properties}]
The distribution morphisms can be viewed as natural transformations i.e.\ they satisfy the following diagrams:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiJdXQ==
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl1d
\[
\begin{tikzcd}[column sep=4ex]
{X \times (Y +Z)} && {A \times (B + C)} & {(Y + Z) \times X} && {(B + C) \times A} \\
{X \times Y + X \times Z} && {A \times B + A \times C} & {Y \times X + Z \times X} && {B \times A + C \times A}
\begin{tikzcd}
{X \times (Y +Z)} && {A \times (B + C)} \\
{X \times Y + X \times Z} && {A \times B + A \times C}
\arrow["{f \times (g + h)}", from=1-1, to=1-3]
\arrow["{f \times g + f \times h}", from=2-1, to=2-3]
\arrow["dstl", from=1-1, to=2-1]
\arrow["dstl", from=1-3, to=2-3]
\arrow["{(g + h) \times f}", from=1-4, to=1-6]
\arrow["dstr"', from=1-4, to=2-4]
\arrow["dstr", from=1-6, to=2-6]
\arrow["{g \times f + h \times f}", from=2-4, to=2-6]
\arrow["{f \times g + f \times h}", from=2-1, to=2-3]
\end{tikzcd}
\]
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIoWSArIFopIFxcdGltZXMgWCJdLFsyLDAsIihCICsgQykgXFx0aW1lcyBBIl0sWzAsMSwiWSBcXHRpbWVzIFggKyBaIFxcdGltZXMgWCJdLFsyLDEsIkIgXFx0aW1lcyBBICsgQyBcXHRpbWVzIEEiXSxbMCwxLCIoZyArIGgpIFxcdGltZXMgZiJdLFswLDIsImRzdHIiLDJdLFsxLDMsImRzdHIiXSxbMiwzLCJnIFxcdGltZXMgZiArIGggXFx0aW1lcyBmIl1d
\[
\begin{tikzcd}
{(Y + Z) \times X} && {(B + C) \times A} \\
{Y \times X + Z \times X} && {B \times A + C \times A}
\arrow["{(g + h) \times f}", from=1-1, to=1-3]
\arrow["dstr"', from=1-1, to=2-1]
\arrow["dstr", from=1-3, to=2-3]
\arrow["{g \times f + h \times f}", from=2-1, to=2-3]
\end{tikzcd}
\]
\end{proposition}
\begin{proof}
We will prove naturality of \(dstl\), naturality for \(dstr\) is symmetric. We use the fact that \(dstl^{-1}\) is an iso and therefore also an epi.
\begin{alignat*}{1}
& dstl \circ (f \times (g + h)) \circ dstl^{-1} \\
=\; & dstl \circ (f \times (g + h)) \circ \lbrack id \times i_1 , id \times i_2 \rbrack \\
=\; & dstl \circ \lbrack f \times ((g + h) \circ i_1) , f \times ((g + h) \circ i_2) \rbrack \\
=\; & dstl \circ \lbrack f \times (i_1 \circ g) , f \times (i_2 \circ h) \rbrack \\
=\; & dstl \circ \lbrack id \times i_1 , id \times i_2 \rbrack \circ (f \times g + f \times h) \\
=\; & dstl \circ dstl^{-1} \circ (f \times g + f \times h) \\
=\; & (f \times g + f \times h) \\
=\; & (f \times g + f \times h) \circ dstl \circ dstl^{-1}\tag*{\qedhere}
\end{alignat*}
\end{proof}
\begin{proposition}
\begin{proposition}[\agdaref{Categories.Category.Distributive.Properties}]
The distribution morphisms satisfy the following properties:
\begin{enumerate}
@ -113,52 +115,8 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\item \(dstr \circ swap = (swap + swap) \circ dstl\)
\end{enumerate}
\end{proposition}
\begin{proof}
Let us verify the five properties concerning \(dstl\), the ones concerning \(dstr\) follow symmetrically:
\begin{enumerate}
\item
\begin{alignat*}{1}
& dstl \circ (id \times i_1)
\\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ i_1
\\=\;&dstl \circ dstl^{-1} \circ i_1
\\=\;&i_1
\end{alignat*}
\item
\begin{alignat*}{1}
& dstl \circ (id \times i_2)
\\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ i_2
\\=\;&dstl \circ dstl^{-1} \circ i_2
\\=\;&i_2
\end{alignat*}
\item
\begin{alignat*}{1}
& \pi_1
\\=\;&\pi_1 \circ dstl^{-1} \circ dstl
\\=\;&[ \pi_1 \circ (id \times i_1) , \pi_1 \circ (id \times i_2) ] \circ dstl
\\=\;&[ \pi_1 , \pi_1 ] \circ dstl
\end{alignat*}
\item
\begin{alignat*}{1}
& \pi_2
\\=\;&\pi_2 \circ dstl^{-1} \circ dstl
\\=\;&[ \pi_2 \circ (id \times i_1) , \pi_2 \circ (id \times i_2) ] \circ dstl
\\=\;&(\pi_2 + \pi_2) \circ dstl
\end{alignat*}
\item
\begin{alignat*}{1}
& dstl \circ swap
\\=\;&dstl \circ swap \circ dstr^{-1} \circ dstr
\\=\;&dstl \circ [ swap \circ (i_1 \times id) , swap \circ (i_2 \times id) ] \circ dstr
\\=\;&dstl \circ [ (id \times i_1) \circ swap , (id \times i_2) \circ swap ] \circ dstr
\\=\;&dstl \circ [ id \times i_1 , id \times i_2 ] \circ (swap + swap) \circ dstr
\\=\;&dstl \circ dstl^{-1} \circ (swap + swap) \circ dstr
\\=\;&(swap + swap) \circ dstr\tag*{\qedhere}
\end{alignat*}
\end{enumerate}
\end{proof}
\begin{definition}[Exponential Object]
\begin{definition}[Exponential Object (\agdaref{Categories.Object.Exponential})]
Let \(\C \) be a Cartesian category and \(X , Y \in \vert \C \vert \).
An object \(X^Y\) is called an exponential object (of \(X\) and \(Y\)) if there exists an evaluation morphism \(eval : X^Y \times Y \rightarrow X\) and for any \(f : X \times Y \rightarrow Z\) there exists a morphism \(curry\; f : X \rightarrow Z^Y\) that is unique with respect to the following diagram:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJaIFxcdGltZXMgWSJdLFsyLDAsIlheWSBcXHRpbWVzIFkiXSxbMiwyLCJYIl0sWzEsMiwiZXZhbCJdLFswLDEsImN1cnJ5XFw7ZiBcXHRpbWVzIGlkIl0sWzAsMiwiZiIsMl1d
@ -174,7 +132,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\]
\end{definition}
\begin{proposition}
\begin{proposition}[\agdaref{Categories.Object.Exponential}]
Every exponential object \(X^Y\) satisfies the following properties:
\begin{enumerate}
@ -183,16 +141,6 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
\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{proposition}
\begin{proof}
\begin{enumerate}
\item Let \(f, g : X \times Y \rightarrow Z\) and \(curry\;f = curry\;g\), then indeed
\[f = eval \circ (curry\; f \times id) = eval \circ (curry\;g \times id) = g. \]
\item \(curry(eval \circ (f \times id)) = f\) follows instantly by uniqueness of \(curry(eval \circ (f \times id))\).
\item Note that \(eval \circ (curry\;f \circ g \times id) = eval \circ (curry\;f \times id) \circ (g \times id) = f \circ (g \times id)\), thus we are done by uniqueness of \(curry(f \circ (g \times id))\).
\qedhere
\end{enumerate}
\end{proof}
A Cartesian closed category is a Cartesian category \(\C \) that also has an exponential object \(X^Y\) for any \(X, Y \in \obj{\C} \).
The internal logic of Cartesian closed categories is the simply typed \(\lambda \)-calculus, which makes them a suitable environment for interpreting programming languages.
@ -201,11 +149,11 @@ For the rest of this thesis we will work in an ambient distributive category \(\
\section{F-Coalgebras}
Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tuples \((X, \alpha : FX \rightarrow X)\) consisting of an object of \(\C \) and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modeling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras; let us formally introduce them now.
\begin{definition}[F-Coalgebra]
\begin{definition}[F-Coalgebra (\agdaref{Categories.Functor.Coalgebra})]
A tuple \((X \in \obj{\C}, \alpha : X \rightarrow FX)\) is called an \emph{F-coalgebra} (hereafter referred to as just \emph{coalgebra}).
\end{definition}
\begin{definition}[Coalgebra Morphisms]\label{def:coalgmorph}
\begin{definition}[Coalgebra Morphisms (\agdaref{Categories.Functor.Coalgebra})]\label{def:coalgmorph}
Let \((X, \alpha : X \rightarrow FX)\) and \((Y, \beta : Y \rightarrow FY)\) be two coalgebras. A morphism between these coalgebras is a morphism \(f : X \rightarrow Y\) such that the following diagram commutes:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMiwiWSJdLFsyLDAsIkZYIl0sWzIsMiwiRlkiXSxbMSwzLCJcXGJldGEiXSxbMCwyLCJcXGFscGhhIl0sWzAsMSwiZiIsMl0sWzIsMywiRmYiXV0=
\[
@ -224,27 +172,15 @@ Let \(F : \C \rightarrow \C \) be an endofunctor. Recall that F-algebras are tup
Coalgebras on a given functor together with their morphisms form a category that we call \(\coalgs{F}\).
\begin{proposition}
\begin{proposition}[\agdaref{Categories.Category.Construction.F-Coalgebras}]
\(\coalgs{F}\) is a category.
\end{proposition}
\begin{proof}
Let \((X , \alpha : X \rightarrow FX)\) be a coalgebra. The identity morphism on \((X , \alpha)\) is the identity morphism of \(\C\) that trivially satisfies \(\alpha \circ id = Fid \circ \alpha \).
Let \((X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)\) and \((Z , \gamma : Z \rightarrow FZ)\) be coalgebras.
Composition of \(f : (X, \alpha) \rightarrow (Y, \beta)\) and \(g : (Y, \beta) \rightarrow (Z, \gamma)\) is composition of the underlying morphisms in \(\C \) where:
\begin{alignat*}{1}
& \gamma \circ g \circ f \\
=\; & Fg \circ \beta \circ f \\
=\; & Fg \circ Ff \circ \alpha \\
=\; & F(g \circ f) \circ \alpha\tag*{\qedhere}
\end{alignat*}
\end{proof}
The terminal object of \(\coalgs{F}\) is sometimes called \textit{final coalgebra}, we will however call it the \textit{terminal coalgebra} for consistency with initial F-algebras.
Similarly to initial F-algebras, the final coalgebra can be used for modeling the semantics of coinductive data types where terminality of the coalgebra yields corecursion as a definitional principle and coinduction as a proof principle.
Let us make the universal property of terminal coalgebras concrete.
\begin{definition}[Terminal Coalgebra]
\begin{definition}[Terminal Coalgebra (\agdaref{Categories.Object.Terminal})]
A coalgebra \((T, t : T \rightarrow FT)\) is called a terminal coalgebra if for any other coalgebra \((X, \alpha : X \rightarrow FX)\) there exists a unique morphism \(\coalg{\alpha} : X \rightarrow T\) satisfying:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzIsMCwiRlgiXSxbMCwyLCJUIl0sWzIsMiwiRlQiXSxbMCwxLCJcXGFscGhhIl0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IFxcYWxwaGEgXFxycmJyYWNrZXQiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMSwzLCJGXFxsbGJyYWNrZXQgXFxhbHBoYSBcXHJyYnJhY2tldCJdXQ==
@ -264,51 +200,14 @@ Let us make the universal property of terminal coalgebras concrete.
We will discuss the concrete form that induction and coinduction take in a type theory in \autoref{chp:agda-cat}. Let us now reiterate a famous Lemma concerning terminal F-coalgebras.
\begin{lemma}[Lambek's Lemma~\cite{lambek}]\label{lem:lambek}
\begin{lemma}[Lambek's Lemma~\cite{lambek} (\agdaref{Categories.Category.Construction.F-Coalgebras})]\label{lem:lambek}
Let \((T, t : T \rightarrow FT)\) be a terminal coalgebra. Then \(t\) is an isomorphism.
\end{lemma}
% \begin{proof}
% First note that \((FT, Ft : FT \rightarrow FFT)\) is also an F-coalgebra. This yields the unique morphism \(\coalg{Ft} : FT \rightarrow T\) satisfying:
% % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGVCJdLFsyLDAsIkZGVCJdLFswLDIsIlQiXSxbMiwyLCJGVCJdLFswLDEsIkZ0Il0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywiRlxcbGxicmFja2V0IEZ0IFxccnJicmFja2V0Il1d
% \[
% \begin{tikzcd}[ampersand replacement=\&]
% FT \&\& FFT \\
% \\
% T \&\& FT
% \arrow["Ft", from=1-1, to=1-3]
% \arrow["t", from=3-1, to=3-3]
% \arrow["{\coalg{Ft}}"', dashed, from=1-1, to=3-1]
% \arrow["{F\coalg{Ft}}", from=1-3, to=3-3]
% \end{tikzcd}
% \]
% \(\coalg{Ft}\) is inverse to \(t\):
% \begin{enumerate}
% \item \(\coalg{Ft} \circ t : (T, t) \rightarrow (T, t)\) is a morphism between F-coalgebras since
% \begin{alignat*}{1}
% & F(\coalg{Ft} \circ t) \circ t \\
% =\; & F \coalg{Ft} \circ t \circ t \\
% =\; & F \coalg{Ft} \circ Ft \circ t \\
% =\; & t \circ \coalg{Ft} \circ t
% \end{alignat*}
% By uniqueness of the identity on \((T, t)\) we follow that \(\coalg{Ft} \circ t = id\).
% \item \(t \circ \coalg{Ft} = id : (FT, Ft) \rightarrow (FT, Ft)\) follows by:
% \begin{alignat*}{1}
% & t \circ \coalg{Ft} \\
% =\; & F\coalg{Ft} \circ Ft \\
% =\; & F(\coalg{Ft} \circ t) \\
% =\; & F(id) \\
% =\; & id
% \end{alignat*}
% \end{enumerate}
% \end{proof}
\section{Monads}
Monads are widely known in functional programming as a means for modeling effects in ``pure'' languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
\begin{definition}[Monad]
\begin{definition}[Monad (\agdaref{Categories.Monad})]
A monad \(\mathbf{T}\) on a category \(\C \) is a triple \((T, \eta, \mu)\), where \(T : \C \rightarrow \C \) is an endofunctor and \(\eta : Id \rightarrow T, \mu : TT \rightarrow T\) are natural transformations, satisfying the following laws:
\begin{alignat*}{2}
& \mu_X \circ \mu_{TX} & & = \mu_X \circ T\mu_X \tag*{(M1)}\label{M1} \\
@ -317,41 +216,55 @@ Monads are widely known in functional programming as a means for modeling effect
\end{alignat*}
These laws are expressed by the following diagrams:
% with indices: % https://q.uiver.app/#q=WzAsOCxbMCwwLCJUVFRYIl0sWzIsMCwiVFRYIl0sWzAsMiwiVFRYIl0sWzIsMiwiVFgiXSxbNCwwLCJUWCJdLFs2LDAsIlRUWCJdLFs4LDAsIlRYIl0sWzYsMiwiVFgiXSxbMCwxLCJcXG11X3tUWH0iXSxbMCwyLCJUXFxtdV9YIiwyXSxbMSwzLCJcXG11X1giXSxbNSw3LCJcXG11X1giXSxbNCw1LCJcXGV0YV97VFh9Il0sWzYsNSwiVFxcZXRhX1giXSxbNCw3LCJpZF97VFh9IiwyXSxbNiw3LCJpZF97VFh9IiwyXSxbMiwzLCJcXG11X1giLDJdXQ==
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJUVFRYIl0sWzIsMCwiVFRYIl0sWzAsMiwiVFRYIl0sWzIsMiwiVFgiXSxbNCwwLCJUWCJdLFs2LDAsIlRUWCJdLFs4LDAsIlRYIl0sWzYsMiwiVFgiXSxbMCwxLCJcXG11Il0sWzAsMiwiVFxcbXUiLDJdLFsxLDMsIlxcbXUiXSxbNSw3LCJcXG11Il0sWzQsNSwiXFxldGEiXSxbNiw1LCJUIl0sWzQsNywiaWQiLDJdLFs2LDcsImlkIiwyXSxbMiwzLCJcXG11IiwyXV0=
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJUVFRYIl0sWzIsMCwiVFRYIl0sWzAsMiwiVFRYIl0sWzIsMiwiVFgiXSxbMCwxLCJcXG11X3tUWH0iXSxbMCwyLCJUXFxtdV9YIiwyXSxbMSwzLCJcXG11X1giXSxbMiwzLCJcXG11X1giLDJdXQ==
\[
\begin{tikzcd}
TTTX && TTX && TX && TTX && TX \\
TTTX && TTX \\
\\
TTX && TX &&&& TX
\arrow["\mu", from=1-1, to=1-3]
\arrow["T\mu"', from=1-1, to=3-1]
TTX && TX
\arrow["{\mu_{TX}}", from=1-1, to=1-3]
\arrow["{T\mu_X}"', from=1-1, to=3-1]
\arrow["{\mu_X}", from=1-3, to=3-3]
\arrow["{\mu_X}"', from=3-1, to=3-3]
\end{tikzcd}
\]
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJUWCJdLFsyLDAsIlRUWCJdLFs0LDAsIlRYIl0sWzIsMiwiVFgiXSxbMSwzLCJcXG11Il0sWzAsMSwiXFxldGEiXSxbMiwxLCJUIl0sWzAsMywiaWQiLDJdLFsyLDMsImlkIiwyXV0=
\[
\begin{tikzcd}
TX && TTX && TX \\
\\
&& TX
\arrow["\eta", from=1-1, to=1-3]
\arrow["id"', from=1-1, to=3-3]
\arrow["\mu", from=1-3, to=3-3]
\arrow["\mu", from=1-7, to=3-7]
\arrow["\eta", from=1-5, to=1-7]
\arrow["T", from=1-9, to=1-7]
\arrow["id"', from=1-5, to=3-7]
\arrow["id"', from=1-9, to=3-7]
\arrow["\mu"', from=3-1, to=3-3]
\arrow["T", from=1-5, to=1-3]
\arrow["id"', from=1-5, to=3-3]
\end{tikzcd}
\]
\end{definition}
\begin{definition}[Monad Morphism]\label{def:monadmorphism}
\begin{definition}[Monad Morphism (\agdaref{Categories.Monad.Morphism})]\label{def:monadmorphism}
A morphism between monads \((S : \C \rightarrow \C, \eta^S, \mu^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T)\) is a natural transformation \(\alpha : S \rightarrow T\) between the underlying functors such that the following diagrams commute.
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFszLDAsIlNTWCJdLFs1LDAsIlNUWCJdLFszLDEsIlNYIl0sWzcsMCwiVFRYIl0sWzcsMSwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFswLDEsIlxcZXRhXlMiXSxbMSwyLCJcXGFscGhhIl0sWzAsMiwiXFxldGFeVCIsMl1d
\[
\begin{tikzcd}[ampersand replacement=\&]
X \&\& SX \& SSX \&\& STX \&\& TTX \\
\&\& TX \& SX \&\&\&\& TX
\begin{tikzcd}
X && SX \\
&& TX
\arrow["{\eta^S}", from=1-1, to=1-3]
\arrow["\alpha", from=1-3, to=2-3]
\arrow["{\eta^T}"', from=1-1, to=2-3]
\arrow["S\alpha", from=1-4, to=1-6]
\arrow["{\mu^S}"', from=1-4, to=2-4]
\arrow["\alpha", from=1-6, to=1-8]
\arrow["\alpha"', from=2-4, to=2-8]
\arrow["{\mu^T}", from=1-8, to=2-8]
\arrow["\alpha", from=1-3, to=2-3]
\end{tikzcd}
\]
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJTU1giXSxbMiwwLCJTVFgiXSxbMCwxLCJTWCJdLFs0LDAsIlRUWCJdLFs0LDEsIlRYIl0sWzAsMSwiU1xcYWxwaGEiXSxbMCwyLCJcXG11XlMiLDJdLFsxLDMsIlxcYWxwaGEiXSxbMiw0LCJcXGFscGhhIiwyXSxbMyw0LCJcXG11XlQiXV0=
\[
\begin{tikzcd}
SSX && STX && TTX \\
SX &&&& TX
\arrow["{S\alpha}", from=1-1, to=1-3]
\arrow["{\mu^S}"', from=1-1, to=2-1]
\arrow["\alpha", from=1-3, to=1-5]
\arrow["{\mu^T}", from=1-5, to=2-5]
\arrow["\alpha"', from=2-1, to=2-5]
\end{tikzcd}
\]
\end{definition}
@ -361,13 +274,10 @@ This yields a category of monads on a given category \(\C\) that we call \(\mona
\begin{proposition}\label{prop:monadscat}
\(\monads{\C}\) is a category.
\end{proposition}
\begin{proof}
The identity morphism of \(\monads{\C}\) is the identity natural transformation \(Id : F \rightarrow F\), which trivially respects the monad unit and multiplication. Composition of monad morphisms is composition of the underlying natural transformation, the diagrams then also follow easily.
\end{proof}
Monads can also be specified in a second equivalent way that is better suited to describe computation.
\begin{definition}[Kleisli Triple]
\begin{definition}[Kleisli Triple (\agdaref{Categories.Monad.Relative})]
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*}{3}
& \eta_X^* & & = id_{FX} \tag*{(K1)}\label{K1} \\
@ -384,7 +294,7 @@ Let \(f : X \rightarrow TY, g : Y \rightarrow TZ\) be two programs, where \(T\)
This yields the category of programs for a Kleisli triple that is called the Kleisli category.
\begin{definition}[Kleisli Category]
\begin{definition}[Kleisli Category (\agdaref{Categories.Category.Construction.Kleisli})]
Given a monad \(T\) on a category \(\C \), the Kleisli category \(\C^T\) is defined as:
\begin{itemize}
\item \(\vert \C^T \vert = \obj{C}\)
@ -395,22 +305,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{proposition}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
\begin{proposition}[\cite{manes} (\agdaref{Categories.Monad.Construction.Kleisli})] 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.
``\(\Rightarrow \)'':
Given a Kleisli triple \((F, \eta, {(-)}^*)\),
we obtain a monad \((F, \eta, \mu)\) where \(F\) is the object mapping of the Kleisli triple together with the functor action \(F(f : X \rightarrow Y) = {(\eta_Y \circ f)}^*\),
\(\eta \) is the morphism family of the Kleisli triple where naturality is easy to show and \(\mu \) is a natural transformation defined as \(\mu_X = id_{FX}^*\)
``\(\Leftarrow \)'': \\
Given a monad \((F, \eta, \mu)\),
we obtain a Kleisli triple \((F, \eta, {(-)}^*)\) by restricting the functor \(F\) on objects,
taking the underlying mapping of \(\eta \) and defining \(f^* = \mu_Y \circ Ff\) for any \(f : X \rightarrow FY\).
\end{proof}
For the rest of this thesis we will use both equivalent notions interchangeably to make definitions easier.
@ -424,7 +320,7 @@ where \(g : X \rightarrow TY\) and \(f : X \times Y \rightarrow TZ\) are program
\[X \overset{\langle id , g \rangle}{\longrightarrow} X \times TY \overset{?}{\longrightarrow} T(X \times Y) \overset{f^*}{\longrightarrow} TZ. \]
Instead, one needs the following stronger notion of monad.
\begin{definition}[Strong Monad] A monad \((T, \eta, \mu)\) on a Cartesian category \(\C \) is called strong if there exists a natural transformation \(\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)\) that satisfies the following conditions:
\begin{definition}[Strong Monad (\agdaref{Categories.Monad.Strong})] A monad \((T, \eta, \mu)\) on a Cartesian category \(\C \) is called strong if there exists a natural transformation \(\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)\) that satisfies the following conditions:
\begin{alignat*}{2}
& T\pi_2 \circ \tau_{1,X} & & = \pi_2 \tag*{(S1)}\label{S1} \\
& \tau_{X,Y} \circ (id_X \times \eta_Y) & & = \eta_{X\times Y} \tag*{(S2)}\label{S2} \\
@ -468,7 +364,7 @@ Let us now consider the following two programs
\end{multicols}
Where \(p : TX\) and \(q : TY\) are computations of some monad \(T\). A monad where these programs are equal, is called commutative.
\begin{definition}[Commutative Monad]
\begin{definition}[Commutative Monad (\agdaref{Categories.Monad.Commutative})]
A strong monad \(\mathbf{T}\) is called commutative if the (right) strength \(\tau \) commutes with the induced left strength
\[\sigma_{X,Y} = Tswap \circ \tau_{Y,X} \circ swap : TX \times Y \rightarrow T(X \times Y)\]
that satisfies symmetrical conditions to the ones \(\tau \) satisfies.
@ -492,7 +388,7 @@ Free objects, roughly speaking, are constructions for instantiating structure de
We will rely on free structures in \autoref{chp:iteration} to define a monad in a general setting. We recall the definition
to establish some notation and then describe how to obtain a monad via existence of free objects.
\begin{definition}[Free Object]\label{def:free}
\begin{definition}[Free Object (\agdaref{Categories.FreeObjects.Free})]\label{def:free}
Let \(\C, \D \) be categories and \(U : \C \rightarrow \D \) be a forgetful functor (whose construction usually is obvious). A free object on some object \(X \in \obj{\D}\) is an object \(FX \in \obj{\C}\) together with a morphism \(\eta : X \rightarrow UFX\) such that for any \(Y \in \obj{\C}\) and \(f : X \rightarrow UY\) there exists a unique morphism \(\free{f} : FX \rightarrow Y\) satisfying:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJVRlgiXSxbMCwxLCJmIl0sWzAsMiwiXFxldGEiLDJdLFsyLDEsIlVcXGZyZWV7Zn0iLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
\[
@ -506,23 +402,7 @@ to establish some notation and then describe how to obtain a monad via existence
\]
\end{definition}
\begin{proposition}\label{thm:freemonad}
\begin{proposition}[\agdaref{Categories.FreeObjects.Free},\agdaref{Categories.Adjoint.Properties}]\label{thm:freemonad}
Let \(U : \C \rightarrow \D \) be a forgetful functor.
If for every \(X \in \obj{\D}\) a free object \(FX \in \obj{C}\) exists then \((X \mapsto UFX, \eta : X \rightarrow UFX, \free{(f : X \rightarrow UFY)} : UFX \rightarrow UFY)\) is a Kleisli triple on \(\D \).
\end{proposition}
\begin{proof}
We are left to check the laws of Kleisli triples.
\begin{itemize}
\item[\ref{K1}] \(\free{\eta} = id\)
By uniqueness of \(\free{\eta}\) it suffices to show that \(id \circ \eta = \eta \) which holds trivially.
\item[\ref{K2}] \(\free{f} \circ \eta = f\) for any \(f : X \rightarrow UFY\)
This is the universal property concerning \(\free{f}\).
\item[\ref{K3}] \(\free{f} \circ \free{g} = \free{\freee{f} \circ g}\) for any \(f : Y \rightarrow UFZ, g : X \rightarrow UFY\)
By uniqueness of \(\free{\freee{f} \circ g}\) we are left to show \(\free{f} \circ \free{g} \circ \eta = \free{f} \circ g\) which again follows directly by the universal property of \(\free{g}\).
\qedhere
\end{itemize}
\end{proof}
\end{proposition}

408
src/04_partiality-monads.tex
View file

@ -18,7 +18,7 @@ The first property of course holds for any commutative monad, the other two are
To ensure that programs are partial, we recall the following notion by Cockett and Lack~\cite{restriction}, that axiomatizes the notion of partiality in a category:
\newcommand{\tdom}{\text{dom}\;}
\begin{definition}[Restriction Structure]
\begin{definition}[Restriction Structure (\agdaref{Categories.Category.Restriction})]
A restriction structure on a category \(\C\) is a mapping \(dom : \C(X, Y) \rightarrow \C(X , X)\) with the following properties:
\begin{alignat*}{1}
f \circ (\tdom f) & = f \\
@ -40,7 +40,7 @@ The morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness
That is, \(\tdom f\) is only defined on values where \(f\) is defined and for those values it behaves like the identity function.
\begin{definition}[Restriction Category]
\begin{definition}[Restriction Category (\agdaref{Categories.Category.Restriction})]
Every category has a trivial restriction structure by taking \(dom (f : X \rightarrow Y) = id_X\).
We call categories with a non-trivial restriction structure \textit{restriction categories}.
\end{definition}
@ -49,7 +49,7 @@ For a suitable defined partiality monad \(T\) the Kleisli category \(\C^T\) shou
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:
\begin{definition}[Equational Lifting Monad]\label{def:eqlm}
\begin{definition}[Equational Lifting Monad (\agdaref{Monad.EquationalLifting})]\label{def:eqlm}
A commutative monad \(T\) is called an \textit{equational lifting monad} if the following diagram commutes:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ==
\[
@ -90,58 +90,11 @@ For the rest of this chapter we will use these definitions to compare two monads
\section{The Maybe Monad}
The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \rightarrow X + 1\) and \(\mu_X = [ id , i_2 ] : (X + 1) + 1 \rightarrow X + 1\).
The monad laws follow easily.
The monad laws follow easily (\agdaref{Monad.Instance.Maybe}).
This is generally known as the maybe monad and can be viewed as the canonical example of an equational lifting monad.
\begin{theorem} M is an equational lifting monad.
\begin{theorem}[\agdaref{Monad.Instance.Maybe.EquationalLifting}] M is an equational lifting monad.
\end{theorem}
\begin{proof}
We define strength as
\[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1. \]
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.
\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 thus 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}
\]
This is easily proven by pre-composing with \(i_1\) and \(i_2\), indeed
\begin{alignat*}{1}
& (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_1) \circ \langle i_1 , id \rangle
\\=\;&(id\;+\;!) \circ i_1 \circ \langle i_1 , id \rangle
\\=\;&i_1 \circ \langle i_1 , id \rangle,
\end{alignat*}
and
\begin{alignat*}{1}
& (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle
\\=\;&(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}
\end{alignat*}
\end{proof}
In the setting of classical mathematics this monad is therefore sufficient for modeling partiality, but in general it will not be useful for modeling non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modeling possibly non-terminating computations another monad has been introduced by Capretta~\cite{delay}.
@ -154,7 +107,7 @@ In this section we will show that these terminal coalgebras indeed yield a monad
Since \(DX\) is defined as a terminal 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\).
\begin{lemma}~\label{lem:delay}
\begin{lemma}[\agdaref{Monad.Instance.Delay}]~\label{lem:delay}
The following conditions hold:
\begin{itemize}
\item \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\) satisfy:
@ -176,82 +129,22 @@ Since \(DX\) is defined as a terminal coalgebra, we can define morphisms via cor
\end{equation*}
\item There exists a unique morphism \(\tau : X \times DY \rightarrow D(X \times Y)\) such that:
\begin{equation*}
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFsyLDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzIsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
\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)}
{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["{id \times out}", from=1-1, to=1-2]
\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]
\arrow["dstl", from=1-2, to=1-3]
\arrow["{id +\tau}"', from=1-3, to=2-3]
\arrow["out", from=2-1, to=2-3]
\end{tikzcd}
\tag*{(D3)}\label{D3}
\end{equation*}
\end{itemize}
\end{lemma}
\begin{proof}
We will make use of the fact that every \(DX\) is a terminal coalgebra:
\begin{itemize}
\item[\ref{D1}] These follow by definition of \(now\) and \(later\):
\begin{alignat*}{3}
& out \circ now & & = out \circ out^{-1} \circ i_1 & = i_1
\\&out \circ later &&= out \circ out^{-1} \circ i_2 &= i_2
\end{alignat*}
\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=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}
\]
Note that \(\coalg{\alpha} \circ i_2 = id : (DY, out) \rightarrow (DY, out)\), by uniqueness of the identity morphism and the fact that \(\coalg{\alpha} \circ i_2\) is a coalgebra morphism, since
\begin{alignat*}{1}
& out \circ \coalg{\alpha} \circ i_2
\\=\;&(id+\coalg{\alpha}) \circ \alpha \circ i_2
\\=\;&(id + \coalg{\alpha}) \circ (id + i_2) \circ out
\\=\;&(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.
\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\).
Note that \([ g , id ] : DX + DY \rightarrow DY\) is a coalgebra morphism, since
\begin{alignat*}{1}
& out \circ [ g , id ]
\\=\;&[ out \circ g , out ]
\\=\;&[ [ out \circ f , i_2 \circ g ] \circ out , out]
\\=\;&[ [ [ i_1 , i_2 ] \circ out \circ f , i_2 \circ g ] \circ out , (id + id) \circ out ]
\\=\;&[ [ [ 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 ].
\end{alignat*}
Thus, \([ g , id ] = \coalg{\alpha}\) by uniqueness of \(\coalg{\alpha}\).
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 \rightarrow D(X \times Y)\), the requisite property then follows by definition.
\qedhere
\end{itemize}
\end{proof}
\begin{lemma}
\begin{lemma}[\agdaref{Monad.Instance.Delay}]
The following properties of \(\mathbf{D}\) hold:
\begin{enumerate}
\item \(out \circ Df = (f + Df) \circ out\)
@ -259,178 +152,46 @@ Since \(DX\) is defined as a terminal coalgebra, we can define morphisms via cor
\item \(later \circ f^* = {(later \circ f)}^* = f^* \circ later\)
\end{enumerate}
\end{lemma}
\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}}
\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}}
\end{alignat*}
\item[3.]
This equational chain follows by monicity of \(out\):
\begin{alignat*}{1}
& out \circ {(later \circ f)}^*
\\=\;&[ out \circ later \circ f , i_2 \circ {(later \circ f)}^*] \circ out\tag*{\ref{D2}}
\\=\;&i_2 \circ [ f , {(later \circ f)}^*] \circ out\tag*{\ref{D1}}
\\=\;&i_2 \circ f^*
\\=\;&out \circ later \circ f^*\tag*{\ref{D1}}
\\=\;&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}}
\end{alignat*}
\end{itemize}
Thus, the postulated properties have been proven.
\end{proof}
\begin{lemma}
\begin{lemma}[\agdaref{Monad.Instance.Delay}]
\(\mathbf{D} := (D, now, {(-)}^*)\) is a Kleisli triple.
\end{lemma}
\begin{proof}
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}.
\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}
This concludes the proof.
\end{proof}
Terminality 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=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCJdXQ==
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFsxLDIsIm91dCJdLFswLDMsIlxcYWxwaGEiXSxbMCwxLCJmIl0sWzMsMiwiaWQgKyBmIl1d
\[
\begin{tikzcd}[ampersand replacement=\&]
X \&\& {Y + X} \&\& X \&\& {Y + X} \\
DY \&\& {Y + DY} \&\& DY \&\& {Y + DY}
\arrow["out", from=2-1, to=2-3]
\begin{tikzcd}
X && {Y + X} \\
DY && {Y + DY}
\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]
\arrow["out", from=2-1, to=2-3]
\end{tikzcd}
\]
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwwLCJZICsgWCJdLFsyLDEsIlkgKyBEWSJdLFswLDIsIlxcYWxwaGEiXSxbMCwxLCJnIl0sWzIsMywiaWQgKyBnIl0sWzEsMywib3V0Il1d
\[
\begin{tikzcd}
X && {Y + X} \\
DY && {Y + DY}
\arrow["\alpha", from=1-1, to=1-3]
\arrow["g", from=1-1, to=2-1]
\arrow["{id + g}", from=1-3, to=2-3]
\arrow["out", from=2-1, to=2-3]
\end{tikzcd}
\]
Uniqueness of the coalgebra morphism \(\coalg{\alpha} : (X, \alpha) \rightarrow (DY, out)\) then results in \(f = g\).
\end{remark}
\begin{lemma}
\begin{lemma}[\agdaref{Monad.Instance.Delay.Strong}]
\(\mathbf{D}\) is a strong monad.
\end{lemma}
\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
\[\tau \circ (f \times {(now \circ g)}^*) = {(now \circ (f \times g))}^* \circ \tau \]
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{\text{-}}}", dashed, from=1-1, to=3-1]
\arrow["{f \times g + id}", from=1-3, to=1-5]
\arrow["{id + \coalg{\text{-}}}", dashed, from=1-5, to=3-5]
\end{tikzcd}
\]
We write \(\coalg{\text{-}}\) to abbreviate the used coalgebra, i.e.\ in the previous diagram
\[\coalg{\text{-}} = \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=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{\text{-}}}", dashed, from=1-1, to=2-1]
\arrow["{id + \coalg{\text{-}}}", 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 will first need to establish
\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 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.
\end{alignat*}
\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=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{\text{-}}}", 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{\text{-}}}"', 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=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{\text{-}}}", dashed, from=1-1, to=3-1]
\arrow["out", from=3-1, to=3-3]
\arrow["{id +\coalg{\text{-}}}"', 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}
Thus, it has been shown that \(\mathbf{D}\) is a strong monad.
\end{proof}
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}
\begin{definition}[\agdaref{Monad.Instance.Delay}]
We call a morphism \(g : X \rightarrow D (Y + X)\) \textit{guarded} if there exists a morphism \(h : X \rightarrow Y + D(Y+X)\) such that the following diagram commutes:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
\[
@ -445,33 +206,14 @@ To prove that \(\mathbf{D}\) is commutative we will use another proof principle
\]
\end{definition}
\begin{corollary}[Solution Theorem]\label{cor:solution}
\begin{corollary}[Solution Theorem (\agdaref{Monad.Instance.Delay})]\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\).
\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 that
\[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i.\]
This is proven by coinduction using
% 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 + \coalg{\text{-}}}", from=1-4, to=2-4]
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
\end{tikzcd}
\]
which concludes the proof.
\end{proof}
Let us record some facts that we will use to prove commutativity of \(\mathbf{D}\):
\begin{corollary}
\begin{corollary}[\agdaref{Monad.Instance.Delay.Strong}, \agdaref{Monad.Instance.Delay.Commutative}]
These properties of \(\tau \) and \(\sigma \) hold:
\begin{alignat*}{2}
& out \circ \tau & & = (id + \tau) \circ dstl \circ (id \times out)\tag*{(\(\tau_1\))}\label{tau1}
@ -481,87 +223,9 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
\end{alignat*}
\end{corollary}
\begin{proof}
\begin{itemize}
\item[\ref{tau1}] This is just~\ref{D3} restated.
\item[\ref{sigma1}] Indeed, by use of~\ref{tau1}
\begin{alignat*}{1}
& out \circ \sigma
\\=\;&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}] By monicity of \(out\):
\begin{alignat*}{1}
& out \circ \tau \circ (id \times out^{-1})
\\=\;&(id + \tau) \circ dstl \circ (id \times out) \circ (id \times out^{-1})\tag*{\ref{tau1}}
\\=\;&(id + \tau) \circ dstl.
\end{alignat*}
\item[\ref{sigma2}] Again, by monicity of \(out\):
\begin{alignat*}{1}
& out \circ \sigma \circ (out^{-1} \times id)
\\=\;&(id + \sigma) \circ dstr \circ (out \times id) \circ (out^{-1} \times id)\tag*{\ref{sigma1}}
\\=\;&(id + \sigma) \circ dstr.\tag*{\qedhere}
\end{alignat*}
\end{itemize}
\end{proof}
\begin{theorem}
\begin{theorem}[\agdaref{Monad.Instance.Delay.Commutative}]
\(\mathbf{D}\) is commutative.
\end{theorem}
\begin{proof}
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.\]
Note that \(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\).
It thus suffices 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, \]
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\):
\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*}
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\), which yields
\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*{\ref{sigma1}}
\\=\;&[ (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*{\ref{sigma2}}
\\=\;&[ (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,
\end{alignat*}
where
\[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\]
indeed follows by epicness of \(dstr^{-1}\):
\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 ].\tag*{\qedhere}
\end{alignat*}
\end{proof}
We have now seen that \(\mathbf{D}\) is strong and commutative, however it is not an equational lifting monad, since besides modeling non-termination, the delay monad also counts the execution time of a computation.
This is a result of the too intensional notion of equality that this monad comes with.

836
src/05_iteration.tex
View file

@ -3,7 +3,7 @@ In this chapter we will draw on the inherent connection between partiality and i
\section{Elgot Algebras}
Recall the following notion from~\cite{elgotalgebras}, previously called \emph{complete Elgot algebra}.
\begin{definition}[Guarded Elgot Algebra]
\begin{definition}[Guarded Elgot Algebra (\agdaref{Algebra.Elgot})]
\ Given a functor \(H : \C \rightarrow \C\), a \emph{(H-)guarded Elgot algebra} consists of: % chktex 36
\begin{itemize}
\item An object \(A \in \obj{\C}\),
@ -24,7 +24,7 @@ Consider an Elgot algebra over the identity functor \(Id : \C \rightarrow \C\) t
The previous intuition gives rise to the following simpler definition that has been introduced in~\cite{uniformelgot}.
\begin{definition}[Elgot Algebra]
\begin{definition}[Elgot Algebra (\agdaref{Algebra.Elgot})]
A \emph{(unguarded) Elgot Algebra}~\cite{uniformelgot} consists of:
\begin{itemize}
\item An object \(A \in \obj{\C}\),
@ -46,7 +46,7 @@ However, we will omit these proofs in most parts of the thesis, since they mostl
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~\cite{uniformelgot}, which is partly illustrated by the following Lemma. % chktex 2
\begin{lemma}
\begin{lemma}[\agdaref{Algebra.Elgot}]
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional axioms
\begin{itemize}
@ -58,109 +58,12 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
\\ for any \(f : X \rightarrow A + (X + X)\).
\end{itemize}
\end{lemma}
\begin{proof} The proofs of the axioms build upon each other, we prove them one by one.
\begin{itemize}
\item \ref{law:compositionality}: First, note that \ref{law:folding} can equivalently be reformulated as % chktex 2
\begin{equation*}
{((f^\sharp + id) \circ h)}^\sharp = {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp \circ i_2, \tag{\textbf{Folding'}}\label{law:folding'}
\end{equation*}
since
\begin{alignat*}{1}
& {((f^\sharp + id) \circ h)}^\sharp
\\=\;&{(f^\sharp + h)}^\sharp \circ h\tag{\ref{law:uniformity}}
\\=\;&[f^\sharp , {(f^\sharp + h)}^\sharp \circ h ] \circ i_2
\\=\;&[ id , {(f^\sharp + h)}^\sharp ] \circ (f^\sharp + h) \circ i_2
\\=\;&{(f^\sharp + h)}^\sharp \circ i_2 \tag{\ref{law:fixpoint}}
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2. \tag{\ref{law:folding}}
\end{alignat*}
Using \ref{law:folding'}, it suffices to show that % chktex 2
\[{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2 = {([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2.\]
Indeed,
\begin{alignat*}{1}
& {[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ i_2
\\=\;&[ id , {[ (id + i_1) \circ f , i_2 \circ h]}^\sharp ] \circ [ (id + i_1) \circ f , i_2 \circ h] \circ i_2 \tag{\ref{law:fixpoint}}
\\=\;&[ id , {[ (id + i_1) \circ f , i_2 \circ h]}^\sharp ] i_2 \circ h
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp \circ h
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h]}^\sharp [ i_1 , h ] \circ i_2
\\=\;&{([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])}^\sharp \circ i_2.\tag{\ref{law:uniformity}}
\end{alignat*}
\item \ref{law:stutter}: Let us first establish % chktex 2
\begin{equation}
[ h , h ] = {(h + i_1)}^\sharp, \tag{*}\label{stutter-helper}
\end{equation}
which follows by
\begin{alignat*}{1}
& {(h + i_1)}^\sharp
\\=\;&[ id , {(h + i_1)}^\sharp ] \circ (h + i_1) \tag{\ref{law:fixpoint}}
\\=\;&[ h , {(h + i_1)}^\sharp \circ i_1 ]
\\=\;&[ h , [ id , {(h + i_1)}^\sharp ] \circ (h + i_1) \circ i_1 ] \tag{\ref{law:fixpoint}}
\\=\;&[ h , h ].
\end{alignat*}
Now we are done by
\begin{alignat*}{1}
& {([ h , h ] + id) \circ f}^\sharp
\\=\;&{({(h + i_1)}^\sharp + id) \circ f}^\sharp\tag{\ref{stutter-helper}}
\\=\;&{([(id + i_1) \circ (h + i_1) , i_2 \circ i_2] \circ [ i_1 , f])}^\sharp \circ i_2\tag{\ref{law:compositionality}}
\\=\;&{([h + i_1 \circ i_1 , i _2 \circ i_2] \circ [ i_1 , f])}^\sharp \circ (i_1 + id) \circ i_2
\\=\;&{[ i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] \circ f ]}^\sharp \circ i_2. \tag{\ref{law:uniformity}}
\end{alignat*}
\item \ref{law:diamond}: Let \(h = [ i_1 \circ i_1 , i_2 + id ] \circ f\) and \(g = (id + \Delta) \circ f\). %chktex 2
First, note that
\begin{equation*}
[ id , g^\sharp ] = {[ i_1 , (id + i_2) \circ g ]}^\sharp, \tag{\(∗\)}\label{diamond-helper}
\end{equation*}
by \ref{law:fixpoint} and \ref{law:uniformity}: % chktex 2
\begin{alignat*}{1}
& [ id , g^\sharp ]
\\=\;&[ id , [ id , g^\sharp ] \circ g ] \tag{\ref{law:fixpoint}}
\\=\;&[ id , [ id , {[ i_1 , (id + i_2) \circ g ]}^\sharp \circ i_2 ] \circ g ] \tag{\ref{law:uniformity}}
\\=\;&[ id , {[ i_1 , (id + i_2) \circ g ]}^\sharp ] \circ [ i_1 , (id + i_2) \circ g ]
\\=\;&{[ i_1 , (id + i_2) \circ g ]}^\sharp. \tag{\ref{law:fixpoint}}
\end{alignat*}
It thus suffices to show that,
\begin{alignat*}{1}
& g^\sharp
\\=\;&{[ (id + i_1) \circ [ i_1 , (id + i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2
\\=\;&{({[i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2\tag{\ref{law:folding}}
\\=\;&{([ i_1 , g^\sharp + id] \circ f)}^\sharp.
\end{alignat*}
Indeed,
\begin{alignat*}{1}
& g^\sharp
\\=\;&g^\sharp \circ [ id , id ] \circ i_2
\\=\;&{[ (id + i_2) \circ g , f ]}^\sharp \circ i_2\tag{\ref{law:uniformity}}
\\=\;&{(([ id , id ] + id) \circ [ (i_1 + i_1) \circ g , (i_2 + id) \circ f ]) }^\sharp \circ i_2
\\=\;&{[ i_1 , [ id + i_1 , i_2 \circ i_2 ] \circ [ (i_1 + i_1) \circ g , (i_2 + id) \circ f] ]}^\sharp \circ i_2 \circ i_2 \tag{\ref{law:stutter}}
\\=\;&{[ i_1 , [ [ i_1 , i_2 \circ i_2 \circ i_1 ] \circ g , [ i_2 \circ i_1 , i_2 \circ i_2 ] \circ f] ]}^\sharp \circ i_2 \circ i_2
\\=\;&{[ i_1 , [ ( id + i_2 \circ i_1) \circ g , i_2 \circ \circ f] ]}^\sharp \circ i_2 \circ i_2
\\=\;&{ [[ i_1 , (id + i_1 \circ i_2) \circ g ] , i_2 \circ h] }^\sharp \circ [ i_1 \circ i_1 , i_2 + id ] \circ i_2 \circ i_2\tag{\ref{law:uniformity}}
\\=\;&{ [[ i_1 , (id + i_1 \circ i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2
\\=\;&{ [(id + i_1) \circ [ i_1 , (id + i_2) \circ g ] , i_2 \circ h ]}^\sharp \circ i_2
\end{alignat*}
and
\begin{alignat*}{1}
& {([ i_1 , g^\sharp + id] \circ f)}^\sharp
\\=\;&{([i_1 \circ [id , g^\sharp] \circ i_1 , [ id , g^\sharp ] \circ i_2 + id ] \circ f)}^\sharp
\\=\;&{(([ id , g^\sharp ] + id) \circ h)}^\sharp
\\=\;&{(([[id , g^\sharp] , [id , g^\sharp] ] + id) \circ (i_2 + id) \circ h)}^\sharp
\\=\;&{[i_1 \circ [ id , g^\sharp ] , [ [id , g^\sharp] + i_1 , i_2 \circ i_2 ] \circ (i_2 + id) \circ h]}^\sharp \circ i_2 \tag{\ref{law:stutter}}
\\=\;&{([ id , g^\sharp ] + h)}^\sharp \circ i_2
\\=\;&{({[ i_1 , (id + i_2) \circ g ]}^\sharp + h)}^\sharp \circ i_2,\tag{\ref{diamond-helper}}
\end{alignat*}
which concludes the proof.
\qedhere
\end{itemize}
\end{proof}
Note that in~\cite{uniformelgot} it has been shown that the \ref{law:diamond} axiom implies \ref{law:compositionality}, yielding another definition of Elgot algebras only requiring the \ref{law:fixpoint}, \ref{law:uniformity} and \ref{law:diamond} axioms. % chktex 2
Let us now consider morphisms that are coherent with respect to the iteration operator. A special case being morphisms between Elgot algebras.
\begin{definition}[Iteration Preserving Morphisms]
\begin{definition}[Iteration Preserving Morphisms (\agdaref{Category.Construction.ElgotAlgebras})]
Let \((A, {(-)}^{\sharp_a}), (B, {(-)}^{\sharp_b})\) be two Elgot algebras.
A morphism \(f : X \times A \rightarrow B\) is called \textit{right iteration preserving} if
@ -179,187 +82,21 @@ Let us now consider morphisms that are coherent with respect to the iteration op
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}\label{lem:elgotalgscat}
\begin{lemma}[\agdaref{Category.Construction.ElgotAlgebras}]\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, B\) and \(C\) be Elgot algebras.
The identity trivially satisfies
\[id \circ f^{\sharp_a} = f^{\sharp_a} = {((id + id) \circ f)}^{\sharp_a}\]
for any \(f : X \rightarrow A + X\).
Given two iteration preserving morphisms \(f : B \hookrightarrow C, g : A \hookrightarrow B\), the composite is iteration preserving since
\begin{alignat*}{1}
& f \circ g \circ h^{\sharp_a}
\\=\;& f \circ {((g + id) \circ h)}^{\sharp_b}
\\=\;&{((f + id) \circ (g + id) \circ h)}^{\sharp_c}
\\=\;&{((f \circ g + id) \circ h)}^{\sharp_c}
\end{alignat*}
for any \(h : X \rightarrow A + X\).
\end{proof}
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:elgotalgscart}
\begin{lemma}[\agdaref{Category.Construction.ElgotAlgebras.Products}]\label{lem:elgotalgscart}
If \(\C\) is a Cartesian category, so is \(\elgotalgs{\C}\).
\end{lemma}
\begin{proof}
Let \(1\) be the terminal object of \(\C \). Given \(f : X \rightarrow 1 + X\) we define the iteration \(f^\sharp =\;! : X \rightarrow 1\) as the unique morphism into the terminal object. The Elgot algebra laws follow instantly by uniqueness of \(!\) and \((1 , !)\) is the terminal Elgot algebra since for every Elgot algebra \(A\) the morphism \(! : A \rightarrow 1\) extends to a morphism between Elgot algebras by uniqueness. % chktex 40
Let \(A, 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}\):
\begin{alignat*}{1}
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle
\\=\;&\langle [ id , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ (\pi_1 + id) \circ f
\\ &, [ id , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \circ (\pi_2 + id) \circ f \rangle \tag{\ref{law:fixpoint}}
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ f , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \circ f \rangle
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \rangle \circ f
\\=\;&[ \langle \pi_1 , \pi_2 \rangle , \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle ] \circ f
\\=\;&[ id , \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle ] \circ f
\end{alignat*}
\item \textbf{Uniformity}: Let \(f : X \rightarrow (A \times B) + X, g : Y \rightarrow (A \times B) + Y, h : X \rightarrow Y\) and \((id + h) \circ f = g \circ h\).
Note that this implies:
\begin{alignat*}{2}
& (id + h) \circ (\pi_1 + id) \circ f & & = (\pi_1 + id) \circ g \circ h
\\&(id + h) \circ (\pi_2 + id) \circ f &&= (\pi_2 + id) \circ g \circ h
\end{alignat*}
Then,~\ref{law:uniformity} of \({(-)}^{\sharp_a}\) and \({(-)}^{\sharp_b}\) with the previous two equations yields:
\begin{alignat*}{2}
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_1 + id) \circ f)}^{\sharp_a} \rangle & & = {((\pi_1 + id) \circ g)}^{\sharp_a} \circ h
\\&\langle {((\pi_2 + id) \circ f)}^{\sharp_b} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle &&= {((\pi_2 + id) \circ g)}^{\sharp_b} \circ h
\end{alignat*}
This concludes the proof of:
\[ \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle = \langle {((\pi_1 + id) \circ g)}^{\sharp_a} , {((\pi_2 + id) \circ g)}^{\sharp_b} \rangle \circ h \]
\item \textbf{Folding}: Let \(f : X \rightarrow (A \times B) + X, h : Y \rightarrow X + Y\). We need to show:
\begin{alignat*}{1}
& \langle {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_a}
\\&,{((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_b} \rangle
\\=\;&\langle (\pi_1 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_a} , (\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_b} \rangle
\end{alignat*}
Indeed, the folding laws for \({(-)}^{\sharp_a}\) and \({(-)}^{\sharp_b}\) imply
\begin{alignat*}{1}
& {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_a}
\\=\;&{({((\pi_1 + id) \circ f)}^{\sharp_a} + h)}^{\sharp_a}
\\=\;&{[ (id + i_1) \circ (\pi_1 + id) \circ f , i_2 \circ h ]}^{\sharp_a}\tag{\ref{law:folding}}
\\=\;&(\pi_1 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_a}
\end{alignat*}
and
\begin{alignat*}{1}
& {((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_b}
\\=\;&{({((\pi_2 + id) \circ f)}^{\sharp_b} + h)}^{\sharp_b}
\\=\;&{[ (id + i_1) \circ (\pi_2 + id) \circ f , i_2 \circ h ]}^{\sharp_b}\tag{\ref{law:folding}}
\\=\;&(\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_b}
\end{alignat*}
which concludes the proof of the folding law.
\end{itemize}
The product diagram of \(A \times B\) in \(\C\) then also holds in \(\elgotalgs{\C}\), we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism \(\langle f , g \rangle\) is iteration preserving for any \(f : C \hookrightarrow A, g : C \rightarrow B\) where \(C \in \obj{\elgotalgs{\C}}\).
Let \(h : X \rightarrow C + X\). We use the fact that \(f\) and \(g\) are iteration preserving to show:
\begin{alignat*}{1}
& \langle f , g \rangle \circ (h^{\sharp_c})
\\=\;&\langle f \circ (h^{\sharp_c}) , g \circ (h^{\sharp_c}) \rangle
\\=\;&\langle {((f + id) \circ h)}^{\sharp_a} , {((g + id) \circ h)}^{\sharp_b} \rangle
\\=\;&\langle {((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_a} , {((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_b} \rangle
\end{alignat*}
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, 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}
\begin{lemma}[\agdaref{Category.Construction.ElgotAlgebras.Exponentials}]\label{lem:elgotexp}
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\).
\begin{itemize}
\item \textbf{Fixpoint}: Let \(f : Y \rightarrow X^A + Y\). We need to show that \(f^\sharp = [ id , f^\sharp ] \circ f\), which follows by uniqueness of \[f^\sharp = curry\;({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a})\] and
\begin{alignat*}{1}
& eval \circ ([ id , curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ f \times id)
\\=\;&eval \circ [ id , curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr \circ (f \times id)\tag*{\ref{hlp:elgot_exp_fixpoint}}
\\=\;&[ eval , eval \circ (curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr \circ (f \times id)
\\=\;&[ eval , {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} ] \circ dstr \circ (f \times id)
\\=\;&[ id , {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} ] \circ (eval + id) \circ dstr \circ (f \times id)
\\=\;&{((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a},\tag{\ref{law:fixpoint}}
\end{alignat*}
where
\begin{alignat*}{1}
& [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \times id
\\= \;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr \tag*{(*)}\label{hlp:elgot_exp_fixpoint}
\end{alignat*}
follows by post-composing with \(\pi_1\) and \(\pi_2\), indeed:
\begin{alignat*}{1}
& \pi_1 \circ [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr
\\=\;&[ \pi_1 , \pi_1 \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr
\\=\;&[ \pi_1 , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \circ \pi_1 ] \circ dstr
\\=\;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ (\pi_1 + \pi_1) \circ dstr
\\=\;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ \pi_1,
\end{alignat*}
and
\begin{alignat*}{1}
& \pi_2 \circ [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr
\\=\;&[ \pi_2 , \pi_2 \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr
\\=\;&[ \pi_2 , \pi_2 ] \circ dstr
\\=\;&\pi_2.
\end{alignat*}
\item \textbf{Uniformity}: Let \(f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z\) and \((id + h) \circ f = g \circ h\). Again, by uniqueness of \(f^\sharp = curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a})\) it suffices to show:
\begin{alignat*}{1}
& {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}
\\=\;&{((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \circ (h \times id)\tag{\ref{law:uniformity}}
\\=\;&eval \circ ({((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \times id) \circ (h \times id)
\\=\;&eval \circ ({((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \circ h \times id).
\end{alignat*}
Note that the application of \ref{law:uniformity} requires: % chktex 2
\begin{alignat*}{1}
& (id + (h \times id)) \circ (eval + id) \circ dstr \circ (f \times id)
\\=\;&(eval + id) \circ (id + (h \times id)) \circ dstr \circ (f \times id)
\\=\;&(eval + id) \circ dstr \circ (id \times h) \circ (id \times id) \circ (f \times id)
\\=\;&(eval + id) \circ dstr \circ (g \times id) \circ (h \times id).
\end{alignat*}
\item \textbf{Folding}: Let \(f : Y \rightarrow X^A + Y, h : Y \rightarrow Z\). We need to show that
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp
\\=\;&curry({((eval + id) \circ dstr \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) + h) \times id))}^{\sharp_a})
\\=\;&curry({((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))}^{\sharp_a})
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp.
\end{alignat*}
Indeed, we are done by
\begin{alignat*}{1}
& {((eval + id) \circ dstr \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) + h) \times id))}^{\sharp_a}
\\=\;&{((eval + id) \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) + (h \times id)) \circ dstr)}^{\sharp_a}
\\=\;&{((eval \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) + (h \times id)) \circ dstr)}^{\sharp_a}
\\=\;&{(({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} + (h \times id)) \circ dstr)}^{\sharp_a}
\\=\;&{(({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} + dstr \circ (h \times id)))}^{\sharp_a} \circ dstr\tag{\ref{law:uniformity}}
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr\tag{\ref{law:folding}}
\\=\;&{((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))}^{\sharp_a},\tag{\ref{law:uniformity}}
\end{alignat*}
where the identity that is required for the second application of~\ref{law:uniformity} follows by epicness of \(dstr^{-1}\).
\qedhere
% \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)
% \\&, (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_2 \times id) ]
% \\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ (((id + i_1) \circ f) \times id)
% \\&, (id + dstr) \circ (eval + id) \circ dstr \circ ((i_2 \circ h) \times id) ]
% \\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ((id + i_1) \times id) \circ (f \times id)
% \\&, (id + dstr) \circ (eval + id) \circ dstr \circ (i_2 \times id) \circ (h \times id) ]
% \\=\;&[ (id + dstr) \circ (eval + id) \circ (id + (i_1 \times id)) \circ dstr \circ (f \times id)
% \\&, (id + dstr) \circ (eval + id) \circ i_2 \circ (h \times id) ]
% \\=\;&[ (eval + i_1) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ]
% \\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr \circ dstr^{-1}.\tag*{\qedhere}
% \end{alignat*}
\end{itemize}
\end{proof}
\section{The Initial (Strong) Pre-Elgot Monad}
\section{The Initial Pre-Elgot Monad}
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial 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}.
@ -385,7 +122,7 @@ Let us first recall the following notion that was introduced in~\cite{elgotmonad
We regard Elgot monads as minimal semantic structures for interpreting side-effecting while loops, as has been argued in~\cite{goncharov2018unguarded, goncharov2017unifying}.
The following notion has been introduced in~\cite{uniformelgot} as a weaker approximation of the notion of Elgot monad, using less sophisticated axioms.
\begin{definition}[Pre-Elgot Monad]
\begin{definition}[Pre-Elgot Monad (\agdaref{Monad.PreElgot})]
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 the monad \(\mathbf{T}\) is additionally strong and the strength \(\tau \) is right iteration preserving we call \(\mathbf{T}\) strong pre-Elgot.
@ -393,26 +130,20 @@ The following notion has been introduced in~\cite{uniformelgot} as a weaker appr
(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.
\begin{lemma}
\begin{lemma}[\agdaref{Category.Construction.PreElgotMonads}, \agdaref{Category.Construction.StrongPreElgotMonads}]
\(\preelgot{\C}\) and \(\strongpreelgot{\C}\) are categories.
\end{lemma}
\begin{proof}
Since \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) are subcategories of the previously defined categories \(\monads{\C}\) and \(\strongmonads{\C}\) respectively, it suffices to show that the components of the identity natural transformation are iteration preserving and that the component wise composition of two pre-Elgot monad morphisms is iteration preserving. This has already been shown in \autoref{lem:elgotalgscat}.
\end{proof}
Assuming a form of the axiom of countable choice it has been proven in~\cite{uniformelgot} that the initial pre-Elgot monad and the initial Elgot monad coincide, thus closing the expressivity gap in such a setting.
However, it is believed to be impossible to close this gap in a general setting.
\begin{proposition}
\begin{proposition}[\agdaref{Monad.Instance.K}]
Existence of all free Elgot algebras yields a monad that we call \(\mathbf{K}\).
\end{proposition}
\begin{proof}
This is a direct consequence of \autoref{thm:freemonad}.
\end{proof}
We will need a notion of stability for \(\mathbf{K}\) to make progress, since we do not assume \(\C \) to be Cartesian closed.
\begin{definition}[Right-Stable Free Elgot Algebra]\label{def:rightstablefreeelgot}
\begin{definition}[Right-Stable Free Elgot Algebra (\agdaref{Algebra.Elgot.Stable}, \agdaref{Algebra.Elgot.Free})]\label{def:rightstablefreeelgot}
Let \(KY\) be a free Elgot algebra on \(Y \in \obj{\C}\). We call \(KY\) \textit{right-stable} if for every \(A \in \elgotalgs{\C}, X \in \obj{\C}\), and \(f : X \times Y \rightarrow A\) there exists a unique right iteration preserving \(\rs{f} : X \times KY \rightarrow A\) such that
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIFxcdGltZXMgWSJdLFsyLDAsIkEiXSxbMCwyLCJYIFxcdGltZXMgS1kiXSxbMCwxLCJmIl0sWzAsMiwiaWRcXHRpbWVzXFxldGEiLDJdLFsyLDEsIlxccnN7Zn0iLDJdXQ==
\[
@ -430,7 +161,7 @@ We will need a notion of stability for \(\mathbf{K}\) to make progress, since we
A symmetrical variant of the previous definition is sometimes useful.
\begin{definition}[Left-Stable Free Elgot Algebra]\label{def:leftstablefreeelgot}
\begin{definition}[Left-Stable Free Elgot Algebra (\agdaref{Algebra.Elgot.Stable}, \agdaref{Algebra.Elgot.Free})]\label{def:leftstablefreeelgot}
Let \(KY\) be a free Elgot algebra on \(Y \in \obj{\C}\). We call \(KY\) \textit{left-stable} if for every \(A \in \elgotalgs{\C}, X \in \obj{\C}\), and \(f : Y \times X \rightarrow A\) there exists a unique left iteration preserving \(\ls{f} : KY \times X \rightarrow A\) such that
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIFxcdGltZXMgWSJdLFsyLDAsIkEiXSxbMCwyLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJmIl0sWzAsMiwiXFxldGFcXHRpbWVzIGlkIiwyXSxbMiwxLCJcXGxze2Z9IiwyXV0=
\[
@ -446,120 +177,17 @@ A symmetrical variant of the previous definition is sometimes useful.
commutes.
\end{definition}
\begin{lemma}
\begin{lemma}[\agdaref{Algebra.Elgot.Stable}]
Definitions~\ref{def:rightstablefreeelgot} and~\ref{def:leftstablefreeelgot} are equivalent in the sense that they imply each other.
\end{lemma}
\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)
\\=\;&\ls{f \circ swap} \circ swap \circ (id \times h^\sharp)
\\=\;&\ls{f \circ swap} \circ (h^\sharp \times id) \circ swap
\\=\;&{((\ls{f \circ swap} + id) \circ dstr \circ (id \times h))}^\sharp \circ swap
\\=\;&{((\ls{f \circ swap} \circ swap + id) \circ dstl \circ (id \times h))}^\sharp\tag{\ref{law:uniformity}}
\\=\;&{((\rs{f} + id) \circ dstl \circ (id \times h))}^\sharp,
\end{alignat*}
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
% Where the application of \ref{law:uniformity} is justified by
% \begin{alignat*}{1}
% &(id + swap) \circ ((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h)
% \\=\;&((\ls{f \circ swap} \circ swap) + swap) \circ dstl \circ (id \times h)
% \\=\;&(\ls{f \circ swap} + id) \circ (swap + swap) \circ dstl \circ (id \times h)
% \\=\;&(\ls{f \circ swap} + id) \circ dstr \circ swap \circ (id \times h)
% \\=\;&(\ls{f \circ swap} + id) \circ dstr \circ (h \times id) \circ swap.
% \end{alignat*}
The requisite diagram commutes, since
\begin{alignat*}{1}
& \rs{f} \circ (id \times \eta)
\\=\;&\ls{f \circ swap} \circ swap \circ (id \times \eta)
\\=\;&\ls{f \circ swap} \circ (\eta \times id) \circ swap
\\=\;&f \circ swap \circ swap
\\=\;&f.
\end{alignat*}
Finally, let us check uniqueness of \(\rs{f} = \ls{f \circ swap} \circ swap\). Let \(g : X \times KY \rightarrow A\) be right iteration preserving with \(g \circ (id \times \eta) = f\). To show that \(g = \ls{f \circ swap} \circ swap\), by uniqueness of \(\ls{f \circ swap}\) it suffices to show that \(g \circ swap\) satisfies \(g \circ swap \circ (\eta \times id) = f \circ swap\) and is left iteration preserving.
Indeed,
\[ g \circ swap \circ (\eta \times id) = g \circ (id \times \eta) \circ swap = f \circ swap\]
and
\begin{alignat*}{1}
& g \circ swap \circ (h^\sharp \times id)
\\=\;&g \circ (id \times h^\sharp) \circ swap
\\=\;&{((g + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
\\=\;&{((g \circ swap + id) \circ dstr \circ (h \times id))}^\sharp,\tag{\ref{law:uniformity}}
\end{alignat*}
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
% The application of \ref{law:uniformity} is justified by
% \begin{alignat*}{1}
% &(id + swap) \circ ((g \circ swap) + id) \circ dstr \circ (h \times id)
% \\=\;&(g + id) \circ (swap + swap) \circ dstr \circ (h \times id)
% \\=\;&(g + id) \circ dstl \circ swap \circ (h \times id)
% \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap.
% \end{alignat*}
This concludes one direction of the proof, the other direction follows symmetrically.
\end{proof}
\begin{lemma}\label{thm:stability}
\begin{lemma}[\agdaref{Algebra.Elgot.Properties}]\label{thm:stability}
In a Cartesian closed category every free Elgot algebra is stable.
\end{lemma}
\begin{proof}
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\).
We will now verify that this does indeed satisfy the requisite properties, i.e.
\begin{alignat*}{1}
& eval \circ (\free{curry\;f} \times id) \circ (\eta \times id)
\\=\;&eval \circ (\free{curry\;f} \circ \eta \times id)
\\=\;&eval \circ (curry\;f \times id)
\\=\;&f
\end{alignat*}
and for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\):
\begin{alignat*}{1}
& eval \circ (\free{curry\;f} \times id) \circ (h^\sharp \times id)
\\=\;&eval \circ (\free{curry\;f} \circ h^\sharp \times id)
\\=\;&eval \circ (curry({((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))}^\sharp) \times id)
\\=\;&{((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \circ h \times id))}^\sharp
\\=\;&{((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))}^\sharp
\\=\;&{((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))}^\sharp
\\=\;&{((eval \circ (\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))}^\sharp.
\end{alignat*}
Lastly, we need to check uniqueness of \(\ls{f}\). Let us consider a left iteration preserving morphism \(g : KY \times X \rightarrow A\) that satisfies \(g \circ (\eta \times id) = f\). Since \(curry\) is an injective mapping it suffices to show that
\begin{alignat*}{1}
& curry\;\ls{f}
\\=\;&curry(eval \circ (\free{curry\;f} \times id))
\\=\;&\free{curry\;f}
\\=\;&curry\;g.
\end{alignat*}
Where the last step is the only non-trivial one. Since \(\free{curry\;f}\) is a unique iteration preserving morphism satisfying \(\free{curry\;f} \circ \eta = curry\;f\), we are left to show that \(g\) is also iteration preserving and satisfies the same property.
Indeed,
\begin{alignat*}{1}
& curry\;g \circ h^\sharp
\\=\;&curry\;(g \circ (h^\sharp \times id))
\\=\;&curry\;({((g + id) \circ dstr \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval \circ (curry\; g \times id) + id) \circ dstr \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))}^\sharp)
\\=\;&curry\;({((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))}^\sharp)
\end{alignat*}
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\), and
\begin{alignat*}{1}
& curry\;g \circ \eta
\\=\;&curry(g \circ (\eta \times id))
\\=\;&curry\;f.
\end{alignat*}
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.
Let us first introduce a proof principle similar to the one introduced in \autoref{rem:coinduction}.
\begin{remark}[Proof by right-stability]~\label{rem:proofbystability}
\begin{remark}[Proof by right-stability (\agdaref{Monad.Instance.K})]~\label{rem:proofbystability}
Given two morphisms \(g, h : X \times KY \rightarrow A\) where \(X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}\). To show that \(g = h\), it suffices to show that \(g\) and \(h\) are right iteration preserving and there exists a morphism \(f : X \times Y \rightarrow A\) such that
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJBIl0sWzAsMiwiWCBcXHRpbWVzIFkiXSxbMCwxLCJnIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImgiLDIseyJvZmZzZXQiOjF9XSxbMiwxLCJmIiwyXSxbMiwwLCJpZCBcXHRpbWVzIFxcZXRhIl1d
\[
@ -576,7 +204,7 @@ Let us first introduce a proof principle similar to the one introduced in \autor
commutes.
\end{remark}
Of course there is also a symmetric version of this.
\begin{remark}[Proof by left-stability]~\label{rem:proofbyleftstability}
\begin{remark}[Proof by left-stability (\agdaref{Monad.Instance.K})]~\label{rem:proofbyleftstability}
Given two morphisms \(g, h : KX \times Y \rightarrow A\) where \(X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}\). To show that \(g = h\), it suffices to show that \(g\) and \(h\) are left iteration preserving and there exists a morphism \(f : X \times Y \rightarrow A\) such that
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJLWCBcXHRpbWVzIFkiXSxbMiwwLCJBIl0sWzAsMiwiWCBcXHRpbWVzIFkiXSxbMCwxLCJnIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImgiLDIseyJvZmZzZXQiOjF9XSxbMiwxLCJmIiwyXSxbMiwwLCJcXGV0YSBcXHRpbWVzIGlkIl1d
\[
@ -593,448 +221,34 @@ Of course there is also a symmetric version of this.
commutes.
\end{remark}
\begin{lemma}\label{lem:Kstrong}
\begin{lemma}[\agdaref{Monad.Instance.K.Strong}]\label{lem:Kstrong}
\(\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 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 using \autoref{rem:proofbystability}, i.e.\ to prove an identity we need to give a unifying morphism such that the requisite diagram commutes, and we need to show that both sides of the identity are right iteration preserving. The proofs of commutativity follow by easy rewriting and are thus deferred to the formalization. The proofs of right iteration preservation follow in most cases instantly since the morphisms are composed of (right) iteration preserving morphisms but in non-trivial cases we will give the full proof.
Naturality of \(\tau \) follows by:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
\[
\begin{tikzcd}
& {A \times KB} && {X \times KY} \\
\\
& {K(A \times B)} && {K(X \times Y)} \\
{A \times B}
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
\arrow["\tau"', from=1-2, to=3-2]
\arrow["{K(f\times g)}"', from=3-2, to=3-4]
\arrow["{f \times Kg}", from=1-2, to=1-4]
\arrow["\tau", from=1-4, to=3-4]
\arrow["{\eta \circ (f \times g)}"', curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}
\]
Notably, \(\tau \circ (f \times Kg)\) is right iteration preserving, since for any \(Z \in \obj{\C}\) and \(h : Z \rightarrow KY + Z\):
\begin{alignat*}{1}
& \tau \circ (f \times Kg) \circ (id \times h^\sharp)
\\=\;&\tau \circ (f \times {((Kg + id) \circ h)}^\sharp)
\\=\;&{((\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)))}^\sharp \circ (f \times id)
\\=\;&{(((\tau \circ (f \times Kg)) + id) \circ dstl \circ (id \times h))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
% where uniformity is justified by
% \begin{alignat*}{1}
% &(id + (f \times id)) \circ \tau \circ ((f \times Kg) + id) \circ dstl \circ (id \times h)
% \\=\;&(\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)) \circ (f \times id)
% \end{alignat*}
% Both sides of the identity are right iteration preserving, since for any \(Z \in \obj{\C}\) and \(h : Z \rightarrow KY + Z\):
% \begin{alignat*}{1}
% &K(f \times g) \circ \tau \circ (id \times h^\sharp)
% \\=\;&K(f \times g) \circ ((\tau + id) \circ dstl \circ (id \times h))^\sharp
% \\=\;&(((K(f \times g) \circ \tau) + id) \circ dstl \circ (id \times h))^\sharp
% \end{alignat*}
% and
% \begin{alignat*}{1}
% &\tau \circ (f \times Kg) \circ (id \times h^\sharp)
% \\=\;&\tau \circ (f \times (Kg \circ h)^\sharp)
% \\=\;&
% \end{alignat*}
Let us now check the strength laws.
\begin{itemize}
\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\), which is proven by right-stability, using:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
\[
\begin{tikzcd}
{X \times KY} && {K(X\times Y)} \\
\\
{X \times Y} && KY
\arrow["\tau", from=1-1, to=1-3]
\arrow["{K\pi_2}", from=1-3, to=3-3]
\arrow["{\pi_2}"', from=1-1, to=3-3]
\arrow["{id \times \eta}"', from=3-1, to=1-1]
\arrow["{\eta \circ \pi_2}"', from=3-1, to=3-3]
\end{tikzcd}
\]
\item[\ref{S2}] As already mentioned, \(\tau \circ (id \times \eta) = \eta\) follows by definition of \(\tau\).
\item[\ref{S3}] To show that \(\tau \circ (id \times \mu) = \tau^* \circ \tau\), we will proceed by right-stability using:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS0tZIl0sWzMsMCwiWCBcXHRpbWVzIEtZIl0sWzMsMiwiSyhYXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFswLDMsIlggXFx0aW1lcyBLWSJdLFswLDEsImlkIFxcdGltZXMgXFxtdSIsMl0sWzEsMiwiXFx0YXUiLDJdLFswLDMsIlxcdGF1Il0sWzMsMiwiXFx0YXVeKiJdLFs0LDAsImlkIFxcdGltZXMgXFxldGEiLDAseyJjdXJ2ZSI6LTJ9XSxbNCwyLCJcXHRhdSIsMCx7ImN1cnZlIjoyfV1d
\[
\begin{tikzcd}
& {X \times KKY} && {X \times KY} \\
\\
& {K(X \times KY)} && {K(X\times Y)} \\
{X \times KY}
\arrow["{id \times \mu}"', from=1-2, to=1-4]
\arrow["\tau"', from=1-4, to=3-4]
\arrow["\tau", from=1-2, to=3-2]
\arrow["{\tau^*}", from=3-2, to=3-4]
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
\arrow["\tau", curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}
\]
\item[\ref{S4}] Lastly, consider the following diagram for the proof by right-stability:
% https://q.uiver.app/#q=WzAsNixbMSwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgS1oiXSxbMSwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIEtZIl0sWzMsMCwiSygoWCBcXHRpbWVzIFkpIFxcdGltZXMgWikiXSxbMywyLCJLKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgSyhZIFxcdGltZXMgWikiXSxbMCwzLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgWiJdLFswLDEsIlxcYWxwaGEiXSxbMiwzLCJLXFxhbHBoYSJdLFswLDIsIlxcdGF1Il0sWzEsNCwiaWQgXFx0aW1lc1xcdGF1Il0sWzQsMywiXFx0YXUiXSxbNSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzUsMywiXFxldGEgXFxjaXJjIFxcYWxwaGEiLDIseyJjdXJ2ZSI6Mn1dXQ==
\[
\begin{tikzcd}
& {(X \times Y) \times KZ} && {K((X \times Y) \times Z)} \\
\\
& {X \times Y \times KY} & {X \times K(Y \times Z)} & {K(X \times Y \times Z)} \\
{(X \times Y) \times Z}
\arrow["\alpha", from=1-2, to=3-2]
\arrow["K\alpha", from=1-4, to=3-4]
\arrow["\tau", from=1-2, to=1-4]
\arrow["{id \times\tau}", from=3-2, to=3-3]
\arrow["\tau", from=3-3, to=3-4]
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
\arrow["{\eta \circ \alpha}"', curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}
\]
where \(\tau \circ (id \times \tau) \circ \alpha \) is right iteration preserving, since for any \(Z \in \obj{\C}\) and \(h : Z \rightarrow KX + Z\):
\begin{alignat*}{1}
& \tau \circ (id \times \tau) \circ \alpha \circ (id \times h^\sharp)
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle \circ (id \times h^\sharp)
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , h^\sharp \circ \pi_2 \rangle \rangle
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ (id \times h^\sharp) \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , {((\tau + id) \circ dstl \circ (id \times h))}^\sharp \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
\\=\;&\tau \circ (id \times {((\tau + id) \circ dstl \circ (id \times h))}^\sharp) \circ \alpha
\\=\;&{((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))}^\sharp \circ \alpha
\\=\;&{(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
\end{itemize}
Thus, strength of \(\mathbf{K}\) has been proven.
\end{proof}
As we did when proving commutativity of \(\mathbf{D}\), let us record some facts about \(\tau \) and the induced \(\sigma \), before proving commutativity of \(\mathbf{K}\).
\begin{corollary}
\(\sigma \) is left iteration preserving and satisfies \(\sigma \circ (\eta \times id) = \eta \) and the following properties of \(\tau \) and \(\sigma \) hold.
\begin{corollary}[\agdaref{Monad.Instance.K.Commutative}]
\(\sigma\) is left iteration preserving and satisfies \(\sigma \circ (\eta \times id) = \eta \) and the following properties of \(\tau \) and \(\sigma \) hold.
\begin{alignat*}{2}
& \tau \circ (f^* \times g^*) & & = {(\tau \circ (id \times g))}^* \circ \tau \circ (f^* \times id)\tag{\(\tau_1\)}\label{Ktau1}
\\&\sigma \circ (f^* \times g^*) &&= {(\sigma \circ (f \times id))}^* \circ \sigma \circ (id \times g^*)\tag{\(\sigma_1\)}\label{Ksigma1}
\end{alignat*}
\end{corollary}
\begin{proof}
Note that the first part of the proof amounts to showing that \(\sigma = \ls{\eta}\) using uniqueness of \(\ls{\eta}\). Indeed,
\begin{alignat*}{1}
& \sigma \circ (\eta \times id)
\\=\;&Kswap \circ \tau \circ swap \circ (\eta \times id)
\\=\;&Kswap \circ \tau \circ (id \times \eta) \circ swap
\\=\;&Kswap \circ \eta \circ swap
\\=\;&\eta \circ swap \circ swap
\\=\;&\eta
\end{alignat*}
and for any \(h : Z \rightarrow KX + Z\)
\begin{alignat*}{1}
& \sigma \circ (h^\sharp \times id)
\\=\;&Kswap \circ \tau \circ swap \circ (h^\sharp \times id)
\\=\;&Kswap \circ \tau \circ (id \times h^\sharp) \circ swap
\\=\;&Kswap \circ {((\tau + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
\\=\;&{(((Kswap \circ \tau) + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
\\=\;&{((\sigma + id) \circ dstr \circ (h \times id))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
Let us now proceed with the properties of \(\tau \) and \(\sigma \).
\begin{itemize}
\item[(\ref{Ktau1})]
\begin{alignat*}{1}
& {(\tau \circ (id \times g))}^* \circ \tau \circ (f^* \times id)
\\=\;&\tau^* \circ K(id \times g) \circ \tau \circ (f^* \times id)
\\=\;&\tau^* \circ \tau \circ (id \times Kg) \circ (f^* \times id)
\\=\;&\tau \circ (id \times \mu) \circ (id \times Kg) \circ (f^* \times id)
\\=\;&\tau \circ (id \times g^*) \circ (f^* \times id)
\\=\;&\tau \circ (f^* \times g^*)
\end{alignat*}
\item[(\ref{Ksigma1})]
\begin{alignat*}{1}
& {(\sigma \circ (f \times id))}^* \circ \sigma \circ (id \times g^*)
\\=\;&\sigma^* \circ K(f \times id) \circ \sigma \circ (id \times g^*)
\\=\;&\sigma^* \circ \sigma \circ (Kf \times id) \circ (id \times g^*)
\\=\;&\sigma \circ (\mu \times id) \circ (Kf \times id) \circ (id \times g^*)
\\=\;&\sigma \circ (f^* \times id) \circ (id \times g^*)
\\=\;&\sigma \circ (f^* \times g^*)
\end{alignat*}
\end{itemize}
Thus, the proof has been concluded.
\end{proof}
The following Lemma is central to the proof of commutativity.
\begin{lemma}\label{lem:KCommKey} Given \(f : X \rightarrow KY + X, g : Z \rightarrow KA + Z\),
\begin{lemma}[\agdaref{Monad.Instance.K.Commutative}]\label{lem:KCommKey} Given \(f : X \rightarrow KY + X, g : Z \rightarrow KA + Z\),
\[\tau^* \circ \sigma \circ ({((\eta + id) \circ f)}^\sharp \times {((\eta + id) \circ g)}^\sharp) = \sigma^* \circ \tau \circ ({((\eta + id) \circ f)}^\sharp \times {((\eta + id) \circ g)}^\sharp).\]
\end{lemma}
\begin{proof}
Let us abbreviate \(\hat{f} := (\eta + id) \circ f\) and \(\hat{g} := (\eta + id) \circ g\). It suffices to find a
\[w : X \times Z \rightarrow K(X \times KA + KY \times Z) + X \times Z\]
such that \(\hat{f}^\sharp \circ \pi_1 = {[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \circ w^\sharp\) and \(\hat{g}^\sharp \circ \pi_2 = {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^* \circ w^\sharp \), because then
\begin{alignat*}{1}
& \tau^* \circ \sigma \circ (\hat{f}^\sharp \times \hat{g}^\sharp)
\\=\;&\tau^* \circ \sigma \circ ({[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ (w^\sharp \times w^\sharp)
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ \sigma \circ (id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ (w^\sharp \times w^\sharp)
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ \sigma \circ (w^\sharp \times w^\sharp)
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ Kswap \circ \tau \circ \Delta \circ w^\sharp
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^*
\\&\hphantom{\tau^* }\circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ Kswap \circ K\langle \eta , id \rangle \circ w^\sharp\tag{\autoref{thm:Klifting}}
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ K\langle id , \eta \rangle \circ w^\sharp
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K\langle id , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle \circ w^\sharp
\\=\;&\tau^* \circ {(\sigma \circ \langle[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle)}^* \circ w^\sharp
\\=\;&\tau^* \circ {(\sigma \circ [\langle \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_2 \rangle , \langle \eta \circ \pi_1 , \hat{g}^\sharp \circ \pi_2 \rangle])}^* \circ w^\sharp
\\=\;&{(\tau^* \circ \sigma \circ [\hat{f}^\sharp \times \eta , \eta \times \hat{g}^\sharp])}^* \circ w^\sharp
\\=\;&{([\tau^* \circ \sigma \circ (\hat{f}^\sharp \times \eta) , \tau^* \circ \sigma \circ (\eta \times \hat{g}^\sharp)])}^* \circ w^\sharp
\\=\;&{([\tau^* \circ K(id \times \eta) \circ \sigma \circ (\hat{f}^\sharp \times id) , \tau^* \circ \eta \circ (id \times \hat{g}^\sharp)])}^* \circ w^\sharp
\\=\;&{([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ (id \times \hat{g}^\sharp)])}^* \circ w^\sharp,
\end{alignat*}
and by a symmetric argument also
\[\sigma^* \circ \tau \circ (\hat{f}^\sharp \times \hat{g}^\sharp) = {([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ (id \times \hat{g}^\sharp)])}^* \circ w^\sharp.\]
Note that we are referencing the equational lifting law established in \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, since we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity, this does not pose a problem.
We are thus left to find such a \(w\), consider
\[w := [ i_1 \circ K i_1 \circ \tau , ((K i_2 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}). \]
\(w\) indeed satisfies the requisite properties, let us check the first property, the second one follows by a symmetric argument. We need to show that
\[{[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \circ w^\sharp = {([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))}^\sharp = \hat{f}^\sharp \circ \pi_1. \]
Indeed,
\begin{alignat*}{1}
& {[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \circ w^\sharp
\\=\;&{(({[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* + id) \circ w)}^\sharp
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}))}^\sharp
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times (\eta + id)) \circ (id \times g))}^\sharp
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ ((id \times \eta) + id) \circ dstl \circ (id \times g))}^\sharp
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau \circ (id \times \eta) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp
\\=\;&{([ i_1 \circ \hat{f}^\sharp \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \hat{f} \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp\tag{\ref{law:fixpoint}}
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 \circ (\hat{f} \times id) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ ((\hat{f} \times id) + (\hat{f} \times id)) \circ dstl \circ (id \times g))}^\sharp
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))}^\sharp
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) \circ dstr , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))}^\sharp
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ (dstr + dstr) \circ dstl \circ (\hat{f} \times g))}^\sharp
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ [ i_1 + i_1 , i_2 + i_2 ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
\\=\;&{([ [ i_1 \circ [id , \hat{f}^\sharp] \circ i_1 \circ \pi_1 , i_1 \circ K\pi_1 \circ \sigma ] , [ i_1 \circ [id , \hat{f}^\sharp] \circ i_2 \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
\\=\;&{([ [ i_1 \circ \pi_1 , i_1 \circ \pi_1 ] , [ i_1 \circ \hat{f}^\sharp \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
\\=\;&{([ i_1 \circ [ \pi_1 , \pi_1 ] , (\hat{f}^\sharp \circ \pi_1 + id) ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
\\=\;&{([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))}^\sharp
\end{alignat*}
and
\begin{alignat*}{1}
& \hat{f}^\sharp \circ \pi_1
\\=\;&{((id + \Delta) \circ h)}^\sharp \tag{\ref{law:uniformity}}
\\=\;&{([ i_1 , {((id + \Delta) \circ h)}^\sharp + id] \circ h)}^\sharp \tag{\ref{law:diamond}}
\\=\;&{([ i_1 , (\hat{f}^\sharp \circ \pi_1) + id ] \circ h)}^\sharp \tag{\ref{law:uniformity}}
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1 \circ \pi_1) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))}^\sharp
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ ((\pi_1 \times id) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))}^\sharp
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ \langle \pi_1 , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))}^\sharp
\\=\;&{([ i_1 \circ \pi_1 \circ (id \times g) , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ (id \times g) ] \circ dstr \circ (\hat{f} \times id))}^\sharp
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))}^\sharp,
\end{alignat*}
where \(h = (\pi_1 + (\pi_1 + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle) \circ dstr \circ (\hat{f} \times id)\) and the application of \ref{law:uniformity} is justified, since % 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)
\\=\;&(\pi_1 + ([ \pi_1 \circ \pi_1 , \pi_1 \circ \pi_1 ] \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
\\=\;&(\pi_1 + (\pi_1 \circ \pi_1 \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
\\=\;&(\pi_1 + \pi_1) \circ dstr \circ (\hat{f} \times id)
\\=\;&\pi_1 \circ (\hat{f} \times id)
\\=\;&\hat{f} \circ \pi_1 .
\end{alignat*}
This concludes the proof.
\end{proof}
\begin{lemma}
\begin{lemma}[\agdaref{Monad.Instance.K.Commutative}]
\(\mathbf{K}\) is a commutative monad.
\end{lemma}
\begin{proof} We need to show that \(\tau^* \circ \sigma = \sigma^* \circ \tau : KX \times KY \rightarrow K(X \times Y)\).
Let us proceed by right stability, consider the following diagram.
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJLWCBcXHRpbWVzIEtZIl0sWzMsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzEsMiwiSyhYIFxcdGltZXMgS1kpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMCwzLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdSJdLFswLDIsIlxcaGF0e1xcdGF1fSIsMl0sWzEsMywiXFxoYXR7XFx0YXV9XioiXSxbMiwzLCJcXHRhdV4qIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMywiXFxoYXR7XFx0YXV9IiwyLHsiY3VydmUiOjJ9XV0=
\[
\begin{tikzcd}
& {KX \times KY} && {K(KX \times Y)} \\
\\
& {K(X \times KY)} && {K(X \times Y)} \\
{KX \times Y}
\arrow["\tau", from=1-2, to=1-4]
\arrow["{\sigma}"', from=1-2, to=3-2]
\arrow["{\sigma^*}", from=1-4, to=3-4]
\arrow["{\tau^*}"', from=3-2, to=3-4]
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
\arrow["{\sigma}"', curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}
\]
The diagram commutes since
\[\sigma^* \circ \tau \circ (id \times \eta) = \sigma^* \circ \eta = \sigma \]
and
\[\tau^* \circ \sigma \circ (id \times \eta) = \tau^* \circ K(id \times \eta) \circ \sigma = {(\tau \circ (id \times \eta))}^* \circ \sigma = \sigma.\]
We are left to show that both \(\sigma^* \circ \tau \) and \(\tau^* \circ \sigma \) are right iteration preserving. Let \(h : Z \rightarrow KY + Z\), indeed
\[\sigma^* \circ \tau \circ (id \times h^\sharp) = \sigma^* {((\tau + id) \circ dstl \circ (id \times h))}^\sharp = {(((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))}^\sharp. \]
Let \(\psi := \tau^* \circ \sigma \) and let us proceed by left stability to show that \(\psi \) is right iteration preserving, consider the following diagram
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
\[
\begin{tikzcd}
&&&& {KX \times KY} \\
{KX \times Z} &&&& {K(X \times Y)} \\
\\
{X \times Z}
\arrow["\psi", from=1-5, to=2-5]
\arrow["{id \times h^\sharp}", from=2-1, to=1-5]
\arrow["{((\psi + id) \circ dstl \circ (id \times h))^\sharp}"', from=2-1, to=2-5]
\arrow["{\eta \times id}", from=4-1, to=2-1]
\arrow["{\tau \circ (id \times h^\sharp)}"', from=4-1, to=2-5]
\end{tikzcd}
\]
which commutes, since
\begin{alignat*}{1}
& \psi \circ (id \times h^\sharp) \circ (\eta \times id)
\\=\;&\psi \circ (\eta \times id) \circ (id \times h^\sharp)
\\=\;&\tau^* \circ \eta \circ (id \times h^\sharp)
\\=\;&\tau \circ (id \times h^\sharp)
\\=\;&{((\tau + id) \circ dstl \circ (id \times h))}^\sharp
\\=\;&{((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (\eta \times id).\tag{\ref{law:uniformity}}
\end{alignat*}
We are left to show that both \(\psi \circ (id \times h^\sharp)\) and \({((\psi + id) \circ dstl \circ (id \times h))}^\sharp \) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi \circ (id \times h^\sharp)\) is left iteration preserving, since
\begin{alignat*}{1}
& \psi \circ (id \times h^\sharp) \circ (g^\sharp \times id)
\\=\;&\psi \circ (g^\sharp \times id) \circ (id \times h^\sharp)
\\=\;&\tau^* \circ {((\sigma + id) \circ dstr \circ (g \times id))}^\sharp \circ (id \times h^\sharp)
\\=\;&{((\psi + id) \circ dstr \circ (g \times id))}^\sharp \circ (id \times h^\sharp)
\\=\;&{(((\psi \circ (id \times h^\sharp)) + id) \circ dstr \circ (g \times id))}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
Lastly, we need to show that
\[{((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (g^\sharp \times id) = {(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp.\]
Note that by~\ref{law:uniformity} the left-hand side can be rewritten as
\[{(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp.\]
Consider now, that
\begin{alignat*}{1}
& {(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{(({({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ {((\eta + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ {(((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))}^\sharp
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&{({((\psi^* + id) \circ (\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({((\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({((\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({(((\tau \circ (id \times \eta)) + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {({((\tau + id) \circ dstl \circ (id \times ((\eta + id) \circ h)))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ {(\tau \circ (id \times {((\eta + id) \circ h)}^\sharp))}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ K(id \times {((\eta + id) \circ h)}^\sharp) \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times {((\eta + id) \circ h)}^\sharp) \circ ({((\eta + id) \circ g)}^\sharp \times id)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp),
\end{alignat*}
and by a symmetric argument
\begin{alignat*}{1}
& {(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp).
\end{alignat*}
We are thus done by
\begin{alignat*}{1}
& {((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (g^\sharp \times id)
\\=\;&{(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp\tag{\ref{law:uniformity}}
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp)
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp)\tag{\autoref{lem:KCommKey}}
\\=\;&{(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp.\tag*{\qedhere}
\end{alignat*}
\end{proof}
\begin{theorem}\label{thm:Klifting}
\begin{theorem}[\agdaref{Monad.Instance.K.EquationalLifting}]\label{thm:Klifting}
\(\mathbf{K}\) is an equational lifting monad.
\end{theorem}
\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:
\begin{alignat*}{1}
& \tau \circ \Delta \circ \eta
\\=\;&\tau \circ \langle \eta , \eta \rangle
\\=\;&\tau \circ (id \times \eta) \circ \langle \eta , id \rangle
\\=\;&\eta \circ \langle \eta , id \rangle.
\end{alignat*}
For iteration preservation of \(\tau \circ \Delta \) consider \(Z \in \obj{\C}\) and \(h : Z \rightarrow KX + Z\), then
\begin{alignat*}{1}
& \tau \circ \Delta \circ h^{\sharp}
\\=\;&\tau \circ \langle h^{\sharp} , h^{\sharp} \rangle
\\=\;&\tau \circ (id \times h^{\sharp}) \circ \langle h^{\sharp} , id \rangle
\\=\;&{((\tau + id) \circ dstl \circ (id \times f))}^\sharp \circ \langle h^{\sharp} , id \rangle
\\=\;&{(((\tau \circ \Delta) + id) \circ f)}^\sharp.\tag{\ref{law:uniformity}}
\end{alignat*}
Note that by monicity of \(dstl^{-1}\) and by~\ref{law:fixpoint}
\[(\Delta + \langle f^\sharp , id \rangle) \circ f = dstl \circ \langle f^\sharp , f \rangle.\tag{*}\label{helperinkey} \]
The application of~\ref{law:uniformity} is then justified by
\begin{alignat*}{1}
& (id + \langle f^\sharp , id \rangle) \circ ((\tau \circ \Delta) + id) \circ f
\\=\;&((\tau \circ \Delta) + \langle f^\sharp , id \rangle) \circ f
\\=\;&(\tau + id) \circ (\Delta + \langle f^\sharp , id \rangle) \circ f
\\=\;&(\tau + id) \circ dstl \circ \langle f^\sharp , f \rangle\tag{\ref{helperinkey}}
\\=\;&(\tau + id) \circ dstl \circ (id \times f) \circ \langle f^\sharp , id \rangle.\tag*{\qedhere}
\end{alignat*}
\end{proof}
\begin{theorem}
\begin{theorem}[\agdaref{Monad.Instance.K.PreElgot},\agdaref{Monad.Instance.K.StrongPreElgot}]
\(\mathbf{K}\) is the initial (strong) pre-Elgot monad.
\end{theorem}
\begin{proof}
Note that \(\mathbf{K}\) is a pre-Elgot monad by definition and strong pre-Elgot by \autoref{lem:Kstrong}. Let us first show that \(\mathbf{K}\) is the initial pre-Elgot monad.
Given any pre-Elgot monad \(\mathbf{T}\), let us introduce alternative names for the monad operations of \(\mathbf{T}\) and \(\mathbf{K}\) to avoid confusion:
\[\mathbf{T} = (T , \eta^T, \mu^T)\]
and
\[\mathbf{K} = (K , \eta^K, \mu^T).\]
For every \(X \in \obj{\C} \) we define \(¡ = \free{(\eta^T : X \rightarrow TX)} : KX \rightarrow TX \). Note that \(¡\) is per definition the unique iteration preserving morphism that satisfies \(¡ \circ \eta^K = \eta^T\). We are done after showing that \(¡\) is natural and respects the monad multiplication.
Let \(f : X \rightarrow Y\). For naturality of \(¡\) it suffices to show
\[¡ \circ Kf = \free{Tf \circ \eta^T} = Tf \circ ¡,\]
where \(\free{Tf \circ \eta^T}\) is the unique Elgot algebra morphism satisfying \(\free{Tf \circ \eta^T} \circ \eta^K = Tf \circ \eta^T \).
Note that both \(¡ \circ Kf \) and \(Tf \circ ¡ \) are iteration preserving since they are composed of iteration preserving morphisms and both satisfy the requisite property, since \(Tf \circ ¡ \circ \eta^K = Tf \circ \eta^T \) follows instantly and
\begin{alignat*}{1}
& ¡ \circ Kf \circ \eta^K
\\=\;&¡ \circ \eta^K \circ f
\\=\;&\eta^T \circ f
\\=\;&Tf \circ \eta^T.
\end{alignat*}
Let us proceed similarly for showing that \(¡\) respects the monad multiplication, i.e.\ consider
\[¡ \circ \mu = \free{¡} = \mu^T \circ T ¡ \circ ¡,\]
where \(\free{¡}\) is the unique Elgot algebra morphism satisfying \(\free{¡} \circ \eta^K = ¡\). Note that again both sides of the identity are iteration preserving, since they are composed of iteration preserving morphisms. Consider also that \(¡ \circ \mu^K \circ \eta^K = ¡\) and
\begin{alignat*}{1}
& \mu^T \circ T¡ \circ ¡ \circ \eta^K
\\=\;&\mu^T \circ ¡ \circ K¡ \circ \eta^K
\\=\;&\mu^T \circ ¡ \circ \eta^K \circ ¡
\\=\;&\mu^T \circ \eta^T \circ ¡
\\=\;&¡.
\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) \). We proceed by right-stability, using:
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS1kiXSxbMywwLCJLKFggXFx0aW1lcyBZKSJdLFszLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzEsMiwiWCBcXHRpbWVzIFRZIl0sWzAsMywiWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdV5LIl0sWzEsMiwiwqEiXSxbMCwzLCJpZCBcXHRpbWVzIMKhIiwyXSxbMywyLCJcXHRhdV5UIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMiwiXFxldGFeVCIsMix7ImN1cnZlIjoyfV1d
\[
\begin{tikzcd}[ampersand replacement=\&]
\& {X \times KY} \&\& {K(X \times Y)} \\
\\
\& {X \times TY} \&\& {T(X \times Y)} \\
{X \times Y}
\arrow["{\tau^K}", from=1-2, to=1-4]
\arrow["{¡}", from=1-4, to=3-4]
\arrow["{id \times ¡}"', from=1-2, to=3-2]
\arrow["{\tau^T}"', from=3-2, to=3-4]
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
\arrow["{\eta^T}"', curve={height=12pt}, from=4-1, to=3-4]
\end{tikzcd}
\]
The diagram commutes, since \( ¡ \circ \tau^K = \eta^T = \tau^T \circ (id \times \eta^T) = \tau^T \circ (id \times ¡) \circ (id \times \eta^T) \). Now we are done, since \(¡ \circ \tau^K\) and \(\tau^T \circ (id \times ¡)\) are both right iteration preserving because both are composed of (right) iteration preserving morphisms.
\end{proof}
\end{theorem}

450
src/06_setoids.tex
View file

@ -7,13 +7,13 @@ In this chapter we will use the quotients-as-setoid approach, i.e.\ we will work
\section{Setoids in Type Theory}
We will now introduce the category that the rest of the chapter will take place in. Let us start with some basic definitions.
\begin{definition}[Setoid]
\begin{definition}[Setoid (\agdaref{Relation.Binary.Bundles})]
A setoid is a tuple \((A, \overset{A}{=})\) where \(A\) (usually called the \textit{carrier}) is a type and \(\overset{A}{=}\) is an equivalence relation on the inhabitants of \(A\).
\end{definition}
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 Morphism]
\begin{definition}[Setoid Morphism (\agdaref{Function.Bundles})]
A morphism between setoids \(A\) and \(B\) constitutes 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 morphisms as \(A ⇝ B\).
\end{definition}
Let us now consider the function space setoid, which is of special interest, since it carries a notion of equality between functions.
@ -24,91 +24,13 @@ Let us now consider the function space setoid, which is of special interest, sin
Setoids together with setoid morphisms 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.
\begin{proposition}
\begin{proposition}[\agdaref{Category.Ambient.Setoids}]
\(\setoids\) is a distributive category.
\end{proposition}
\begin{proof}
To show that \(\setoids\) is (co)Cartesian we will give the respective data types and unique functions. % chktex 36
For brevity, we will omit the proofs that the functions respect the corresponding equivalences, these are however included in the Agda standard library~\cite{agda-stdlib}.
\begin{itemize}
\item \textbf{Products}:
\begin{minted}{agda}
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
constructor _,_
field
fst : A
snd : B
<_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (A → B) → (A → C) → A → (B × C)
< f , g > x = (f x , g x)
\end{minted}
The product setoid is denoted \((A \times B, \overset{\times}{=})\) or just \(A \times B\). Equality of products is defined in the canonical way.
\item \textbf{Terminal Object}:
\begin{minted}{agda}
record ⊤ {l} : Set l where
constructor tt
! : ∀ {l} {X : Set l} → X → ⊤ {l}
! _ = tt
\end{minted}
The terminal setoid is thus \((\top, \overset{\top}{=})\), where \(\top \overset{\top}{=} \top\).
\item \textbf{Coproducts}:
\begin{minted}{agda}
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
i₁ : A → A + B
i₂ : B → A + B
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (A → C) → (B → C) → (A + B) → C
[ f , g ] (i₁ x) = f x
[ f , g ] (i₂ x) = g x
\end{minted}
Similarly to products, the coproduct setoid is denoted \((A + B, \overset{+}{=})\) or just \(A + B\), where equality of coproducts is defined in the canonical way.
\item \textbf{Initial Object}:
\begin{minted}{agda}
data ⊥ {l} : Set l where
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
¡ ()
\end{minted}
The initial setoid is then \((\bot, \emptyset)\), where the equivalence is the empty relation.
\end{itemize}
Lastly we need to show that the canonical distributivity function is an iso. Recall that the canonical distributivity morphism is defined as \(dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)\).
This is equivalent to the following definition that uses pattern matching.
\begin{minted}{agda}
distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (A × B) + (A × C) → A × (B + C)
distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
\end{minted}
The inverse can then be defined similarly:
\begin{minted}{agda}
distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ A × (B + C) → (A × B) + (A × C)
distributeˡ (x , i₁ y) = i₁ (x , y)
distributeˡ (x , i₂ y) = i₂ (x , y)
\end{minted}
Note that these functions are inverse by definition, and it follows quickly that they are setoid morphisms.
\end{proof}
\begin{proposition}\label{prop:setoids-ccc}
\begin{proposition}[\agdaref{Categories.Category.Instance.Properties.Setoids.CCC}]\label{prop:setoids-ccc}
\(\setoids\) is Cartesian closed.
\end{proposition}
\begin{proof}
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
curry f x y = f (x , y)
eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
eval (f , x) = f x
\end{minted}
The universal property of exponential objects follows instantly.
\end{proof}
\section{Quotienting the Delay Monad}
In this section we will introduce data types only using inference rules. For that we adopt the convention that coinductive types are introduced by doubled lines while inductive types are introduced with a single line.
@ -127,7 +49,7 @@ Let \(A\) be a setoid. Lifting the equivalence \(\overset{A}{=}\) to \(D\;A\) yi
\inferrule*{x \sim y}{later\; x \sim later\; y} \qquad
\]
\begin{proposition}[\cite{quotienting}]
\begin{proposition}[\cite{quotienting} (\agdaref{Monad.Instance.Setoids.Delay})]
\((D\;A, \sim)\) is a setoid and admits a monad structure.
\end{proposition}
@ -144,378 +66,24 @@ Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \ap
\inferrule*{x \approx y}{later \;x \approx later \;y} \qquad
\]
\begin{proposition}[\cite{delay}]
\begin{proposition}[\cite{delay} (\agdaref{Monad.Instance.Setoids.Delay})]
\((D\;A, \approx)\) is a setoid and admits a monad structure.
\end{proposition}
\begin{proof}
The monad unit is the constructor \(now : A \rightarrow D\;A\) and the multiplication \(\mu : D\;D\;A \rightarrow D\;A\) can be defined as follows:
\[\mu\;x = \begin{cases}
z & \text{if } x = now\;z \\
later(\mu\;z) & \text{if } x = later\;z
\end{cases}\]
Given a function \(f : A \rightarrow B\), the lifted function \(Df : D\;A \rightarrow D\;B\) is defined as
\[Df\;x = \begin{cases}
now(f\;z) & \text{if } x = now\;z \\
later(Df\;z) & \text{if } x = later\;z
\end{cases}\]
It has been shown in~\cite{delay} that this indeed extends to a monad.
\end{proof}
For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\) and \(\dbtilde{D}\;A = (D_A, \approx)\).
\begin{lemma}\label{lem:Delgot}
\begin{lemma}[\agdaref{Monad.Instance.Setoids.K}]\label{lem:Delgot}
Every \(\dbtilde{D}\;A\) can be equipped with an Elgot algebra structure.
\end{lemma}
\begin{proof}
We need to show that for every setoid \(A\) the resulting setoid \(\dbtilde{D}\;A\) extends to an Elgot algebra.
Let \(X\) be a setoid and \(f : X ⇝ \dbtilde{D}\;A + X\) be a setoid morphism, we define \(f^\sharp : X ⇝ \dbtilde{D}\;A\) point wise:
\[
f^\sharp\;x :=
\begin{cases}
a & \text{if } f\;x = i_1 (a) \\
later\;(f^{\sharp}\;a) & \text{if } f\;x = i_2 (a)
\end{cases}
\]
Let us first verify that \(f^\sharp\) is indeed a setoid morphism, i.e.\ given \(x, y : X\) with \(x \overset{X}{=} y\), we need to show that \(f^\sharp\;x \approx f^\sharp\;y\). Since \(f\) is a setoid morphism we know that \(f\;x \overset{+}{=} f\;y\), which already implies that \(f^\sharp\;x \approx f^\sharp\;y\) by the definition of \(f^\sharp\). Note that by the same argument we can define an iteration operator that respects strong bisimilarity, let us call it \(f^{\tilde{\sharp}}\) as we will later need to distinguish between \(f^\sharp\) and \(f^{\tilde{\sharp}}\).
Next, we check the iteration laws:
\begin{itemize}
\item \ref{law:fixpoint}: We need to show that \(f^\sharp \;x \approx [ id , f^\sharp ](f\;x)\) for any \(x : X\). Let us proceed by case distinction: % chktex 2
\begin{mycase}
\case{} \(f\;x = i_1\;a\)
\[ f^\sharp\;x \approx a \approx [ id , f^\sharp ] (i_1\;a) \approx [ id , f^\sharp ] (f\;x) \]
\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 ⇝ \dbtilde{D}\;A + Y, h : X ⇝ Y\) be setoid morphisms, 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,
\[f^\sharp\; x \approx a \approx b \approx g^\sharp (h\;x)\]
\case{} \(f\;x = i_2\;a\) and \(g (h\;x) = i_2\;b\)\\
Note that \((id + h) \circ f \doteq g \circ h\) on \(x\) yields \(i_2(h\;a) \overset{+}{=} i_2\;b\) and thus \(h\;a \overset{Y}{=} b\).
We are done by coinduction, which yields
\[f^\sharp\;x \approx later(f^\sharp\;a) \approx later(g^\sharp(h\;a)) \approx later(g^\sharp\;b) \approx g^\sharp (h\;x).\]
\end{mycase}
\item \ref{law:folding}: Let \(Y\) be a setoid and \(h : Y ⇝ X + Y\) a setoid morphism, 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:
\begin{mycase}
\case{} \(f\;c = i_1\;a\)
\[f^\sharp\;c \approx a \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c)\]
\case{} \(f\;c = i_2\;a\)
\[f^\sharp\;c \approx later(f^\sharp\;a) \approx later({[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a)) \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c)\]
\end{mycase}
We will now proceed with the proof of \ref{law:folding}, by case distinction on \(z\): % chktex 2
\begin{mycase}
\case{} \(z = i_1\;x\)\\
Another case distinction on \(f\;x\) yields:
\subcase{} \(f\;x = i_1\;a\)\\
We are done, since \({(f^\sharp + h)}^\sharp(i_1 \; x) \approx a \approx {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x)\)
\subcase{} \(f\;x = i_2\;a\)\\
Now, using the fact we established prior
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_1 \; x)
\\\approx\;&later(f^\sharp\;a)
\\\approx\;&later({[(id + i_1) \circ f , i_2 \circ h]}^\sharp (i_1\;a))\tag{\ref{folding-helper}}
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;x).
\end{alignat*}
\case{} \(z = i_2\;y\)\\
Let us proceed by discriminating on \(h\;y\).
\subcase{} \(h\;y = i_1\;a\)\\
Indeed by coinduction,
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_2 \; y)
\\\approx\;&later((f^\sharp + h)(i_1\;a))
\\\approx\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;a))
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\end{alignat*}
\subcase{} \(h\;y = i_2\;a\)\\
Similarly by coinduction,
\begin{alignat*}{1}
& {(f^\sharp + h)}^\sharp(i_2 \; y)
\\\approx\;&later((f^\sharp + h)(i_2\;a))
\\\approx\;&later({[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;a))
\\\approx\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_2\;y)
\end{alignat*}
\end{mycase}
\end{itemize}
This concludes the proof that every \(\dbtilde{D}\;A\) extends to an Elgot algebra.
\end{proof}
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}
\begin{corollary}[\agdaref{Monad.Instance.Setoids.K}]\label{cor:discretize}
Given a setoid morphism \(g : X ⇝ \dbtilde{D}\;A + X\), there exists a setoid morphism \(\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 morphism that behaves as \(g\) does but with a different type profile.
The requisite property follows by case distinction on \(g\;x\).
\begin{mycase}
\case{} \(g\;x = i_1\;a\)\\
We are done, since \(g^\sharp\;x \sim a \sim \bar{g}^{\tilde{\sharp}}\;x\)
\case{} \(g\;x = i_2\;a\)\\
By coinduction \(g^\sharp\;x \sim later(g^\sharp\;a) \sim later(\bar{g}^{\tilde{\sharp}}\;a) \sim \bar{g}^{\tilde{\sharp}}\;x\), which concludes the proof.
\qedhere
\end{mycase}
\end{proof}
\begin{theorem}\label{thm:Dfreeelgot}
\begin{theorem}[\agdaref{Monad.Instance.Setoids.K}]\label{thm:Dfreeelgot}
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 morphism \(now : A ⇝ \dbtilde{D}\;A\) is a free such algebra.
Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid morphism \(f : A ⇝ B\). We need to define an Elgot algebra morphism \(\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 ⇝ 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 morphism \(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
\[g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\]
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid morphism \(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)
\\\overset{B}{=}\;&g^{\sharp_b} (\bar{h}^{\tilde{\sharp}}\;x)\tag{\autoref{cor:discretize}}
\\\overset{B}{=}\;&(g^{\sharp_b} \circ [ id , \bar{h}^{\tilde{\sharp}}])(i_2\;x)
\\\overset{B}{=}\;&{([(id + i_1) \circ g , i_2 \circ i_2 ] \circ [i_1 , h])}^{\sharp_b} (i_2\;x)\tag{\ref{law:uniformity}}
\\\overset{B}{=}\;&{((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\tag{\ref{law:compositionality}}
\end{alignat*}
Thus, \(g^{\sharp_b}\) is an Elgot algebra morphism. 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 morphisms \(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 extends to the following conversion setoid morphism \(conv : \tilde{D}\;A ⇝ \dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid morphism \(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{\(∗\)}\label{uniq-helper}\]
Let us now return to the proof of uniqueness. We proceed by
\begin{alignat*}{1}
& e\;x
\\\approx\;&e({((conv + id) \circ o)}^\sharp\;x)\tag{\ref{uniq-helper}}
\\\approx\;&{((e \circ conv + id) \circ o)}^{\sharp_b}\;x\tag{Preservation}
\\\approx\;&{((h \circ conv + id) \circ o)}^{\sharp_b}\;x
\\\approx\;&h({((conv + id) \circ o)}^\sharp\;x)\tag{Preservation}
\\\approx\;&h\;x.\tag{\ref{uniq-helper}}
\end{alignat*}
It thus suffices to show that \((e \circ conv + id)(o\;x) \approx (h \circ conv + id)(o\;x)\). Indeed, discriminating over \(x\) yields:
\begin{mycase}
\case{} \(x = now\;z\)
\begin{alignat*}{1}
& (e \circ conv + id)(o(now\;z))
\\\overset{+}{=}\;&(e \circ conv + id)(i_1(now\;z))
\\\overset{+}{=}\;&e(now\;z)
\\\overset{+}{=}\;&f\;z
\\\overset{+}{=}\;&h(now\;z)
\\\overset{+}{=}\;&(h \circ conv + id)(i_1(now\;z))
\\\overset{+}{=}\;&(h \circ conv + id)(o(now\;z))
\end{alignat*}
\case{} \(x = later\;z\)
\begin{alignat*}{1}
& (e \circ conv + id)(o(later\;z))
\\\overset{+}{=}\;&(e \circ conv + id)(i_2\;z)
\\\overset{+}{=}\;&i_2\;z
\\\overset{+}{=}\;&(h \circ conv + id)(i_2\;z)
\\\overset{+}{=}\;&(h \circ conv + id)(o(later\;z))
\end{alignat*}
\end{mycase}
It has thus been proven that every \(\dbtilde{D}\;A\) admits a free Elgot algebra structure.
\end{proof}
Let us now establish some functions for inspecting and manipulating the computation of elements of \(D\;A\). These functions and some key facts will then be used to finish the remaining proof needed for \autoref{thm:Dfreeelgot}.
First, consider the ordering with respect to execution time on elements of \(D\;A\), defined by
\[
\mprset{fraction={===}}\inferrule*{p: x \downarrow a}{now_\lesssim\;p : now\;a \lesssim x} \qquad
\inferrule*{p : x \lesssim y}{later_\lesssim\;p : later\;x \lesssim later\;y}.
\]
Note that \(x \lesssim y\) implies \(x \approx y\) for any \(x, y : D\;A\), which follows easily by coinduction.
Now, consider the following function \(race : D\;A \rightarrow D\;A \rightarrow D\;A\) which tries running two computations and returns the one that finished first:
\[race\;p\;q := \begin{cases}
now\;a & \text{if } p = now\;a \\
now\;b & \text{if } p = later\;a \text{ and } q = now\;b \\
later\;(race\;a\;b) & \text{if } p = later\;a \text{ and } q = later\;b
\end{cases}\]
The following Corollary, whose proof can be found in the formalization, will be needed.
\begin{corollary}\label{cor:race}
\(race\) satisfies the following properties:
\begin{alignat*}{3}
& x \approx y & & \text{ implies } race\;x\;y \sim race\;y\;x & \text{for any } x, y : D\;A
\\ &x \approx y && \text{ implies } race\;x\;y \lesssim y & \text{ for any } x, y : D\;A.
\end{alignat*}
\end{corollary}
Next, let us consider functions for counting steps of computations, first regard \(\Delta_0 : (x : D\;A) \rightarrow (a : A) \rightarrow (x \downarrow a) \rightarrow \mathbb{N}\), which returns the number of steps a terminating computation has to take and is defined by
\[\Delta_0\;x\;a\;p := \begin{cases}
0 & \text{if } x = now\;y \\
(\Delta_0\; y\;a\;q) + 1 & \text{if } x = later\;y \text{ and } p = later_\downarrow q
\end{cases}\]
Similarly, consider \(\Delta : (x, y : D\;A) \rightarrow x \lesssim y \rightarrow D(A \times \mathbb{N})\) defined by
\[\Delta\;x\;y\;p := \begin{cases}
now(a , \Delta_0\;x\;a\;q) & \text{if } x = now\;a \text{ and } p = now_\lesssim q \\
later(\Delta\;a\;b\;q) & \text{if } x = later\;a, y = later\;b \text{ and } p = later_\lesssim q
\end{cases}\]
Lastly, consider the function \(\iota : A \times \mathbb{N} \rightarrow D\;A\), which adds a number of \(later\) constructors in front of a value and is given by
\[\iota\;(a, n) := \begin{cases}
now\;x & \text{if } n = 0 \\
later(\iota\;(a, m)) & \text{if } n = m + 1
\end{cases}\]
Trivially, \(\iota\) extends to a setoid morphism \(\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:
\begin{alignat*}{4}
& p : x \lesssim y & & \text{ implies } \tilde{D}(fst (\Delta\;x\;y\;p))\; & \sim x & & \text{ for any } x, y : D\;A\tag{\(\Delta_1\)}\label{delta1} \\
& p : x \lesssim y & & \text{ implies } \iota^* (\Delta\;x\;y\;p) & \sim y & & \text{ for any } x, y : D\;A.\tag{\(\Delta_2\)}\label{delta2}
\end{alignat*}
\end{corollary}
Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
\begin{corollary}\label{cor:respects}
The setoid morphism \(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}:
\begin{alignat*}{1}
& g^{\sharp_b}\;x
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*(\Delta\;(race\;y\;x)\;x\;q))\tag{\ref{delta2}}
\\\overset{B}{=}\;&g^{\sharp_b}(\tilde{D}fst(\Delta\;(race\;y\;x)\;x\;q))\tag{\ref{respects-key-helper}}
\\\overset{B}{=}\;&g^{\sharp_b}(race\;y\;x)\tag{\ref{delta1}}
\\\overset{B}{=}\;&g^{\sharp_b}(race\;x\;y)\tag{\autoref{cor:race}}
\\\overset{B}{=}\;&g^{\sharp_b}(\tilde{D}fst(\Delta\;(race\;x\;y)\;y\;p))\tag{\ref{delta1}}
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*(\Delta\;(race\;x\;y)\;y\;p))\tag{\ref{respects-key-helper}}
\\\overset{B}{=}\;&g^{\sharp_b}\;y.\tag{\ref{delta2}}
\end{alignat*}
We have thus reduced the proof to showing that
\[g^{\sharp_b} (\tilde{D}fst\;z) \overset{B}{=} g^{\sharp_b}(\iota^*\;z) \text{ for any } z : D(A \times \mathbb{N}). \tag{*}\label{respects-key-helper}\]
Let us proceed as follows
\begin{alignat*}{1}
& g^{\sharp_b} (\tilde{D}fst\;z)
\\\overset{B}{=}\;&g_1^{\sharp_b}\;z\tag{\ref{law:uniformity}}
\\\overset{B}{=}\;&g_2^{\sharp_b}\;z
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*\;z). \tag{\ref{law:uniformity}}
\end{alignat*}
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) \\
i_2\;q & \text{if } p = later\;q
\end{cases}\]
and
\[g_2\;p := \begin{cases}
i_1(f\;x) & \text{if } p = now\;(x , n) \\
i_2\;q & \text{if } p = later\;q
\end{cases}\]
where \(o : A ⇝ A \times \mathbb{N}\) is a setoid morphism 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 morphism
\[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) \\
i_2(i_1(\tilde{D}o(\iota\;(x,n)))) & \text{if } p = now\;(x, n + 1) \\
i_2(i_2\;q) & \text{if } p = later\;q
\end{cases}\]
Let us now proceed by
\begin{alignat*}{1}
& g_1^{\sharp_b}\;z
\\\overset{B}{=}\;&{((id + [ id , id ]) \circ g_3)}^{\sharp_b}\;z
\\\overset{B}{=}\;&{([ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] \circ g_3)}^{\sharp_b}\;z\tag{\ref{law:diamond}}
\\\overset{B}{=}\;&g_2^{\sharp_b}\;z.
\end{alignat*}
Where for the first step notice that \(g_1\;x \overset{+}{=} (id + [ id , id ])(g_3\;x)\) for any \(x : \tilde{D}(A \times \mathbb{N})\) follows simply by case distinction on \(x\). For the last step, it suffices to show that \([ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x) \overset{+}{=} g_2\;x\) for any \(x : \tilde{D}(A \times \mathbb{N})\). We proceed by case distinction on \(x\).
\begin{mycase}
\case{} \(x = now\;(y, 0)\)\\
The goal reduces to
\begin{alignat*}{1}
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_1(f\;y))
\\\overset{+}{=}\;&i_1(f\;y)
\\\overset{+}{=}\;&g_2\;x,
\end{alignat*}
which indeed holds by the definitions of \(g_2\) and \(g_3\).
\case{} \(x = now\;(y, n + 1)\)\\
The goal reduces to
\begin{alignat*}{1}
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_2(i_1(\tilde{D}o(\iota\;(y,n)))))
\\\overset{+}{=}\;&i_1({((id + [ id , id]) \circ g_3)}^{\sharp_b}((\tilde{D}o(\iota\;(y,n)))))
\\\overset{+}{=}\;&i_1(f\;y)\tag{\ref{finalhelper}}
\\\overset{+}{=}\;&g_2\;x
\end{alignat*}
Where
\[{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,n))) \overset{B}{=} f\;y \tag{\(∗\)}\label{finalhelper}\]
follows by induction on \(n\):
\subcase{} \(n = 0\)\\
We are done by
\begin{alignat*}{1}
& {((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,0)))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(now\;y))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(now(y,0))
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id]) \circ g_3) (now(y,0))\tag{\ref{law:fixpoint}}
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id])) i_1(f\;y)
\\\overset{B}{=}\;&[ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] i_1(f\;y)
\\\overset{B}{=}\;&f\;y
\end{alignat*}
\subcase{} \(n = m + 1\)\\
Assuming that \({((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,m))) \overset{B}{=} f\;y\), we are done by
\begin{alignat*}{1}
& {((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,m+1)))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(later(\iota\;(y,m))))
\\\overset{B}{=}\;&{((id + [ id , id]) \circ g_3)}^{\sharp_b}(later(\tilde{D}o(\iota\;(y,m))))
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id]) \circ g_3) (later(\tilde{D}o(\iota\;(y,m))))\tag{\ref{law:fixpoint}}
\\\overset{B}{=}\;&([ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ] \circ (id + [ id , id])) (i_2(i_2(\tilde{D}o(\iota\;(y,m)))))
\\\overset{B}{=}\;&[ id , {((id + [ id , id]) \circ g_3)}^{\sharp_b} ](\tilde{D}o(\iota\;(y,m)))
\\\overset{B}{=}\;&f\;y
\end{alignat*}
\case{} \(x = later\;p\)\\
The goal reduces to
\begin{alignat*}{1}
& [ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (g_3\;x)
\\\overset{+}{=}\;&[ i_1 , {((id + [ id , id]) \circ g_3)}^{\sharp_b} + id ] (i_2(i_2\;p))
\\\overset{+}{=}\;&i_2\;p
\\\overset{+}{=}\;&g_2\;x,
\end{alignat*}
which instantly follows by definition.
\end{mycase}
This finishes the proof of the Corollary and thus \autoref{thm:Dfreeelgot} holds.
\end{proof}
We have shown in \autoref{thm:Dfreeelgot} that every \(\dbtilde{D}\;A\) extends to a free Elgot algebra. Together with \autoref{prop:setoids-ccc} and \autoref{thm:stability} this yields a description for the monad \(\mathbf{K}\) which has been defined in \autoref{chp:iteration}, in the category \(\setoids\).

2
src/titlepage.tex
View file

@ -23,7 +23,7 @@
% \large\bfseries
% \\ and \ldots
% \\[1cm]
\textbf{\large Bachelor Thesis in Computer Science}
\textbf{\large Bachelor Thesis in Computer Science (Consolidated Version)}
}\\[0.5\baselineskip]
\rule{\textwidth}{1pt}\par
\vfill