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

Finish proofs in chapter 4 and apply some chktex hints

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-09 10:46:41 +01:00
parent 75a6789d18
commit 5e3600d29c
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
9 changed files with 1085 additions and 1126 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
thesis/.chktexrc Normal file
View file

@ -0,0 +1,2 @@
# Exclude these environments from syntax checking
VerbEnvir { tikzcd }

4
thesis/Makefile
View file

@ -4,9 +4,9 @@ imgpdf = $(wildcard img/*.pdf)
.PHONY: all clean
all: $(pdf) $(imgpdf)
all: \((pdf) \)(imgpdf)
%.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib) $(imgpdf)
%.pdf: %.tex \((wildcard src/*.tex) \)(wildcard *.bib) $(imgpdf)
latexmk -pdf -xelatex -shell-escape -file-line-error -synctex=1 -halt-on-error -shell-escape $<
clean:

18
thesis/main.tex
View file

@ -165,19 +165,19 @@
\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.
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, \today{} \rule{7cm}{1pt}\\
\phantom{Erlangen, \today{}} \theauthor{}
\vspace{5em}
Erlangen, \today{} \rule{7cm}{1pt}\\
\phantom{Erlangen, \today{}} \theauthor{}
\end{german}
\chapter*{Licensing}
\doclicenseThis{}
\tableofcontents
\listoftodos
\listoftodos\
\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}}
@ -188,8 +188,8 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
% for creating custom labels like (Fixpoint)
\makeatletter
\newcommand{\customlabel}[2]{%
\protected@write \@auxout {}{\string \newlabel {#1}{{#2}{\thepage}{#2}{#1}{}} }%
\hypertarget{#1}{#2}%
\protected@write \@auxout {}{\string \newlabel {#1}{{#2}{\thepage}{#2}{#1}{}} }%
\hypertarget{#1}{#2}%
}
\makeatother
@ -219,5 +219,3 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
\renewcommand*{\listtheoremname}{List of Definitions}
\listoftheorems[ignoreall,show={definition}]
\end{document}
% vim: tw=80 nospell spelllang=en nocul

590
thesis/src/01_preliminaries.tex
View file

@ -1,94 +1,102 @@
\chapter{Preliminaries}
We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co-)products, terminal and initial objects and special morphisms like isos, epis and monos.
We assume familiarity with basic categorical notions, in particular: categories, functors, functor algebras and natural transformations, as well as special objects like (co-) products, terminal and initial objects and special morphisms like isos, epis and monos.
In this chapter we will introduce notation that will be used throughout the thesis and also introduce some notions that are crucial to this thesis in more detail.
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 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}
Let us first introduce notation for binary (co-) products by giving their usual diagrams:
\begin{figure}[ht]
% https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
\[\begin{tikzcd}
A && {A \times B} && B && A && {A + B} && B \\
\\
&& 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]
\end{tikzcd}\]
\caption{The defining diagrams of products and coproducts}
% https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
\[
\begin{tikzcd}
A && {A \times B} && B && A && {A + B} && B \\
\\
&& 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]
\end{tikzcd}
\]
\caption{The defining diagrams of products and coproducts}
\end{figure}
We will furthermore overload this notation and write $f \times g := \langle f \circ \pi_1 , g \circ \pi_2 \rangle$ and $f + g := \lbrack i_1 \circ f , i_2 \circ g \rbrack$ on morphisms. To avoid parentheses we will use the convention that products bind stronger than coproducts.
We will furthermore overload this notation and write \(f \times g := \langle f \circ \pi_1 , g \circ \pi_2 \rangle \) and \(f + g := \lbrack i_1 \circ f , i_2 \circ g \rbrack \) on morphisms. To avoid parentheses we will use the convention that products bind stronger than coproducts.
We write $1$ for the terminal object together with the unique morphism $! : A \rightarrow 1$ and $0$ for the initial object with the unique morphism $\text{!`} : A \rightarrow 0$.
We write \(1\) for the terminal object together with the unique morphism \(! : A \rightarrow 1\) and \(0\) for the initial object with the unique morphism \(¡ : A \rightarrow 0\).
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.
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}
A cartesian and cocartesian category $\C$ is called distributive if the canonical (left) distributivity morphism $dstl^{-1}$ is an iso:
A cartesian and cocartesian category \(\C \) is called distributive if the canonical (left) distributivity morphism \(dstl^{-1}\) is an iso:
% https://q.uiver.app/#q=WzAsMixbMCwwLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzMsMCwiWCBcXHRpbWVzIChZICsgWikiXSxbMCwxLCJkc3RsXnstMX0gOj0ge1xcbGJyYWNrIGlkIFxcdGltZXMgaV8xICwgaWQgXFx0aW1lcyBpXzIgXFxyYnJhY2t9IiwwLHsiY3VydmUiOi0zfV0sWzEsMCwiZHN0bCIsMCx7ImN1cnZlIjotM31dXQ==
\[\begin{tikzcd}
{X \times Y + X \times Z} &&& {X \times (Y + Z)}
\arrow["{dstl^{-1} := {\lbrack id \times i_1 , id \times i_2 \rbrack}}", curve={height=-18pt}, from=1-1, to=1-4]
\arrow["dstl", curve={height=-18pt}, from=1-4, to=1-1]
\end{tikzcd}\]
\[
\begin{tikzcd}
{X \times Y + X \times Z} &&& {X \times (Y + Z)}
\arrow["{dstl^{-1} := {\lbrack id \times i_1 , id \times i_2 \rbrack}}", curve={height=-18pt}, from=1-1, to=1-4]
\arrow["dstl", curve={height=-18pt}, from=1-4, to=1-1]
\end{tikzcd}
\]
\end{definition}
\begin{remark}
Definition~\ref{def:distributive} can equivalently be expressed by requiring that the canonical (right) distributivity morphism is an iso, giving these inverse morphisms:
% https://q.uiver.app/#q=WzAsMixbMCwwLCJZIFxcdGltZXMgWCArIFpcXHRpbWVzIFgiXSxbMywwLCIoWSArIFopIFxcdGltZXMgWCJdLFswLDEsImRzdHJeey0xfSA6PSBbIGlfMSBcXHRpbWVzIGlkICwgaV8yIFxcdGltZXMgaWQgXSIsMCx7ImN1cnZlIjotM31dLFsxLDAsImRzdHIiLDAseyJjdXJ2ZSI6LTN9XV0=
\[\begin{tikzcd}
{Y \times X + Z\times X} &&& {(Y + Z) \times X}
\arrow["{dstr^{-1} := [ i_1 \times id , i_2 \times id ]}", curve={height=-18pt}, from=1-1, to=1-4]
\arrow["dstr", curve={height=-18pt}, from=1-4, to=1-1]
\end{tikzcd}\]
\[
\begin{tikzcd}
{Y \times X + Z\times X} &&& {(Y + Z) \times X}
\arrow["{dstr^{-1} := [ i_1 \times id , i_2 \times id ]}", curve={height=-18pt}, from=1-1, to=1-4]
\arrow["dstr", curve={height=-18pt}, from=1-4, to=1-1]
\end{tikzcd}
\]
These two can be derived from each other by taking either
\[dstr := (swap + swap) \circ dstl \circ swap \]
or
\[dstl := (swap + swap) \circ dstr \circ swap \]
where $swap := \langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A$.
where \(swap := \langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A\).
\end{remark}
\begin{proposition}
The distribution morphisms can be viewed as natural transformations i.e.\ they satisfy the following diagrams:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIFxcdGltZXMgKFkgK1opIl0sWzIsMCwiQSBcXHRpbWVzIChCICsgQykiXSxbMCwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBaIl0sWzIsMSwiQSBcXHRpbWVzIEIgKyBBIFxcdGltZXMgQyJdLFszLDAsIihZICsgWikgXFx0aW1lcyBYIl0sWzUsMCwiKEIgKyBDKSBcXHRpbWVzIEEiXSxbMywxLCJZIFxcdGltZXMgWCArIFogXFx0aW1lcyBYIl0sWzUsMSwiQiBcXHRpbWVzIEEgKyBDIFxcdGltZXMgQSJdLFswLDEsImYgXFx0aW1lcyAoZyArIGgpIl0sWzIsMywiZiBcXHRpbWVzIGcgKyBmIFxcdGltZXMgaCJdLFswLDIsImRzdGwiXSxbMSwzLCJkc3RsIl0sWzQsNSwiKGcgKyBoKSBcXHRpbWVzIGYiXSxbNCw2LCJkc3RyIiwyXSxbNSw3LCJkc3RyIl0sWzYsNywiZyBcXHRpbWVzIGYgKyBoIFxcdGltZXMgZiJdXQ==
\[\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}
\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]
\end{tikzcd}\]
\[
\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}
\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]
\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.
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}
& 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}
\end{alignat*}
\end{proof}
@ -96,173 +104,183 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
The distribution morphisms satisfy the following properties:
\begin{enumerate}
\item $dstl \circ (id \times i_1) = i_1$
\item $dstl \circ (id \times i_2) = i_2$
\item $[ \pi_1 , \pi_1 ] \circ dstl = \pi_1$
\item $( \pi_2 + \pi_2 ) \circ dstl = \pi_2$
\item $dstl \circ swap = (swap + swap) \circ dstr$
\item $dstr \circ (i_1 \times id) = i_1$
\item $dstr \circ (i_2 \times id) = i_2$
\item $(\pi_1 + \pi_1) \circ dstr = \pi_1$
\item $[ \pi_2 , \pi_2 ] \circ dstr = \pi_2$
\item $dstr \circ swap = (swap + swap) \circ dstl$
\item \(dstl \circ (id \times i_1) = i_1\)
\item \(dstl \circ (id \times i_2) = i_2\)
\item \([ \pi_1 , \pi_1 ] \circ dstl = \pi_1\)
\item \(( \pi_2 + \pi_2 ) \circ dstl = \pi_2\)
\item \(dstl \circ swap = (swap + swap) \circ dstr\)
\item \(dstr \circ (i_1 \times id) = i_1\)
\item \(dstr \circ (i_2 \times id) = i_2\)
\item \((\pi_1 + \pi_1) \circ dstr = \pi_1\)
\item \([ \pi_2 , \pi_2 ] \circ dstr = \pi_2\)
\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:
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*}
\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}
&\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*}
\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}
&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
\end{alignat*}
\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
\end{alignat*}
\end{enumerate}
\end{proof}
\begin{definition}[Exponential Object]
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:
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
\[\begin{tikzcd}
{Z \times Y} && {X^Y \times Y} \\
\\
&& X
\arrow["eval", from=1-3, to=3-3]
\arrow["{curry\;f \times id}", from=1-1, to=1-3]
\arrow["f"', from=1-1, to=3-3]
\end{tikzcd}\]
\[
\begin{tikzcd}
{Z \times Y} && {X^Y \times Y} \\
\\
&& X
\arrow["eval", from=1-3, to=3-3]
\arrow["{curry\;f \times id}", from=1-1, to=1-3]
\arrow["f"', from=1-1, to=3-3]
\end{tikzcd}
\]
\end{definition}
A cartesian closed category is a cartesian category $\C$ that also has an exponential object $X^Y$ for any $X, Y \in \C$.
The internal logic of cartesian closed categories is the simply typed $\lambda$-calculus, which makes them a suitable target for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however does not have to be cartesian closed as to be more general.
\todo[inline]{Properties of exponentials, \(\beta, \eta, \ldots \)}
A cartesian closed category is a cartesian category \(\C \) that also has an exponential object \(X^Y\) for any \(X, Y \in \C \).
The internal logic of cartesian closed categories is the simply typed \(\lambda \)-calculus, which makes them a suitable target for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however does not have to be cartesian closed as to be more general.
\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 modelling 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.
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 modelling 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]
A tuple $(X \in \obj{\C}, \alpha : X \rightarrow FX)$ is called an F-coalgebra.
A tuple \((X \in \obj{\C}, \alpha : X \rightarrow FX)\) is called an F-coalgebra.
\end{definition}
\begin{definition}[Morphisms between Coalgebras]\label{def:coalgmorph}
Let $(X \in \obj{\C} , \alpha : X \rightarrow FX)$ and $(Y \in \obj{\C} , \beta : Y \rightarrow FY)$ be two F-coalgebras. A morphism between these coalgebras is a morphism $f : X \rightarrow Y$ such that the following diagram commutes:
Let \((X \in \obj{\C} , \alpha : X \rightarrow FX)\) and \((Y \in \obj{\C} , \beta : Y \rightarrow FY)\) be two F-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=
\[\begin{tikzcd}[ampersand replacement=\&]
X \&\& FX \\
\\
Y \&\& FY
\arrow["\beta", from=3-1, to=3-3]
\arrow["\alpha", from=1-1, to=1-3]
\arrow["f"', from=1-1, to=3-1]
\arrow["Ff", from=1-3, to=3-3]
\end{tikzcd}\]
\[
\begin{tikzcd}[ampersand replacement=\&]
X \&\& FX \\
\\
Y \&\& FY
\arrow["\beta", from=3-1, to=3-3]
\arrow["\alpha", from=1-1, to=1-3]
\arrow["f"', from=1-1, to=3-1]
\arrow["Ff", from=1-3, to=3-3]
\end{tikzcd}
\]
\end{definition}
\todo[inline]{Adopt text, lemma style}
\begin{proposition}
F-coalgebras together with their morphisms form a category that we call $Coalg(F)$.
F-coalgebras together with their morphisms form a category that we call \(Coalg(F)\).
\end{proposition}
\begin{proof}
Let $(X , \alpha : X \rightarrow FX)$ be an F-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)\) be an F-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 F-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:
Let \((X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)\) and \((Z , \gamma : Z \rightarrow FZ)\) be F-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
& \gamma \circ g \circ f \\
=\; & Fg \circ \beta \circ f \\
=\; & Fg \circ Ff \circ \alpha \\
=\; & F(g \circ f) \circ \alpha
\end{alignat*}
\end{proof}
The terminal object of $Coalg(F)$ is sometimes called \textit{final F-coalgebra} and can now similarly to initial F-algebras be used for modelling 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 F-coalgebras concrete:
The terminal object of \(Coalg(F)\) is sometimes called \textit{final F-coalgebra} and can now similarly to initial F-algebras be used for modelling 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 F-coalgebras concrete:
\begin{definition}[Terminal F-Coalgebra]
An F-coalgebra $(T, t : T \rightarrow FT)$ is called a terminal F-coalgebra if for any other F-coalgebra $(X, \alpha : X \rightarrow FX)$ there exists a unique morphism $\coalg{\alpha} : X \rightarrow T$ satisfying:
An F-coalgebra \((T, t : T \rightarrow FT)\) is called a terminal F-coalgebra if for any other F-coalgebra \((X, \alpha : X \rightarrow FX)\) there exists a unique morphism \(\coalg{\alpha} : X \rightarrow T\) satisfying:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzIsMCwiRlgiXSxbMCwyLCJUIl0sWzIsMiwiRlQiXSxbMCwxLCJcXGFscGhhIl0sWzIsMywidCJdLFswLDIsIlxcbGxicmFja2V0IFxcYWxwaGEgXFxycmJyYWNrZXQiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMSwzLCJGXFxsbGJyYWNrZXQgXFxhbHBoYSBcXHJyYnJhY2tldCJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
X \&\& FX \\
\\
T \&\& FT
\arrow["\alpha", from=1-1, to=1-3]
\arrow["t", from=3-1, to=3-3]
\arrow["{\coalg{\alpha}}"', dashed, from=1-1, to=3-1]
\arrow["{F\coalg{\alpha}}", from=1-3, to=3-3]
\end{tikzcd}\]
\[
\begin{tikzcd}[ampersand replacement=\&]
X \&\& FX \\
\\
T \&\& FT
\arrow["\alpha", from=1-1, to=1-3]
\arrow["t", from=3-1, to=3-3]
\arrow["{\coalg{\alpha}}"', dashed, from=1-1, to=3-1]
\arrow["{F\coalg{\alpha}}", from=1-3, to=3-3]
\end{tikzcd}
\]
\end{definition}
\begin{lemma}[Lambek's Lemma~\cite{lambek}]
Let $(T, t : T \rightarrow FT)$ be a terminal F-coalgebra. Then $t$ is an isomorphism.
Let \((T, t : T \rightarrow FT)\) be a terminal F-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:
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}\]
\[
\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\):
$\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 \(\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*}
\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}
@ -270,166 +288,174 @@ The terminal object of $Coalg(F)$ is sometimes called \textit{final F-coalgebra}
Monads are widely known among programmers as a way of modelling effects in pure languages and are also central to this thesis. Let us recall the basic definitions\cite{Lane1971}\cite{moggi}.
\begin{definition}[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:
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}\\
&\mu_X \circ \eta_{TX} &&= id_{TX} \tag*{(M2)}\label{M2}\\
&\mu_X \circ T\eta_X &&= id_{TX} \tag*{(M3)}\label{M3}
& \mu_X \circ \mu_{TX} & & = \mu_X \circ T\mu_X \tag*{(M1)}\label{M1} \\
& \mu_X \circ \eta_{TX} & & = id_{TX} \tag*{(M2)}\label{M2} \\
& \mu_X \circ T\eta_X & & = id_{TX} \tag*{(M3)}\label{M3}
\end{alignat*}
These laws are expressed by the following diagrams:
% with indices: % https://q.uiver.app/#q=WzAsOCxbMCwwLCJUVFRYIl0sWzIsMCwiVFRYIl0sWzAsMiwiVFRYIl0sWzIsMiwiVFgiXSxbNCwwLCJUWCJdLFs2LDAsIlRUWCJdLFs4LDAsIlRYIl0sWzYsMiwiVFgiXSxbMCwxLCJcXG11X3tUWH0iXSxbMCwyLCJUXFxtdV9YIiwyXSxbMSwzLCJcXG11X1giXSxbNSw3LCJcXG11X1giXSxbNCw1LCJcXGV0YV97VFh9Il0sWzYsNSwiVFxcZXRhX1giXSxbNCw3LCJpZF97VFh9IiwyXSxbNiw3LCJpZF97VFh9IiwyXSxbMiwzLCJcXG11X1giLDJdXQ==
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJUVFRYIl0sWzIsMCwiVFRYIl0sWzAsMiwiVFRYIl0sWzIsMiwiVFgiXSxbNCwwLCJUWCJdLFs2LDAsIlRUWCJdLFs4LDAsIlRYIl0sWzYsMiwiVFgiXSxbMCwxLCJcXG11Il0sWzAsMiwiVFxcbXUiLDJdLFsxLDMsIlxcbXUiXSxbNSw3LCJcXG11Il0sWzQsNSwiXFxldGEiXSxbNiw1LCJUIl0sWzQsNywiaWQiLDJdLFs2LDcsImlkIiwyXSxbMiwzLCJcXG11IiwyXV0=
\[\begin{tikzcd}
TTTX && TTX && TX && TTX && TX \\
\\
TTX && TX &&&& TX
\arrow["\mu", from=1-1, to=1-3]
\arrow["T\mu"', from=1-1, to=3-1]
\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]
\end{tikzcd}\]
\[
\begin{tikzcd}
TTTX && TTX && TX && TTX && TX \\
\\
TTX && TX &&&& TX
\arrow["\mu", from=1-1, to=1-3]
\arrow["T\mu"', from=1-1, to=3-1]
\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]
\end{tikzcd}
\]
\end{definition}
As with many categorical concepts we may consider the category of monads:
\todo[inline]{Use text => lemma style}
\begin{definition}[The Category of Monads]~\label{def:monads}
Let $\C$ be a category.
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 satisfying:
Let \(\C \) be a category.
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 satisfying:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFszLDAsIlNTWCJdLFs1LDAsIlNUWCJdLFszLDEsIlNYIl0sWzcsMCwiVFRYIl0sWzcsMSwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
\[\begin{tikzcd}[ampersand replacement=\&]
X \&\& SX \& SSX \&\& STX \&\& TTX \\
\&\& TX \& 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]
\end{tikzcd}\]
\[
\begin{tikzcd}[ampersand replacement=\&]
X \&\& SX \& SSX \&\& STX \&\& TTX \\
\&\& TX \& 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]
\end{tikzcd}
\]
This yields the category of monads on $\C$ which we call $\monads{\C}$. 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.
This yields the category of monads on \(\C \) which we call \(\monads{\C}\). 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{definition}
Monads can also be specified in a second equivalent way that is better suited to describe computation.
\begin{definition}[Kleisli Triple]
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:
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}\\
&f^* \circ \eta_X &&= f &&\text{ for any } f : X \rightarrow FY \tag*{(K2)}\label{K2}\\
&f^* \circ g* &&= (f^* \circ g)^* &&\text{ for any } f : Y \rightarrow FZ, g : X \rightarrow FY \tag*{(K3)}\label{K3}
& \eta_X^* & & = id_{FX} \tag*{(K1)}\label{K1} \\
& f^* \circ \eta_X & & = f & & \text{ for any } f : X \rightarrow FY \tag*{(K2)}\label{K2} \\
& f^* \circ g* & & = {(f^* \circ g)}^* & & \text{ for any } f : Y \rightarrow FZ, g : X \rightarrow FY \tag*{(K3)}\label{K3}
\end{alignat*}
\end{definition}
Let $f : X \rightarrow TY, g : Y \rightarrow TZ$ be two programs, where $T$ is a Kleisli triple. These programs can be composed by taking: $f^* \circ g : X \rightarrow TZ$, which is called Kleisli composition. Haskell's do-notation is a useful tool for writing Kleisli composition in a legible way. $f^* \circ g$ can equivalently be expressed as:
Let \(f : X \rightarrow TY, g : Y \rightarrow TZ\) be two programs, where \(T\) is a Kleisli triple. These programs can be composed by taking: \(f^* \circ g : X \rightarrow TZ\), which is called Kleisli composition. Haskell's do-notation is a useful tool for writing Kleisli composition in a legible way. We will sometimes express \((f^* \circ g) x\) equivalently as
\begin{minted}{haskell}
do y <- f x
g y
do y <- g x
f y
\end{minted}
The possibility of Kleisli composition enables us to define the category of programs for any Kleisli triple $T$.
The possibility of Kleisli composition enables us to define the category of programs for any Kleisli triple \(T\).
\begin{definition}[Kleisli Category]
Given a monad $T$ on a category $\C$, the Kleisli category $\C^T$ is defined as:
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}$
\item $\mathcal{C^T}(X, Y) = \C(X, TY)$
\item \(\vert \C^T \vert = \obj{C}\)
\item \(\mathcal{C^T}(X, Y) = \C(X, TY)\)
\item Composition of programs is Kleisli composition.
\item The identity morphisms are the unit morphisms of $T$, $id_X = \eta_X : X \rightarrow TX$
\end{itemize}
\item The identity morphisms are the unit morphisms of \(T\), \(id_X = \eta_X : X \rightarrow TX\)
\end{itemize}
The laws of categories then follow from the Kleisli triple laws.
\end{definition}
\begin{theorem}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
\end{theorem}
\begin{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.
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 get 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}^*$
``\(\Rightarrow \)'':
Given a Kleisli triple \((F, \eta, {(-)}^*)\),
we get 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 get 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$.
``\(\Leftarrow \)'': \\
Given a monad \((F, \eta, \mu)\),
we get 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.
\section{Strong and Commutative Monads}
When modelling partiality with a monad, one would expect the following two programs to be equivalent:
When modelling partiality with a monad, one would expect the following two programs to be equivalent
\begin{multicols}{2}
\begin{minted}{haskell}
do x <- p
y <- q
return (x, y)
\end{minted}
\begin{minted}{haskell}
\begin{minted}{haskell}
do y <- q
x <- p
return (x, y)
\end{minted}
\end{multicols}
where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
Where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
\change[inline]{Find Motivation for strong monads}
\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] 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}\\
&\tau_{X,Y} \circ (id_X \times \mu_Y) &&= \mu_{X\times Y} \circ T\tau_{X,Y} \circ \tau_{X,TY} \tag*{(S3)}\label{S3}\\
&M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} &&= \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,TZ} \tag*{(S4)}\label{S4}
& 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} \\
& \tau_{X,Y} \circ (id_X \times \mu_Y) & & = \mu_{X\times Y} \circ T\tau_{X,Y} \circ \tau_{X,TY} \tag*{(S3)}\label{S3} \\
& M \alpha_{X,Y,Z} \circ \tau_{X \times Y, Z} & & = \tau_{X, Y\times Z} \circ (id_X \times \tau_{Y, Z}) \circ \alpha_{X,Y,TZ} \tag*{(S4)}\label{S4}
\end{alignat*}
where $\alpha_{X,Y,Z} = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : X \times (Y \times Z) \rightarrow (X \times Y) \times Z$ is the associativity morphism on products.
where \(\alpha_{X,Y,Z} = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : X \times (Y \times Z) \rightarrow (X \times Y) \times Z\) is the associativity morphism on products.
\end{definition}
\todo[inline]{Use text => lemma style}
As with monads we can now consider the category of strong monads:
\begin{definition}[The Category of Strong Monads]\label{def:strongmonads}
Let $\C$ be a category. A morphism between two strong monads $(S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)$ and $(T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)$ is a morphism between monads as in \autoref{def:monads} that additionally satisfies:
Let \(\C \) be a category. A morphism between two strong monads \((S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)\) and \((T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)\) is a morphism between monads as in \autoref{def:monads} that additionally satisfies:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgU1kiXSxbMCwyLCJTKFggXFx0aW1lcyBZKSJdLFsyLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIFRZIl0sWzAsMSwiXFx0YXVeUyJdLFsxLDIsIlxcYWxwaGEiXSxbMCwzLCJpZCBcXHRpbWVzIFxcYWxwaGEiXSxbMywyLCJcXHRhdV5UIiwyXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
{X \times SY} \&\& {X \times TY} \\
\\
{S(X \times Y)} \&\& {T(X \times Y)}
\arrow["{\tau^S}", from=1-1, to=3-1]
\arrow["\alpha", from=3-1, to=3-3]
\arrow["{id \times \alpha}", from=1-1, to=1-3]
\arrow["{\tau^T}"', from=1-3, to=3-3]
\end{tikzcd}\]
This yields the category $\strongmonads{\C}$ of strong monads over $\C$.
\[
\begin{tikzcd}[ampersand replacement=\&]
{X \times SY} \&\& {X \times TY} \\
\\
{S(X \times Y)} \&\& {T(X \times Y)}
\arrow["{\tau^S}", from=1-1, to=3-1]
\arrow["\alpha", from=3-1, to=3-3]
\arrow["{id \times \alpha}", from=1-1, to=1-3]
\arrow["{\tau^T}"', from=1-3, to=3-3]
\end{tikzcd}
\]
This yields the category \(\strongmonads{\C}\) of strong monads over \(\C \).
\end{definition}
Now we can express the above condition:
\begin{definition}[Commutative Monad]
A strong monad $\mathbf{T}$ is called commutative if the (right) strength $\tau$ commutes with the induced left strength
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.
Concretely, $\mathbf{T}$ is called commutative if the following diagram commutes:
that satisfies symmetrical conditions to the ones \(\tau \) satisfies.
Concretely, \(\mathbf{T}\) is called commutative if the following diagram commutes:
% https://q.uiver.app/#q=WzAsNCxbMCwyLCJUKFggXFx0aW1lcyBUWSkiXSxbMiwwLCJUKFRYIFxcdGltZXMgWSkiXSxbMiwyLCJUKFggXFx0aW1lcyBZKSJdLFswLDAsIlRYIFxcdGltZXMgVFkiXSxbMywxLCJcXHRhdSJdLFszLDAsIlxcc2lnbWEiLDJdLFswLDIsIlxcdGF1XioiLDJdLFsxLDIsIlxcc2lnbWFeKiJdXQ==
\[\begin{tikzcd}
{TX \times TY} && {T(TX \times Y)} \\
\\
{T(X \times TY)} && {T(X \times Y)}
\arrow["\tau", from=1-1, to=1-3]
\arrow["\sigma"', from=1-1, to=3-1]
\arrow["{\tau^*}"', from=3-1, to=3-3]
\arrow["{\sigma^*}", from=1-3, to=3-3]
\end{tikzcd}\]
\[
\begin{tikzcd}
{TX \times TY} && {T(TX \times Y)} \\
\\
{T(X \times TY)} && {T(X \times Y)}
\arrow["\tau", from=1-1, to=1-3]
\arrow["\sigma"', from=1-1, to=3-1]
\arrow["{\tau^*}"', from=3-1, to=3-3]
\arrow["{\sigma^*}", from=1-3, to=3-3]
\end{tikzcd}
\]
\end{definition}
\section{Free Objects}
@ -438,33 +464,35 @@ on free structures in \autoref{chp:iteration} to define a monad in a general set
to establish some notation and then describe how to obtain a monad via existence of free objects.
\begin{definition}[Free Object]\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} : UFX \rightarrow UY$ satisfying:
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} : UFX \rightarrow UY\) satisfying:
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJVRlgiXSxbMCwxLCJmIl0sWzAsMiwiXFxldGEiLDJdLFsyLDEsIlxcZnJlZXtmfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
X \& UY \\
UFX
\arrow["f", from=1-1, to=1-2]
\arrow["\eta"', from=1-1, to=2-1]
\arrow["{\free{f}}"', dashed, from=2-1, to=1-2]
\end{tikzcd}\]
\[
\begin{tikzcd}[ampersand replacement=\&]
X \& UY \\
UFX
\arrow["f", from=1-1, to=1-2]
\arrow["\eta"', from=1-1, to=2-1]
\arrow["{\free{f}}"', dashed, from=2-1, to=1-2]
\end{tikzcd}
\]
\end{definition}
\begin{theorem}\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$.
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{theorem}
\begin{proof}
We are left to check the laws of Kleisli triples.
\begin{itemize}
\item[\ref{K1}] $\free{\eta} = id$
\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}$.
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}\).
\end{itemize}
\end{proof}

32
thesis/src/02_agda-categories.tex
View file

@ -8,24 +8,24 @@ This chapter shall serve as a quick introduction to the library and the formaliz
\section{Setoid Enriched Categories}
The usual textbook definition of a category glosses over some design decisions that have to be made when implementing it in type theory. One would usually see something like this:
\begin{definition}[Category]
A category consists of
\begin{itemize}
\item A collection of objects
\item A collection of morphisms between objects
\item For every two morphisms $f : X \rightarrow Y, g : Y \rightarrow Z$ another morphism $g \circ f : X \rightarrow Z$ called the composition
\item For every object $X$ a morphism $id_X : X \rightarrow X$ called the identity
\end{itemize}
where the composition is associative, and the identity morphisms are identities with respect to the composition.
A category consists of
\begin{itemize}
\item A collection of objects
\item A collection of morphisms between objects
\item For every two morphisms \(f : X \rightarrow Y, g : Y \rightarrow Z\) another morphism \(g \circ f : X \rightarrow Z\) called the composition
\item For every object \(X\) a morphism \(id_X : X \rightarrow X\) called the identity
\end{itemize}
where the composition is associative, and the identity morphisms are identities with respect to the composition.
\end{definition}
Here \textit{collection} refers to something that behaves set-like, which is not a set and is needed to prevent size issues (there is no set of all sets, otherwise we would obtain Russel's paradox, but there is a collection of all sets), it is not immediately clear how to translate this to type theory.
Furthermore, in mathematical textbooks equality between morphisms is usually taken for granted, i.e. there is some global notion of equality that is clear to everyone. In type theory we need to be more thorough as there is no global notion of equality, eligible for all purposes, e.g. the standard notion of propositional equality has issues when dealing with functions in that it requires extra axioms like functional extensionality.
Furthermore, in mathematical textbooks equality between morphisms is usually taken for granted, i.e.\ there is some global notion of equality that is clear to everyone. In type theory we need to be more thorough as there is no global notion of equality, eligible for all purposes, e.g.\ the standard notion of propositional equality has issues when dealing with functions in that it requires extra axioms like functional extensionality.
The definition of category that we will work with can be seen in listing~\ref{lst:category} (unnecessary information has been stripped).
The key differences to the definition above are firstly that instead of talking about collections, Agda's infinite \Verb{Set} hierarchy is utilized to prevent size issues.
The notion of category is thus parametrized by 3 universe levels, one for objects, one for morphisms and one for equalities.
The consequence is that the category does not contain a type of all morphisms, instead it contains a type of morphisms for any pair of objects.
Furthermore, the types of morphisms are equipped with an equivalence relation \Verb{_≈_}, making them setoids.
The definition of category that we will work with can be seen in listing~\ref{lst:category} (unnecessary information has been stripped).
The key differences to the definition above are firstly that instead of talking about collections, Agda's infinite \Verb{Set} hierarchy is utilized to prevent size issues.
The notion of category is thus parametrized by 3 universe levels, one for objects, one for morphisms and one for equalities.
The consequence is that the category does not contain a type of all morphisms, instead it contains a type of morphisms for any pair of objects.
Furthermore, the types of morphisms are equipped with an equivalence relation \Verb{_≈_}, making them setoids.
This addresses the aforementioned issue of how to implement equality between morphisms: the notion of equality is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}.
Because of using a custom equality relation, proofs like \Verb{∘-resp-≈} are needed throughout the library to make sure that operations on morphisms respect the equivalence relation.
Lastly, the authors also include symmetric proofs like \Verb{sym-assoc} to definitions, in this case to guarantee that the opposite category of the opposite category is equal to the original category, and a similar reason for requiring \Verb{identity²}, we won't address the need for these proofs and just accept the requirement as given for the rest of the thesis.
@ -58,12 +58,12 @@ record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
\label{lst:category}
\end{listing}
From this it should be clear how other basic notions like functors or natural transformations look in the library.
From this it should be clear how other basic notions like functors or natural transformations look in the library.
\section{The formalization}
\improvement{Explain more}
The Agda formalization of this thesis is structured similar to the agda-categories library, e.g. key concepts like monads and categories correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties, and possibly folders 'Instances' for specific instances, and 'Construction' for blueprints for constructing this concept (e.g. the Kleisli category of a monad would be in 'Category.Construction.Kleisli').
The Agda formalization of this thesis is structured similar to the agda-categories library, e.g.\ key concepts like monads and categories correspond to separate top-level folders, which contain the core definitions as well as folders for sub-concepts and their properties, and possibly folders `Instances' for specific instances, and `Construction' for blueprints for constructing this concept (e.g.\ the Kleisli category of a monad would be in `Category.Construction.Kleisli').
The source code of the formalization can be found \href{https://git8.cs.fau.de/theses/bsc-leon-vatthauer}{here} (internal) or as clickable HTML \href{https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/}{here} (public).

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

@ -1,5 +1,5 @@
\chapter{Partiality Monads}\label{chp:partiality}
Moggi's categorical semantics~\cite{moggi} describe a way to interpret an effectful programming language in a category. For this one needs a (strong) monad $T$ capturing the desired effects, then we can take the elements of $TA$ as denotations for programs of type $A$. The Kleisli category of $T$ can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
Moggi's categorical semantics~\cite{moggi} describe a way to interpret an effectful programming language in a category. For this one needs a (strong) monad \(T\) capturing the desired effects, then we can take the elements of \(TA\) as denotations for programs of type \(A\). The Kleisli category of \(T\) can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples.
@ -19,25 +19,25 @@ To ensure that programs are partial, we recall the following notion by Cockett a
\newcommand{\tdom}{\text{dom}\;}
\begin{definition}[Restriction Structure]
A restriction structure on a category $\mathcal{C}$ is a mapping $dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)$ with the following properties:
A restriction structure on a category \(\mathcal{C}\) is a mapping \(dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)\) with the following properties:
\begin{alignat*}{1}
f \circ (\tdom f) & = f\tag*{(R1)}\label{R1} \\
(\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2} \\
\tdom(g \circ (\tdom f)) & = (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3} \\
(\tdom h) \circ f & = f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4}
\end{alignat*}
for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
for any \(X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z\).
\end{definition}
\begin{lemma}
For any $f : X \rightarrow Y$ the restriction morphism $\tdom f$ is idempotent.
For any \(f : X \rightarrow Y\) the restriction morphism \(\tdom f\) is idempotent.
\end{lemma}
\begin{proof}
This follows by \ref{R3} and \ref{R1}:
This follows by~\ref{R3} and~\ref{R1}:
\[\tdom f \circ \tdom f = \tdom (f \circ \tdom f) = \tdom f\]
\end{proof}
The idempotent morphism $\tdom f : X \rightarrow X$ represents the domain of definiteness of $f : X \rightarrow Y$. In the category of partial functions this takes the following form:
The idempotent morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
\[
(\tdom f)(x) = \begin{cases}
@ -46,30 +46,31 @@ The idempotent morphism $\tdom f : X \rightarrow X$ represents the domain of def
\end{cases}
\]
That is, $\tdom f$ is only defined on values where $f$ is defined and for those values it behaves like the identity function.
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]
Every category has a trivial restriction structure by taking $dom (f : X \rightarrow Y) = id_X$.
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}
For a suitable defined partiality monad $T$ the Kleisli category $\C^T$ should be a restriction category.
For a suitable defined partiality monad \(T\) the Kleisli category \(\C^T\) should be a restriction category.
Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
\begin{definition}[Equational Lifting Monad]
\label{def:eqlm}
A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:
\begin{definition}[Equational Lifting Monad]\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==
\[\begin{tikzcd}
\[
\begin{tikzcd}
TX && {TX \times TX} \\
\\
&& {T(TX \times X)}
\arrow["\Delta", from=1-1, to=1-3]
\arrow["\tau", from=1-3, to=3-3]
\arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
\end{tikzcd}\]
where $\Delta : X \rightarrow X \times X$ is the diagonal morphism.
\end{tikzcd}
\]
where \(\Delta : X \rightarrow X \times X\) is the diagonal morphism.
\end{definition}
To make the equational lifting property more comprehensible we can alternatively state it using do-notation. The equational lifting property states that the following programs must be equal:
@ -79,23 +80,23 @@ To make the equational lifting property more comprehensible we can alternatively
do x <- p
return (x , p)
\end{minted}
\begin{minted}{haskell}
do x <- p
return (x , return x)
\end{minted}
\end{multicols}
That is, if some computation $p : TX$ terminates with the result $x : X$, then $p = return\;x$ must hold. This of course implies that running $p$ multiple times yields the same result as running $p$ once.
That is, if some computation \(p : TX\) terminates with the result \(x : X\), then \(p = return\;x\) must hold. This of course implies that running \(p\) multiple times yields the same result as running \(p\) once.
\begin{theorem}[\cite{eqlm}]
If $T$ is an equational lifting monad the Kleisli category $\mathcal{C}^T$ is a restriction category.
If \(T\) is an equational lifting monad the Kleisli category \(\mathcal{C}^T\) is a restriction category.
\end{theorem}
Definition~\ref{def:eqlm} combines all three properties stated above, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads. For the rest of this chapter we will use these definitions to compare two monads that are commonly used to model partiality.
\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. This is generally known as the maybe monad and can be viewed as the canonical example of an equational lifting 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. 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.
\end{theorem}
@ -103,7 +104,7 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
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$:
Naturality of \(\tau \) follows by naturality of \(dstl\):
\begin{alignat*}{1}
& (id + !) \circ dstl \circ (id \times (f + id)) \\
@ -116,7 +117,8 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
We are left to check the equational lifting law:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ==
\[\begin{tikzcd}
\[
\begin{tikzcd}
{X+1} &&& {(X+1)\times(X+1)} \\
\\
&&& {((X+1)\times X) +((X+1)\times 1)} \\
@ -126,22 +128,23 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rig
\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}\]
\end{tikzcd}
\]
This is easily proven by pre-composing with $i_1$ and $i_2$:
This is easily proven by pre-composing with \(i_1\) and \(i_2\):
\begin{alignat*}{1}
&(id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle
& (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*}
\begin{alignat*}{1}
&(id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle
& (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\; !
\\=\;&i_2 \;\circ \; ! \circ \langle i_2 , id \rangle
\\=\;&i_2 \;\circ \; !
\end{alignat*}
\end{proof}
@ -150,26 +153,26 @@ In the setting of classical mathematics this monad is therefore sufficient for m
\section{The Delay Monad}
\todo[inline]{Take introduction from setoids chapter and put it here!}
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
This monad is usually defined by the two coinductive constructors $now$ and $later$, where $now$ is for lifting a value to a computation and $later$ intuitively delays a computation by one time unit:
This monad is usually defined by the two coinductive constructors \(now\) and \(later\), where \(now\) is for lifting a value to a computation and \(later\) intuitively delays a computation by one time unit:
\todo[inline]{Explain convention of double lines vs single lines ==> remove double lines here!!}
\[\mprset{fraction={===}}
\inferrule {x : X} {now\; x : DX}\hskip 2cm
\inferrule {x : X} {now\; x : DX}\qquad
\inferrule {c : DX} {later\; c : DX}\]
Categorically we obtain this monad by the final coalgebras $DX = \nu A. X + A$, which we assume to exist. In this section we will show that $\mathbf{D}$ is a strong and commutative monad.
Categorically we obtain this monad by the final coalgebras \(DX = \nu A. X + A\), which we assume to exist. In this section we will show that \(\mathbf{D}\) is a strong and commutative monad.
Since $DX$ is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By Lambek's lemma 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$.
Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By Lambek's lemma 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}
The following conditions hold:
\begin{itemize}
\item $now : X \rightarrow DX$ and $later : DX \rightarrow DX$ satisfy:
\item \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\) satisfy:
\begin{equation*}
out \circ now = i_1 \qquad\qquad\qquad out \circ later = i_2 \tag*{(D1)}\label{D1}
\end{equation*}
\item For any $f : X \rightarrow DY$ there exists a unique morphism $f^* : DX \rightarrow DY$ satisfying:
\item For any \(f : X \rightarrow DY\) there exists a unique morphism \(f^* : DX \rightarrow DY\) satisfying:
\begin{equation*}
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIlggKyBEWCJdLFswLDEsIkRZIl0sWzMsMSwiWSArIERZIl0sWzAsMSwib3V0Il0sWzAsMiwiZl4qIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywib3V0Il0sWzEsMywiWyBvdXQgXFxjaXJjIGYgLCBpXzIgXFxjaXJjIGZeKiBdIl1d
\begin{tikzcd}
@ -179,9 +182,10 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
\arrow["{f^*}", dashed, from=1-1, to=2-1]
\arrow["out", from=2-1, to=2-4]
\arrow["{[ out \circ f , i_2 \circ f^* ]}", from=1-4, to=2-4]
\end{tikzcd}\tag*{(D2)}\label{D2}
\end{tikzcd}
\tag*{(D2)}\label{D2}
\end{equation*}
\item There exists a unique morphism $\tau : X \times DY \rightarrow D(X \times Y)$ satisfying:
\item There exists a unique morphism \(\tau : X \times DY \rightarrow D(X \times Y)\) satisfying:
\begin{equation*}
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
\begin{tikzcd}[ampersand replacement=\&]
@ -192,22 +196,24 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
\arrow["dstl", from=1-3, to=1-5]
\arrow["{id +\tau}"', from=1-5, to=2-5]
\arrow["out", from=2-1, to=2-5]
\end{tikzcd}\tag*{(D3)}\label{D3}
\end{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 final coalgebra:
We will make use of the fact that every \(DX\) is a final coalgebra:
\begin{itemize}
\item[\ref{D1}] These follow by definition:
\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:
\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=\&]
\[
\begin{tikzcd}[ampersand replacement=\&]
DX \\
{DX + DY} \&\&\&\&\&\&\& {Y + (DX + DY)} \\
DY \&\&\&\&\&\&\& {Y + DY}
@ -216,19 +222,20 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
\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}\]
\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:
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:
\begin{alignat*}{1}
&out \circ \coalg{\alpha} \circ i_2
& 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:
Let us verify that \(f^*\) indeed satisfies the requisite property:
\begin{alignat*}{1}
&out \circ \coalg{\alpha} \circ i_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
@ -236,96 +243,97 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
\\=\;&[ 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:
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:
\begin{alignat*}{1}
&out \circ [ g , id ]
& 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 , (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}$.
Thus, \([ g , id ] = \coalg{\alpha}\) by uniqueness of \(\coalg{\alpha}\).
It follows: \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*\]
\item[\ref{D3}] This follows immediately since $\tau$ is the unique coalgebra morphism from $(X \times DY, dstl \circ (id \times out))$ into the terminal coalgebra $(D(X \times Y) , out)$.
\item[\ref{D3}] This follows immediately since \(\tau \) is the unique coalgebra morphism from \((X \times DY, dstl \circ (id \times out))\) into the terminal coalgebra \((D(X \times Y) , out)\).
\end{itemize}
\end{proof}
\begin{lemma}
The following properties follow from \autoref{lem:delay}:
\begin{enumerate}
\item $out \circ Df = (f + Df) \circ out$
\item $f^* = [ f , {(later \circ f)}^* ] \circ out$
\item $later \circ f^* = {(later \circ f)}^* = f^* \circ later$
\item \(out \circ Df = (f + Df) \circ out\)
\item \(f^* = [ f , {(later \circ f)}^* ] \circ out\)
\item \(later \circ f^* = {(later \circ f)}^* = f^* \circ later\)
\end{enumerate}
\end{lemma}
\begin{proof}
\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.]
These equations follow 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*}
\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.]
These equations follow 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}
\end{proof}
\begin{theorem}
$\mathbf{D} = (D, now, (-)^*)$ is a Kleisli triple.
\(\mathbf{D} = (D, now, {(-)}^*)\) is a Kleisli triple.
\end{theorem}
\begin{proof}
We will now use the properties proven in Corollary~\ref{lem:delay} to prove the Kleisli triple laws:
\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*}
By uniqueness of \(now^*\) it suffices to show that \(out \circ id = [ out \circ now , i_2 \circ id ] \circ out\) which instantly follows by~\ref{D1}.
\item[\ref{K2}] Let \(f : X \rightarrow DY\). We proceed by monicity of \(out\):
\begin{alignat*}{1}
& out \circ f^* \circ now
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ now\tag*{\ref{D2}}
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_1\tag*{\ref{D1}}
\\=\;&out \circ f
\end{alignat*}
\item[\ref{K3}] Let \(f : Y \rightarrow Z, g : X \rightarrow Z\) to show \(f^* \circ g^* = {(f^* \circ g)}^*\) by uniqueness of \({(f^* \circ g)}^*\) it suffices to show:
\begin{alignat*}{1}
& out \circ f^* \circ g^*
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ g^*\tag*{\ref{D2}}
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ [ out \circ g , i_2 \circ g^* ] \circ out\tag*{\ref{D2}}
\\=\;&[ [ out \circ f , i_2 \circ f^* ] \circ out \circ g , i_2 \circ f^* \circ g^* ] \circ out
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out\tag*{\ref{D2}}
\end{alignat*}
\end{itemize}
\end{proof}
Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ yields the following proof principle:
Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}}\) yields the following proof principle:
\begin{remark}[Proof by coinduction]~\label{rem:coinduction}
Given two morphisms $f, g : X \rightarrow DY$. To show that $f = g$ it suffices to show that there exists a coalgebra structure $\alpha : X \rightarrow Y + X$ such that the following diagrams commute:
Given two morphisms \(f, g : X \rightarrow DY\). To show that \(f = g\) it suffices to show that there exists a coalgebra structure \(\alpha : X \rightarrow Y + X\) such that the following diagrams commute:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
\[
\begin{tikzcd}[ampersand replacement=\&]
X \&\& {Y + X} \&\& X \&\& {Y + X} \\
DY \&\& {Y + DY} \&\& DY \&\& {Y + DY}
\arrow["out", from=2-1, to=2-3]
@ -336,21 +344,23 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
\arrow["g", from=1-5, to=2-5]
\arrow["{id + g}", from=1-7, to=2-7]
\arrow["out", from=2-5, to=2-7]
\end{tikzcd}\]
Uniqueness of the coalgebra morphism $\coalg{\alpha} : (X, \alpha) \rightarrow (DY, out)$ then results in $f = g$.
\end{tikzcd}
\]
Uniqueness of the coalgebra morphism \(\coalg{\alpha} : (X, \alpha) \rightarrow (DY, out)\) then results in \(f = g\).
\end{remark}
\begin{theorem}
$\mathbf{D}$ is a strong monad.
\(\mathbf{D}\) is a strong monad.
\end{theorem}
\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\]
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=\&]
\[
\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)}
@ -360,15 +370,17 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
\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
\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:
\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=\&]
\[
\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]
@ -377,12 +389,13 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
\arrow["{id \times out}", from=1-1, to=1-2]
\arrow["dstl", from=1-2, to=1-3]
\arrow["{\pi_2 + id}", from=1-3, to=1-4]
\end{tikzcd}\]
\item[\ref{S2}] We don't need coinduction to show $\tau \circ (id \times now) = now$, but we need a small helper lemma:
\end{tikzcd}
\]
\item[\ref{S2}] We don't need coinduction to show \(\tau \circ (id \times now) = now\), but we need a small helper lemma:
\begin{equation*}
\tau \circ (id \times out^{-1}) = out^{-1} \circ (id + \tau) \circ dstl \tag*{($\ast$)}\label{helper}
\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}.
which is a direct consequence of~\ref{D3}.
With this the proof is straightforward:
\begin{alignat*}{1}
& \tau \circ (id \times now) \\
@ -390,10 +403,11 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
=\; & out^{-1} \circ (id + \tau) \circ dstl \circ (id \times i_1)\tag*{\ref*{helper}} \\
=\; & now
\end{alignat*}
where the last step follows by $dstl \circ (id \times i_1) = i_1$.
\item[\ref{S3}] We need to check $\tau^* \circ \tau = \tau \circ (id \times id^*)$, the coalgebra for coinduction is:
where the last step follows by \(dstl \circ (id \times i_1) = i_1\).
\item[\ref{S3}] We need to check \(\tau^* \circ \tau = \tau \circ (id \times id^*)\), the coalgebra for coinduction is:
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXGNvYWxney19IiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
\[
\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)}
@ -403,10 +417,12 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
\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:
\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=\&]
\[
\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)}
@ -416,37 +432,40 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$
\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{tikzcd}
\]
\end{itemize}
\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:
To prove that \(\mathbf{D}\) is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
\begin{definition}
We call a morphism $g : X \rightarrow D (Y + X)$ \textit{guarded} if there exists an $h : X \rightarrow Y + D(Y+X)$ such that the following diagram commutes:
We call a morphism \(g : X \rightarrow D (Y + X)\) \textit{guarded} if there exists an \(h : X \rightarrow Y + D(Y+X)\) such that the following diagram commutes:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
\[\begin{tikzcd}[ampersand replacement=\&]
\[
\begin{tikzcd}[ampersand replacement=\&]
X \&\&\& {D (Y +X)} \\
{Y + D(Y+X)} \&\&\& {(Y + X) + D(Y + X)}
\arrow["g", from=1-1, to=1-4]
\arrow["out", from=1-4, to=2-4]
\arrow["{i_1 + id}"', from=2-1, to=2-4]
\arrow["h"', from=1-1, to=2-1]
\end{tikzcd}\]
\end{tikzcd}
\]
\end{definition}
\begin{corollary}[Solution Theorem]
\label{cor:solution}
Let $g : X \rightarrow D(Y + X)$ be guarded. \textit{Solutions} of g are unique, i.e. given two morphisms $f, i : X \rightarrow DY$ then
$f = [ now , f ]^* \circ g$ and $i = [ now , i ]^* \circ g$ already implies $f = i$.
\begin{corollary}[Solution Theorem]\label{cor:solution}
Let \(g : X \rightarrow D(Y + X)\) be guarded.\ \textit{Solutions} of g are unique, i.e.\ given two morphisms \(f, i : X \rightarrow DY\) then
\(f = {[ now , f ]}^* \circ g\) and \(i = {[ now , i ]}^* \circ g\) already implies \(f = i\).
\end{corollary}
\begin{proof}
Let $g : X \rightarrow D(Y + X)$ be guarded by $h : X \rightarrow Y + D(Y+X)$ and $f, i : X \rightarrow DY$ be solutions of g.
It suffices to show $[ now , f ]^* = [ now , i ]^*$, because then follows:
\[f = [ now , f ]^* \circ g = [ now , i ]^* \circ g = i\]
Let \(g : X \rightarrow D(Y + X)\) be guarded by \(h : X \rightarrow Y + D(Y+X)\) and \(f, i : X \rightarrow DY\) be solutions of g.
It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows:
\[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i\]
We prove this by coinduction using:
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[\begin{tikzcd}[ampersand replacement=\&]
\[
\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]
@ -454,18 +473,19 @@ To prove that $\mathbf{D}$ is commutative we will use another proof principle pr
\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}\]
\end{tikzcd}
\]
\end{proof}
Let us record some facts that we will use to prove commutativity of $\mathbf{D}$:
Let us record some facts that we will use to prove commutativity of \(\mathbf{D}\):
\begin{corollary}
These properties of $\tau$ and $\sigma$ hold:
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}
\\&out \circ \sigma &&= (id + \sigma) \circ dstr \circ (out \times id)\tag*{($\sigma_1$)}\label{sigma1}
\\&\tau \circ (id \times out^{-1}) &&= out^{-1} \circ (id + \tau) \circ dstl\tag*{($\tau_2$)}\label{tau2}
\\& \sigma \circ (out^{-1} \times id) &&= out^{-1} \circ (id + \sigma) \circ dstr\tag*{($\sigma_2$)}\label{sigma2}
& out \circ \tau & & = (id + \tau) \circ dstl \circ (id \times out)\tag*{(\(\tau_1\))}\label{tau1}
\\&out \circ \sigma &&= (id + \sigma) \circ dstr \circ (out \times id)\tag*{(\(\sigma_1\))}\label{sigma1}
\\&\tau \circ (id \times out^{-1}) &&= out^{-1} \circ (id + \tau) \circ dstl\tag*{(\(\tau_2\))}\label{tau2}
\\& \sigma \circ (out^{-1} \times id) &&= out^{-1} \circ (id + \sigma) \circ dstr\tag*{(\(\sigma_2\))}\label{sigma2}
\end{alignat*}
\end{corollary}
@ -473,48 +493,48 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
\begin{itemize}
\item[\ref{tau1}] This is just~\ref{D3} restated.
\item[\ref{sigma1}]
\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}] 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
\end{alignat*}
\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}] 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
\end{alignat*}
\end{itemize}
\end{proof}
\begin{theorem}
$\mathbf{D}$ is 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$.
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
Let \(w = (dstr + dstr) \circ dstl \circ (out \times out)\) and take
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\]
$g$ is trivially guarded by $[ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$.
\(g\) is trivially guarded by \([ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\).
We are left to show that both $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of $g$. Consider:
We are left to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider:
\[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = [ now , \tau^* \circ \sigma]^* \circ g \]
\[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = [ now , \sigma^* \circ \tau]^* \circ g \]
\[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = {[ now , \tau^* \circ \sigma]}^* \circ g \]
\[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = {[ now , \sigma^* \circ \tau]}^* \circ g \]
The last step in both equations can be proven generally for any $f : DX \times DY \rightarrow D(X \times Y)$ using monicity of $out$:
The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\):
\begin{alignat*}{1}
& out \circ {[ now , f ]}^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w
& out \circ {[ now , f ]}^* \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
@ -522,9 +542,9 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
\\=\; & [ 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.
Let us now check the first step in the equation for \(\sigma^* \circ \tau \), the same step for \(\tau^* \circ \sigma \) is then symmetric.
Again we proceed by monicity of $out$:
Again we proceed by monicity of \(out\):
\begin{alignat*}{1}
& out \circ \sigma^* \circ \tau
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
@ -533,19 +553,19 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
\\=\;&[ (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) \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}\]
is proven using epicness of $dstr^{-1}$:
is proven using epicness of \(dstr^{-1}\):
\begin{alignat*}{1}
& Ddstr \circ \tau \circ dstr^{-1}
@ -556,6 +576,6 @@ Let us record some facts that we will use to prove commutativity of $\mathbf{D}$
\end{proof}
\improvement[inline]{Elaborate more?}
We have now seen that $\mathbf{D}$ is strong and commutative, however it is not an equational lifting monad, since besides modelling 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.
We have now seen that \(\mathbf{D}\) is strong and commutative, however it is not an equational lifting monad, since besides modelling 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.
In chapter~\ref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored. This will then yield an equational lifting monad on the category of setoids. However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient. Chapman et al. have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of $\mathbf{D}$.
In \autoref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored. This will then yield an equational lifting monad on the category of setoids. However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient. Chapman et al.\ have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of \(\mathbf{D}\).

916
thesis/src/04_iteration.tex
View file

File diff suppressed because it is too large Load diff

126
thesis/src/05_setoids.tex
View file

@ -1,35 +1,35 @@
\chapter{A Case Study on Setoids}\label{chp:setoids}
In chapter~\ref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e. we will work in the category of setoids and show that the quotiented delay monad is the initial pre-Elgot monad in this category.
In \autoref{chp:partiality} we have argued that the delay monad is not an equational lifting monad, because it does not only model partiality, but it also respects computation time. One way to remedy this is to take the quotient of the delay monad where computations with the same result are identified. In this chapter we will use the quotients-as-setoid approach, i.e. we will work in the category of setoids and show that the quotiented delay monad is the initial pre-Elgot monad in this category.
Let us introduce the category that we are working in:
\section{Setoids in Type Theory}
\begin{definition}[Setoid]
A setoid is a tuple $(A, \hat{=})$ where $A$ (usually called the \textit{carrier}) is a type and $\hat{=}$ an equivalence relation on the inhabitants of $A$.
A setoid is a tuple \((A, \hat{=})\) where \(A\) (usually called the \textit{carrier}) is a type and \(\hat{=}\) an equivalence relation on the inhabitants of \(A\).
\end{definition}
Morphisms between setoids are functions that respect the equivalence relation:
Morphisms between setoids are functions that respect the equivalence relation.
\begin{definition}[Setoid Morphism]
A morphism between two setoids $(A , =^A)$ and $(B , =^B)$ is a function $f : A \rightarrow B$ such that $x =^A y$ implies $fx =^B fy$ for any $x, y : A$.
A morphism between two setoids \((A , =^A)\) and \((B , =^B)\) is a function \(f : A \rightarrow B\) such that \(x =^A y\) implies \(fx =^B fy\) for any \(x, y : A\).
\end{definition}
Setoids and setoid morphisms form a category that we call $\setoids$.
Setoids and setoid morphisms form a category that we call \(\setoids\).
\improvement[inline]{Talk about equality between setoid morphisms}
\improvement[inline]{Text is not good}
\begin{lemma}
$\setoids$ is a distributive category.
\(\setoids\) is a distributive category.
\end{lemma}
\begin{proof}
To show that $\setoids$ is (co-)cartesian we will give the respective data types and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the Agda standard library.
To show that \(\setoids\) is (co-)cartesian we will give the respective data types and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the Agda standard library.
\begin{itemize}
\item \textbf{Products}:
\begin{minted}{agda}
\begin{minted}{agda}
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
constructor _,_
field
@ -41,7 +41,7 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
< f , g > x = (f x , g x)
\end{minted}
\item \textbf{Terminal Object}:
\begin{minted}{agda}
\begin{minted}{agda}
record ⊤ {l} : Set l where
constructor tt
@ -49,7 +49,7 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
! _ = tt
\end{minted}
\item \textbf{Coproducts}:
\begin{minted}{agda}
\begin{minted}{agda}
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
i₁ : A → A + B
i₂ : B → A + B
@ -60,7 +60,7 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
[ f , g ] (i₂ x) = g x
\end{minted}
\item \textbf{Initial Object}:
\begin{minted}{agda}
\begin{minted}{agda}
data ⊥ {l} : Set l where
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
@ -68,7 +68,7 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
\end{minted}
\end{itemize}
Lastly we need to show that the canonical distributivity morphism is an iso. Recall that the canonical distributive 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 corresponds to the following definition using pattern matching:
Lastly we need to show that the canonical distributivity morphism is an iso. Recall that the canonical distributive 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 corresponds to the following definition using 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)
@ -86,11 +86,11 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
\end{proof}
\begin{lemma}
$\setoids$ is cartesian closed.
\(\setoids\) is cartesian closed.
\end{lemma}
\begin{proof}
We have already shown that $\setoids$ is cartesian, we need to show that given two setoids $(A, =^A), (B, =^B)$ we can construct an exponential object.
Indeed, take the function space setoid $(A \rightarrow B, \doteq)$ where $\doteq$ is point wise equality of setoid morphisms i.e. $f , g : A \rightarrow B$ are point wise equal $f \doteq g$ \textit{iff} $f x =^B g x$ for any $x : A$. $curry$ and $eval$ are then defined as usual:
We have already shown that \(\setoids\) is cartesian, we need to show that given two setoids \((A, =^A), (B, =^B)\) we can construct an exponential object.
Indeed, take the function space setoid \((A \rightarrow B, \doteq)\) where \(\doteq\) is point wise equality of setoid morphisms i.e. \(f , g : A \rightarrow B\) are point wise equal \(f \doteq g\) \textit{iff} \(f x =^B g x\) for any \(x : A\). \(curry\) and \(eval\) are then defined as usual:
\begin{minted}{agda}
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
→ (C × A → B) → C → A → B
@ -103,9 +103,9 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
\section{Quotienting the Delay Monad}
% TODO merge this into introduction
% Chapman et al. have already proven that quotienting the delay datatype by weak bisimilarity using the quotients-as-setoids approach yields a monad~\cite{quotienting}, we will build upon their results and show that this quotient is indeed an instance of our monad $\mathbf{K}$.
% Chapman et al. have already proven that quotienting the delay datatype by weak bisimilarity using the quotients-as-setoids approach yields a monad~\cite{quotienting}, we will build upon their results and show that this quotient is indeed an instance of our monad \(\mathbf{K}\).
% Historically proof assistants like Agda and Coq have been offering multiple ways of defining coinductive types, nowadays the manuals of both Agda and Coq advise users to use coinductive records instead of defining coinductive types by constructors, we will heed this advice.
% Since the delay monad is usually defined by the constructors $now$ and $later$
% Since the delay monad is usually defined by the constructors \(now\) and \(later\)
Originally the delay monad has been introduced as a coinductive datatype with two constructors, in pseudo Agda like code this would look something like:
\begin{minted}{agda}
@ -133,43 +133,43 @@ Here \Verb{Delay} is defined as an inductive datatype where the coinductive part
For the sake of readability we will introduce other concepts only by inference rules instead of Agda code, for the delay monad this looks like:
\[
\inferrule*{x : A}{now\; x : Delay \;A} \hskip 1cm
\inferrule*{x : Delay' \;A}{later \;x : Delay\; A} \hskip 1cm
\mprset{fraction={===}}\inferrule*{x : Delay' \;A}{force \;x : Delay \;A}
\inferrule*{x : A}{now\; x : Delay \;A} \hskip 1cm
\inferrule*{x : Delay' \;A}{later \;x : Delay\; A} \hskip 1cm
\mprset{fraction={===}}\inferrule*{x : Delay' \;A}{force \;x : Delay \;A}
\]
We will now introduce two notions of equality on inhabitants of the delay type, given a setoid $(A, =^A)$ we call the equivalence received by lifting $=^A$ to $Delay\;A$ \textit{strong bisimilarity}, the definition is as follows:
We will now introduce two notions of equality on inhabitants of the delay type, given a setoid \((A, =^A)\) we call the equivalence received by lifting \(=^A\) to \(Delay\;A\) \textit{strong bisimilarity}, the definition is as follows:
\[
\inferrule*{eq : x =^A y}{now \;eq : x \sim y} \hskip 1cm
\inferrule*{eq : force \;x \sim' force\; y}{later\;eq : later\; x \sim later\; y} \hskip 1cm
\mprset{fraction={===}}\inferrule*{eq : x \sim' y}{force\; eq : x \sim y}
\inferrule*{eq : x =^A y}{now \;eq : x \sim y} \hskip 1cm
\inferrule*{eq : force \;x \sim' force\; y}{later\;eq : later\; x \sim later\; y} \hskip 1cm
\mprset{fraction={===}}\inferrule*{eq : x \sim' y}{force\; eq : x \sim y}
\]
\begin{lemma}
$(Delay\;A, \sim)$ is a setoid.
\((Delay\;A, \sim)\) is a setoid.
\end{lemma}
In $(Delay\;A, \sim)$ computations that evaluate to the same result but in a different amount of time are not equal. We will now build the quotient of this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
In \((Delay\;A, \sim)\) computations that evaluate to the same result but in a different amount of time are not equal. We will now build the quotient of this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
\[
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \hskip 1cm
\inferrule*{d : force\;x \downarrow c}{later\;d : later\;x \downarrow c }
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \hskip 1cm
\inferrule*{d : force\;x \downarrow c}{later\;d : later\;x \downarrow c }
\]
Now we can relate two computations \textit{iff} they evaluate to the same result:
\[
\inferrule*{eq : a =^A b \\ xa : x \downarrow a \\ yb : y \downarrow b}{\downarrow\approx \; eq \; xa \; yb : x \approx y} \hskip 1cm
\inferrule*{eq : force \;x \approx' force \;y}{later\;eq : later \;x \approx later \;y} \hskip 1cm
\mprset{fraction={===}}\inferrule*{eq : x \approx' y}{force\;eq : x \approx y}
\inferrule*{eq : a =^A b \\ xa : x \downarrow a \\ yb : y \downarrow b}{\downarrow\approx \; eq \; xa \; yb : x \approx y} \hskip 1cm
\inferrule*{eq : force \;x \approx' force \;y}{later\;eq : later \;x \approx later \;y} \hskip 1cm
\mprset{fraction={===}}\inferrule*{eq : x \approx' y}{force\;eq : x \approx y}
\]
\begin{lemma}
$(Delay\;A, \approx)$ is a setoid.
\((Delay\;A, \approx)\) is a setoid.
\end{lemma}
\begin{theorem}
$(Delay\;A, \approx)$ is a monad.
\((Delay\;A, \approx)\) is a monad.
\end{theorem}
\begin{proof}
The monad unit is the constructor \Verb{now} and monad multiplication can be defined as follows:
@ -186,53 +186,53 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
\end{proof}
\begin{theorem}
$(Delay\;A , \approx)$ is an instance of $\mathbf{K}$ in the category $\setoids$.
\((Delay\;A , \approx)\) is an instance of \(\mathbf{K}\) in the category \(\setoids\).
\end{theorem}
\begin{proof}
We need to show that for every setoid $(A, =^A)$ the resulting setoid $(Delay\;A, \approx)$ can be extended to a stable free Elgot algebra.
Stability follows automatically by theorem~\ref{thm:stability} and the fact that $\setoids$ is cartesian closed, so it suffices to define a free Elgot Algebra on $(Delay\;A, \approx)$.
We need to show that for every setoid \((A, =^A)\) the resulting setoid \((Delay\;A, \approx)\) can be extended to a stable free Elgot algebra.
Stability follows automatically by theorem~\ref{thm:stability} and the fact that \(\setoids\) is cartesian closed, so it suffices to define a free Elgot Algebra on \((Delay\;A, \approx)\).
Let $(X , =^X) \in \obj{\setoids}$ and $f : X \rightarrow Delay\; A + X$ be a setoid morphism, we define $f^\# : X \rightarrow Delay\;A$ point wise:
Let \((X , =^X) \in \obj{\setoids}\) and \(f : X \rightarrow Delay\; A + X\) be a setoid morphism, we define \(f^\# : X \rightarrow Delay\;A\) point wise:
\[
f^\# (x) :=
\begin{cases}
a & \text{if } f\;x = i_1 (a)\\
later\;(f^{\#'} a) & \text{if } f\;x = i_2 (a)
\end{cases}
f^\# (x) :=
\begin{cases}
a & \text{if } f\;x = i_1 (a) \\
later\;(f^{\#'} a) & \text{if } f\;x = i_2 (a)
\end{cases}
\]
where $f^{\#'} : X \rightarrow Delay'\;A$ is defined corecursively by:
where \(f^{\#'} : X \rightarrow Delay'\;A\) is defined corecursively by:
\[
force (f^{\#'}(x)) = f^\#(x)
force (f^{\#'}(x)) = f^\#(x)
\]
Let us first show that $f^\#$ is a setoid morphism, i.e. given $x, y : X$ with $x =^X y$, we need to show that $f^\#(x) = f^\#(y)$. Since $f$ is a setoid morphism we know that $f(x) =^+ f(y)$ in the coproduct setoid $(Delay\;A + X, =^+)$. We proceed by case distinction on $f(x)$:
Let us first show that \(f^\#\) is a setoid morphism, i.e. given \(x, y : X\) with \(x =^X y\), we need to show that \(f^\#(x) = f^\#(y)\). Since \(f\) is a setoid morphism we know that \(f(x) =^+ f(y)\) in the coproduct setoid \((Delay\;A + X, =^+)\). We proceed by case distinction on \(f(x)\):
\begin{itemize}
\item Case $f(x) = i_1 (a)$:
\[f^\# (x) = a = f^\#(y)\]
\item Case $f(x) = i_2 (a)$:
\[f^\# (x) = later (f^{\#'}(a)) = f^\# (y)\]
\item Case \(f(x) = i_1 (a)\):
\[f^\# (x) = a = f^\#(y)\]
\item Case \(f(x) = i_2 (a)\):
\[f^\# (x) = later (f^{\#'}(a)) = f^\# (y)\]
\end{itemize}
Now we check the iteration laws:
\change[inline]{change the equivalence sign of coproducts}
\change[inline]{change the equivalence sign of coproducts}
\begin{itemize}
\item \textbf{Fixpoint}: We need to show that $f^\# (x) \approx ([ id , f^\# ] \circ f)(x)$:
\begin{itemize}
\item Case $f(x) =^+ i_1 (a)$:
\[ f^\#(x) \approx a \approx [ id , f^\# ] (i_1 (a)) = ([ id , f^\# ] \circ f) (x) \]
\item Case $f(x) =^+ i_2 (a)$:
\[ f^\#(x) \approx later (f^{\#'}(a)) \overset{(*)}{\approx} f^\#(a) \approx [ id , f^\# ] (i_2 (a)) \approx ([ id , f^\# ] \circ f) (x)\]
\end{itemize}
where $(*)$ follows from a general fact: any $z : Delay'\;A$ satisfies $force\;z \approx later\;z$.
\item \textbf{Uniformity}: Let $(Y , =^Y) \in \setoids$ and $g : Y \rightarrow Delay\; A + Y, h : X \rightarrow Y$ be setoid morphisms with $(id + h) \circ f = g \circ h$.
\item \textbf{Fixpoint}: We need to show that \(f^\# (x) \approx ([ id , f^\# ] \circ f)(x)\):
\begin{itemize}
\item Case \(f(x) =^+ i_1 (a)\):
\[ f^\#(x) \approx a \approx [ id , f^\# ] (i_1 (a)) = ([ id , f^\# ] \circ f) (x) \]
\item Case \(f(x) =^+ i_2 (a)\):
\[ f^\#(x) \approx later (f^{\#'}(a)) \overset{(*)}{\approx} f^\#(a) \approx [ id , f^\# ] (i_2 (a)) \approx ([ id , f^\# ] \circ f) (x)\]
\end{itemize}
where \((*)\) follows from a general fact: any \(z : Delay'\;A\) satisfies \(force\;z \approx later\;z\).
\item \textbf{Uniformity}: Let \((Y , =^Y) \in \setoids\) and \(g : Y \rightarrow Delay\; A + Y, h : X \rightarrow Y\) be setoid morphisms with \((id + h) \circ f = g \circ h\).
\item \textbf{Folding}:
\end{itemize}
\end{proof}

129
thesis/src/examples.tex
View file

@ -1,129 +0,0 @@
\chapter{Some Introduction and Examples}
You can freely use the present template for your final thesis (i.e.~master or
bachelor or project thesis).
This template was made from the following theses:
\begin{itemize}
\item \url{http://thorsten-wissmann.de/theses/ma-wissmann.pdf}
\item \url{http://thorsten-wissmann.de/theses/project-wissmann.pdf}
\item \url{http://thorsten-wissmann.de/theses/bachelor-thesis-wissmann.pdf}
\end{itemize}
\section{Meaning}
It is not mandatory at all to use this template for your final thesis. It is
just a suggestion! You are also allowed to change anything you would like to
change in order to fit your needs/taste/$\ldots$.
Of course, you should adjust some places when using it for your final thesis:
\begin{enumerate}
\item In the parameters to the \texttt{hyperref}-package, you should adjust the
fields \texttt{pdfauthor} and \texttt{pdftitle} to your name and the title of
your thesis.
\item In \texttt{src/titlepage.tex} you should adjust the title and (possibly
the) subtitle of your thesis, the degree of your thesis (Masters degree?
Bachelor?), your name and the name of your advisors.
\end{enumerate}
\section{Some hints}
\subsection{Macros}
% some macros only needed for these hints here
\newcommand{\C}{\ensuremath{\mathcal{C}}\xspace}
\newcommand{\preview}[2]{
\begin{center}
\fbox{\begin{minipage}[t]{.47\textwidth}
#1
\end{minipage}}%
\hspace{.02\textwidth}%
\fbox{\begin{minipage}[t]{.47\textwidth}
#2
\end{minipage}}%
\end{center}}
When using certain mathematical symbols very often, it makes sense to define
macros for them, e.g.~
\begin{verbatim}
\newcommand{\C}{\ensuremath{\mathcal{C}}\xspace}
\end{verbatim}
The \texttt{ensuremath} enforces mathmode and the \texttt{xspace} inserts a
space if necessary:
\preview{
\Verb|Some \textbackslash C in the midle of the sentence|
\Verb|and at the end: \textbackslash C.|
}{
Some \C in the midle of the sentence
and at the end: \C.
}
\subsection{UTF-8}
I strongly recommend exploiting the utf8 capability of \LaTeX:
\begin{verbatim}
\usepackage{newunicodechar}
\newunicodechar{∀}{\ensuremath{\forall}}
\newunicodechar{∃}{\ensuremath{\exists}}
\newunicodechar{×}{\ensuremath{\times}}
\newunicodechar{ø}{\ensuremath{\emptyset}}
\newunicodechar{≤}{\ensuremath{\le}}
\newunicodechar{∈}{\ensuremath{\in}}
\newunicodechar{→}{\ensuremath{\to}}
\newunicodechar{⊆}{\ensuremath{\subseteq}}
\newunicodechar{⊗}{\ensuremath{\otimes}}
\newunicodechar{∧}{\ensuremath{\wedge}}
\end{verbatim}
with that, you can write:
\begin{verbatim}
\begin{definition}[Transitivity]
A relation $\text{``}≤\text{''} ⊆ X×X$ has upper bounds if
\[
∀a,b ∈ X\ ∃ c ∈ X: a ≤ c ∧ b ≤ c
\]
\end{definition}
\end{verbatim}
It will result in the following:
\begin{definition}[Transitivity]
A relation $\text{``}≤\text{''} ⊆ X×X$ has upper bounds if
\[
∀a,b ∈ X\ ∃ c ∈ X: a ≤ c ∧ b ≤ c
\]
\end{definition}
In order to input unicode characters, just configure a compose key, e.g.:
\begin{itemize}
\item \url{https://en.wikipedia.org/wiki/Compose_key}
\item
\url{https://wiki.archlinux.org/index.php/Keyboard_configuration_in_Xorg#Configuring_compose_key}
\end{itemize}
\subsection{Autoref}
Let \LaTeX~include whether something references is a definition or what else
using the \texttt{\textbackslash autoref} command:
\begin{verbatim}
\begin{definition}[label={relation},name={Relation}]
A relation $R$ between sets $X$ and $Y$ is just a subset of $X×Y$.
\end{definition}
We have just seen \autoref{relation}.
\end{verbatim}
This results in:
\begin{definition}[label={relation},name={Relation}]
A relation $R$ between sets $X$ and $Y$ is just a subset of $X×Y$.
\end{definition}
We have just seen \autoref{relation}.
\subsection{Further Comments}
For even more convenience while writing, you should look at the following:
synctex, git (for managing your \TeX-sources).
% vim: tw=80 nospell spelllang=en nocul