mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Compare commits
3 commits
a3f077bd8d
...
96f9bf4bb9
| Author | SHA1 | Date | |
|---|---|---|---|
96f9bf4bb9
|
|||
|
294392b212
|
|||
|
72c790f941
|
5 changed files with 162 additions and 112 deletions
|
|
@ -13,7 +13,7 @@
|
|||
frame=lines,
|
||||
autogobble
|
||||
}
|
||||
\usepackage[dvipsnames]{xcolor} % Coloured text etc.
|
||||
\usepackage[dvipsnames]{xcolor} % Coloured text etc.
|
||||
\usepackage{amssymb}
|
||||
\usepackage{amsthm}
|
||||
\usepackage{thmtools}
|
||||
|
|
@ -36,15 +36,12 @@
|
|||
\usepackage{makeidx}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{fvextra}
|
||||
\usepackage[style=ieee, sorting=ynt]{biblatex} %advanced citations
|
||||
\usepackage[english=british]{csquotes} %biblatex recommended to load this
|
||||
\usepackage[style=ieee, sorting=ynt]{biblatex} % advanced citations
|
||||
\usepackage[english=british]{csquotes} % biblatex recommended to load this
|
||||
\usepackage{etoolbox,xpatch}
|
||||
|
||||
\makeatletter
|
||||
\AtBeginEnvironment{minted}{\dontdofcolorbox}
|
||||
\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}
|
||||
\xpatchcmd{\inputminted}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{}
|
||||
\xpatchcmd{\mintinline}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{} % see https://tex.stackexchange.com/a/401250/
|
||||
\AtBeginEnvironment{minted}{\dontdofcolorbox}\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}\xpatchcmd{\inputminted}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{}\xpatchcmd{\mintinline}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{} % see https://tex.stackexchange.com/a/401250/
|
||||
\makeatother
|
||||
\usepackage{scrhack}
|
||||
|
||||
|
|
@ -54,11 +51,11 @@
|
|||
%\usepackage[justific=raggedright,totoc]{idxlayout}
|
||||
\usepackage[type=CC, modifier=by-sa,version=4.0]{doclicense}
|
||||
|
||||
\addto\extrasenglish{%
|
||||
\addto\extrasenglish{
|
||||
\renewcommand{\chapterautorefname}{Section}
|
||||
\renewcommand{\sectionautorefname}{Section}
|
||||
\renewcommand{\subsectionautorefname}{Subsection}
|
||||
}
|
||||
}
|
||||
|
||||
\newcommand\chap[1]{%
|
||||
\chapter*{#1}%
|
||||
|
|
@ -111,6 +108,7 @@
|
|||
|
||||
% category C
|
||||
\newcommand*{\C}{\ensuremath{\mathcal{C}}}
|
||||
\newcommand*{\D}{\ensuremath{\mathcal{D}}}
|
||||
% objects of category
|
||||
\newcommand*{\obj}[1]{\ensuremath{\vert #1 \vert}}
|
||||
% category of elgot algebras on #1
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
\chapter{Preliminaries}
|
||||
|
||||
\todo[inline]{Also note that we require some knowledge with type theory}
|
||||
|
||||
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$.
|
||||
|
|
@ -108,19 +110,57 @@ Categories with finite products (i.e. binary products and a terminal object) are
|
|||
\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. But in this thesis we will not assume a cartesian closed category as to be more general.
|
||||
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{Coalgebras}
|
||||
\todo[inline]{Maybe introduce (co-)induction here via (co-)algebras}
|
||||
\todo[inline]{introduce (terminal) coalgebras, proof lambeks lemma}
|
||||
|
||||
\section{Adjunctions and Free Objects}
|
||||
\todo[inline]{introduce adjunctions}
|
||||
|
||||
Free objects are constructions capturing the essence of structures in a minimal way, we will rely on free structures in chapter~\ref{chp:iteration} to define a monad in a general setting. We recall the definition to establish some notation:
|
||||
|
||||
\begin{definition}[Free Object]
|
||||
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 the following universal property holds for any $Y \in \obj{\C}$ and $f : X \rightarrow UY$:
|
||||
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxleGlzdHMhXFxsbGJyYWNrZXQgZiBcXHJyYnJhY2tldCIsMl1d
|
||||
\[\begin{tikzcd}
|
||||
X & UY \\
|
||||
FX
|
||||
\arrow["f", from=1-1, to=1-2]
|
||||
\arrow["\eta"', from=1-1, to=2-1]
|
||||
\arrow["{\exists!\llbracket f \rrbracket}"', from=2-1, to=1-2]
|
||||
\end{tikzcd}\]
|
||||
\end{definition}
|
||||
|
||||
\section{Monads}
|
||||
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 on a category $\C$ is a triple $(F, \eta, \mu)$, where $F : \C \rightarrow \C$ is an endofunctor and $\eta : Id \rightarrow F, \mu : F^2 \rightarrow F$ are natural transformations, satisfying the following laws:
|
||||
\begin{alignat*}{1}
|
||||
&\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X \tag*{(M1)}\label{M1}\\
|
||||
&\mu_X \circ \eta_{FX} = id_{FX} \tag*{(M2)}\label{M2}\\
|
||||
&\mu_X \circ F\eta_X = id_{FX} \tag*{(M3)}\label{M3}
|
||||
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}
|
||||
\end{alignat*}
|
||||
\todo[inline]{diagrams}
|
||||
|
||||
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}\]
|
||||
\end{definition}
|
||||
|
||||
Morphisms between monads are natural transformations that respect the monad operations:
|
||||
|
|
@ -148,17 +188,17 @@ Morphisms between monads are natural transformations that respect the monad oper
|
|||
\end{definition}
|
||||
|
||||
\begin{definition}[The Category of Monads]
|
||||
Monads on a category $\C$ together with monad morphisms yield a category that we call $\monads{\C}$. The identity morphism is the identity natural transformation that trivially respects the monad operations and composition of morphisms is composition of natural transformations.
|
||||
Monads on a category $\C$ together with monad morphisms form a category that we call $\monads{\C}$. The identity morphism is the identity natural transformation that trivially respects the monad operations and composition of morphisms is composition of natural transformations.
|
||||
\end{definition}
|
||||
|
||||
For programmers a second equivalent definition is more useful:
|
||||
|
||||
\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:
|
||||
\begin{alignat*}{1}
|
||||
&\eta_X^* = id_{FX} \tag*{(K1)}\label{K1}\\
|
||||
&\eta_X \circ f^* = f \tag*{(K2)}\label{K2}\\
|
||||
&f^* \circ g* = (f \circ g^*)^* \tag*{(K3)}\label{K3}
|
||||
A Kleisli triple on a category $\C$ is a triple $(F, \eta, (-)^*)$, where $F : \obj{C} \rightarrow \obj{C}$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\obj{C}}$ is a family of morphisms and for every morphism $f : X \rightarrow FY$ there exists a morphism $f^* : FX \rightarrow FY$ called the kleisli lifting, where the following laws hold:
|
||||
\begin{alignat*}{2}
|
||||
&\eta_X^* &&= id_{FX} \tag*{(K1)}\label{K1}\\
|
||||
&\eta_X \circ f^* &&= f \tag*{(K2)}\label{K2}\\
|
||||
&f^* \circ g* &&= (f \circ g^*)^* \tag*{(K3)}\label{K3}
|
||||
\end{alignat*}
|
||||
\end{definition}
|
||||
|
||||
|
|
@ -176,8 +216,8 @@ This results in the following:
|
|||
\begin{itemize}
|
||||
\item $\vert \C^T \vert = \obj{C}$
|
||||
\item $\mathcal{C^T}(X, Y) = \C(X, TY)$
|
||||
\item composition of $f : X \rightarrow TY$ and $g : Y \rightarrow TZ$ is defined as $f \circ_{\C^T} g = f^* \circ_{\C} g$.
|
||||
\item the identity morphisms are the unit morphisms of $T$, $id_X = \eta_X : X \rightarrow TX$
|
||||
\item Composition of $f : X \rightarrow TY$ and $g : Y \rightarrow TZ$ is defined as $f \circ_{\C^T} g = f^* \circ_{\C} g$.
|
||||
\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, making this indeed a category.
|
||||
\end{definition}
|
||||
|
|
@ -219,35 +259,27 @@ When modelling partiality with a monad, one would expect the following two progr
|
|||
\end{multicols}
|
||||
where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
|
||||
|
||||
\begin{definition}[Strong Monad] A monad $M$ on a cartesian category $\C$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times MY \rightarrow M(X \times Y)$, satisfying the following conditions:
|
||||
\begin{alignat*}{1}
|
||||
&M\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 M\tau_{X,Y} \circ \tau_{X,MY} \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,MZ} \tag*{(S4)}\label{S4}
|
||||
\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)$, satisfying 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}
|
||||
\end{alignat*}
|
||||
where $\alpha_{X,Y,Z} : X \times (Y \times Z) \rightarrow (X \times Y) \times Z$ is the obvious associativity morphism.
|
||||
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}
|
||||
|
||||
Now we can express the above condition:
|
||||
\begin{definition}[Commutative Monad]
|
||||
A strong monad $M$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength $\hat{\tau}_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap$. Concretely if the following equation holds:
|
||||
\[
|
||||
\tau_{X,Y}^* \circ \hat{\tau}_{X, MY} = \hat{\tau}_{X,Y}^* \circ \tau_{X, MY}
|
||||
\]
|
||||
\end{definition}
|
||||
|
||||
\section{Free Objects}
|
||||
Free objects are constructions capturing the essence of structures in a minimal way, we will rely on free structures in chapter~\ref{chp:iteration} to define a monad in a general setting. We recall the definition to establish some notation:
|
||||
|
||||
\begin{definition}[Free Object]
|
||||
Let $\C, \mathcal{D}$ be categories and $U : C \rightarrow D$ a forgetful functor (whose construction usually is obvious). A free object on some object $X \in \mathcal{D}$ is an object $FX \in \C$ together with a morphism $\eta : X \rightarrow UFX$ such that the following universal property holds for any $Y \in \obj{C}$ and $f : X \rightarrow UY$:
|
||||
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxleGlzdHMhXFxsbGJyYWNrZXQgZiBcXHJyYnJhY2tldCIsMl1d
|
||||
\[\begin{tikzcd}
|
||||
X & UY \\
|
||||
FX
|
||||
\arrow["f", from=1-1, to=1-2]
|
||||
\arrow["\eta"', from=1-1, to=2-1]
|
||||
\arrow["{\exists!\llbracket f \rrbracket}"', from=2-1, to=1-2]
|
||||
\end{tikzcd}\]
|
||||
A strong monad $\mathbf{T}$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength $\sigma_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap$. Concretely if the following equation holds:
|
||||
% 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}\]
|
||||
\end{definition}
|
||||
|
|
@ -1,12 +1,12 @@
|
|||
\chapter{Category Theory in Agda}
|
||||
|
||||
There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits are clear, having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
|
||||
Also ideally such a development will bring researchers together and enable them to work in a unified setting.
|
||||
In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library by Jason Hu and Jacques Carette that gives us a good foundation of categorical definitions to work with.
|
||||
There are many formalizations of category theory in proof assistants like Coq or Agda. The benefits of such a formalization are clear: having a usable formalization allows one to reason about categorical notions in a typechecked environment that makes errors less likely.
|
||||
Ideally such a development will bring researchers together and enable them to work in a unified setting that enables efficient communication of ideas and concepts.
|
||||
In this thesis we will work with the dependently typed programming language Agda~\cite{agda} and the agda-categories~\cite{agda-categories} library that serves as an extensive foundation of categorical definitions.
|
||||
This chapter shall serve as a quick introduction to the library and the formalization of this thesis.
|
||||
|
||||
\section{Setoid Enriched Categories}
|
||||
The usual textbook definition of a category hides some design decisions that have to be made when implementing it in type theory. One would usually see something like this:
|
||||
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}
|
||||
|
|
@ -18,10 +18,17 @@ A category consists of
|
|||
where the composition is associative and the identity morphisms are identities with respect to the composition.
|
||||
\end{definition}
|
||||
|
||||
Here a \textit{collection} usually is something that behaves set-like, but prevents size issues (there is no collection of all collections, preventing Russel's Paradox), it is not instantly clear how to translate this to a proof assistant. 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 Agda we need to be more thorough, there is no global notion of equality that 'just works', e.g. the standard notion of propositional equality has trouble dealing with functions and needs extra axioms like functional extensionality.
|
||||
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.
|
||||
|
||||
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, i.e. the whole category is 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 set of all morphisms, instead it contains a set of morphisms for any pair of objects. Furthermore the sets of morphisms are equipped with an equivalence relation \Verb{_≈_}, making them setoids. This solves the aforementioned issue of how to implement equality between morphisms, it is just added to the definition of a category. This kind of category is also called a \textit{setoid-enriched category}.
|
||||
Because of this proofs like \Verb{∘-resp-≈} are needed throughout the library to make sure that operations on morphisms respect the equivalence relation. Lastly, the authors also add 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.
|
||||
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.
|
||||
|
||||
\begin{listing}[H]
|
||||
\begin{minted}{agda}
|
||||
|
|
@ -57,6 +64,6 @@ From this it should be clear how other basic notions like functors or natural tr
|
|||
|
||||
\improvement{explain more}
|
||||
|
||||
The agda formalization of this thesis is structured similar to the agda-categories library, e.g. 'big' concepts like monads and categories get a top-level folder, that itself contains the core definitions, 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).
|
||||
|
|
@ -6,15 +6,17 @@ For this thesis we will restrict ourselves to monads for modelling partiality, t
|
|||
\section{Properties of Partiality Monads}
|
||||
We will now look at how to express the following non-controversial properties of partiality monads categorically:
|
||||
|
||||
|
||||
\todo[inline]{Not happy with third point}
|
||||
\begin{itemize}
|
||||
\item Commutativity of programs
|
||||
\item Programs should be partial
|
||||
\item There should be no other effect besides partiality
|
||||
\item Irrelevance of execution order
|
||||
\item Partiality of programs
|
||||
\item No other effect besides partiality
|
||||
\end{itemize}
|
||||
|
||||
The first property of course holds for any commutative monad, the other two are more interesting.
|
||||
|
||||
To ensure that programs are partial, we recall the following notion by Cockett and Lack~\cite{restriction}, that ensures that morphisms of a category are partial maps:
|
||||
To ensure that programs are partial, we recall the following notion by Cockett and Lack~\cite{restriction}, that axiomatizes the notion of partiality in a category:
|
||||
|
||||
\newcommand{\tdom}{\text{dom}\;}
|
||||
\begin{definition}[Restriction Structure]
|
||||
|
|
@ -27,16 +29,18 @@ To ensure that programs are partial, we recall the following notion by Cockett a
|
|||
\end{alignat*}
|
||||
for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
|
||||
\end{definition}
|
||||
|
||||
\todo[inline]{be more precise}
|
||||
Intuitively $\tdom f$ captures the domain of definedness of $f$.
|
||||
|
||||
\begin{definition}[Restriction Category]
|
||||
Every category has a trivial restriction structure by taking $dom (f : X \rightarrow Y) = id_X$.
|
||||
A \textit{restriction category} is a category with a non-trivial restriction structure.
|
||||
We call categories with a non-trivial restriction structure \textit{restriction categories}.
|
||||
\end{definition}
|
||||
|
||||
A partiality monad $T$ should then have the property that $\mathcal{C}^T$ is a restriction category.
|
||||
A suitably defined partiality monad $T$ should then have the property that $\mathcal{C}^T$ is 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 partiality:
|
||||
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}
|
||||
|
|
@ -53,6 +57,7 @@ Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which ca
|
|||
where $\Delta : X \rightarrow X \times X$ is the diagonal morphism.
|
||||
\end{definition}
|
||||
|
||||
\todo[inline]{proof?}
|
||||
\begin{theorem}[no proof]
|
||||
Let $T$ be an equational lifting monad, then $\mathcal{C}^T$ is a restriction category~\cite{eqlm}.
|
||||
\end{theorem}
|
||||
|
|
@ -60,7 +65,7 @@ Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which ca
|
|||
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 common examples of monads that are used to model partiality.
|
||||
|
||||
\section{The Maybe Monad}
|
||||
The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X : X \rightarrow X + 1 = i_1$ and $\mu_X : (X + 1) + 1 \rightarrow X + 1 = [ id , i_2 ]$. The monad laws follow easily. This is generally known as the maybe monad and can be viewed as the prototypical 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 prototypical example of an equational lifting monad:
|
||||
|
||||
\begin{theorem} M is an equational lifting monad.
|
||||
\end{theorem}
|
||||
|
|
@ -91,7 +96,7 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X : X \rightarro
|
|||
\arrow["{id+\;!}", from=3-4, to=5-4]
|
||||
\arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4]
|
||||
\end{tikzcd}\]
|
||||
By postcomposing $i_1$ and $i_2$ it suffices to show that:
|
||||
By pre-composing with $i_1$ and $i_2$ it suffices to show that
|
||||
\[i_1 \circ \langle i_1 , id \rangle = (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle\]
|
||||
and
|
||||
\[i_2 \;\circ \;! = (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle\]
|
||||
|
|
@ -101,27 +106,30 @@ The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X : X \rightarro
|
|||
\[dstl \circ (id \times i_2) = i_2\]
|
||||
\end{proof}
|
||||
|
||||
In a classical setting this monad is therefore sufficient for modelling partiality, but in general it won't be useful for modelling programming languages that have non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modelling possibly non-terminating computations another monad has been developed by Venanzio Capretta.
|
||||
In the setting of classical mathematics this monad is therefore sufficient for modelling partiality, but in general it will not be useful for modelling non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modelling possibly non-terminating computations another monad has been developed by Capretta~\cite{delay}.
|
||||
|
||||
\section{The Delay Monad}
|
||||
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
|
||||
It 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 coinduction in introduction or here?}
|
||||
\todo[inline]{Explain convention of double lines vs single lines}
|
||||
|
||||
\[\mprset{fraction={===}}
|
||||
\inferrule {x : X} {now\; x : DX}\hskip 2cm
|
||||
\inferrule {c : DX} {later\; c : DX}\]
|
||||
|
||||
Categorically we get 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$.
|
||||
|
||||
\begin{corollary}
|
||||
\begin{proposition}
|
||||
\label{col:delay}
|
||||
The following conditions hold:
|
||||
\begin{itemize}
|
||||
\item There exists a unit morphism $\eta : X \rightarrow DX$ for any DX, satisfying
|
||||
\item There exists a unit morphism $now : X \rightarrow DX$ for any DX, satisfying
|
||||
\begin{equation*}
|
||||
out \circ unit = i_1 \tag*{(D1)}\label{D1}
|
||||
out \circ now = i_1 \tag*{(D1)}\label{D1}
|
||||
\end{equation*}
|
||||
\item For any $f : X \rightarrow DY$ there exists a unique morphism $f^* : DX \rightarrow DY$ satisfying:
|
||||
\begin{equation*}
|
||||
|
|
@ -149,11 +157,14 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
|
|||
\end{tikzcd}\tag*{(D3)}\label{D3}
|
||||
\end{equation*}
|
||||
\end{itemize}
|
||||
\end{corollary}
|
||||
\end{proposition}
|
||||
\begin{proof}
|
||||
We will make use of the fact that every $DX$ is a final coalgebra:
|
||||
\begin{itemize}
|
||||
\item[\ref{D1}] Take $\eta = now$ then $out \circ now = i_1$ follows by definition of $now$.
|
||||
\item[\ref{D1}] This follows by definition of $now$.
|
||||
\item[\ref{D2}] We define $f^* = \;! \circ i_1$, where $!$ is the unique coalgebra-morphism in this diagram:
|
||||
\todo[inline]{Use other name than '!' for unique morphism}
|
||||
|
||||
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJbIFsgWyBpXzEgLCBpXzIgXFxjaXJjIGlfMiBdIFxcY2lyYyAob3V0IFxcY2lyYyBmKSAsIGlfMiBcXGNpcmMgaV8xIF0gXFxjaXJjIG91dCAsIChpZCArIGlfMikgXFxjaXJjIG91dCBdIl0sWzIsMCwiaV8xIl0sWzAsMywiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIm91dCJdLFsxLDQsImlkICsgISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
|
||||
\[\begin{tikzcd}
|
||||
DX \\
|
||||
|
|
@ -167,10 +178,10 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
|
|||
\end{tikzcd}\]
|
||||
$out \circ f^* = [ out \circ f , i_2 \circ f^* ] \circ out$ then follows from this diagram.
|
||||
|
||||
We are left to check uniqueness, let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$.
|
||||
Then $[ g , id ] : DX + DY \rightarrow DY$ is a coalgebra morphism, we get $[ g , id ] =\;!$ by uniqueness of $!$, it follows:
|
||||
\[g = [ g , id ] \circ i_1 =\;! \circ i_1 = f^*\]
|
||||
\item[\ref{D3}] This follows immediately, $\tau$ is the unique coalgebra morphism from $(X \times DY, dstl \circ (id \times out))$ into the terminal coalgebra $(D(X \times Y) , out)$.
|
||||
We are left to check uniqueness. Let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$.
|
||||
Then $[ g , id ] : DX + DY \rightarrow DY$\improvement{details of why it is coalgebra morphism} is a coalgebra morphism and thus $[ g , id ] =\;!$ by uniqueness of $!$.
|
||||
It follows: \[g = [ g , id ] \circ i_1 =\;! \circ i_1 = f^*\]
|
||||
\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}
|
||||
|
||||
|
|
@ -178,24 +189,23 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
|
|||
$\mathbf{D} = (D, now, (-)^*)$ is a kleisli triple.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
We will use the properties proven in corollary~\ref{col:delay} to prove the kleisli triple and strength laws.
|
||||
First we show that $(D , now, (-)^*)$ is a kleisli triple:
|
||||
We will now use the properties proven in Corollary~\ref{col:delay} to prove the Kleisli triple laws:
|
||||
\begin{itemize}
|
||||
\item[\ref{K1}]
|
||||
By uniqueness of $now^*$ it suffices to show that $out \circ id = [ out \circ now , i_2 \circ id ] \circ out$ which instantly follows by \ref{D1}.
|
||||
\item[\ref{K2}] Let $f : X \rightarrow DY$, we use the fact that $out$ is monic:
|
||||
\item[\ref{K2}] Let $f : X \rightarrow DY$. We use the fact that $out$ is monic and the following equation:
|
||||
|
||||
\[out \circ f^* \circ now \overset{\ref{D2}}{=} [ out \circ f , i_2 \circ f^* ] \circ out \circ now \overset{\ref{D1}}{=} out \circ f \]
|
||||
|
||||
\item[\ref{K3}] Using uniqueness of $(h^* \circ g)^*$ we need to show $out \circ h^* \circ g^* = [ out \circ h^* \circ g , i_2 \circ h^* \circ g^* ] \circ out$ which follows by multiple uses of \ref{D2}.
|
||||
\todo[inline]{More details probably for both K2 and K3}
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
Since $(DX, out)$ is a final coalgebra we get 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=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCIsMl1d
|
||||
\[\begin{tikzcd}
|
||||
X && {Y + X} && X && {Y + X} \\
|
||||
|
|
@ -216,7 +226,7 @@ Since $(DX, out)$ is a final coalgebra we get the following proof principle:
|
|||
$\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 needed coalgebra structure, the proofs that the diagrams commute can be looked up in the agda formalization.
|
||||
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\]
|
||||
|
|
@ -289,10 +299,11 @@ Since $(DX, out)$ is a final coalgebra we get the following proof principle:
|
|||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
To show that $\mathbf{D}$ is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} and \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
|
||||
To show that $\mathbf{D}$ is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
|
||||
|
||||
\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:
|
||||
\todo[inline]{change name of morphism}
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
|
||||
\[\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \&\&\& {D (Y +X)} \\
|
||||
|
|
@ -330,25 +341,25 @@ To show that $\mathbf{D}$ is commutative we will use another proof principle pre
|
|||
$\mathbf{D}$ is commutative.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
Using corollary~\ref{cor:solution} it suffices to show that both $\tau^* \circ \hat{\tau}$ and $\hat{\tau}^* \circ \tau$ are solutions of some guarded morphism $g$.
|
||||
Using corollary~\ref{cor:solution} it suffices to show that both $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of some guarded morphism $g$.
|
||||
|
||||
Let $w = (dstr + dstr) \circ dstl \circ (out \times out)$ and
|
||||
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \hat{\tau} , 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 \hat{\tau} , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$.
|
||||
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\]
|
||||
$g$ is trivially guarded by $[ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$.
|
||||
|
||||
We are left to show that $\tau^* \circ \hat{\tau}$ and $\hat{\tau}^* \circ \tau$ are solutions of $g$, i.e.:
|
||||
We are left to show that $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of $g$, i.e.:
|
||||
|
||||
\[\tau^* \circ \hat{\tau} = out^{-1} \circ [ id + \hat{\tau} , i_2 \circ [ \tau , later \circ \tau^* \circ \hat{\tau} ] ] \circ w = [ now , \tau^* \circ \hat{\tau}]^* \circ g \]
|
||||
\[\hat{\tau}^* \circ \tau = out^{-1} \circ [ id + \hat{\tau} , i_2 \circ [ \tau , later \circ \hat{\tau}^* \circ \tau ] ] \circ w = [ now , \hat{\tau}^* \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 first step in both equations can be proven by monicity of $out$ and then using \ref{D3} and the dual diagram for $\hat{\tau}$ which is a direct consequence of \ref{D3}:
|
||||
The first step in both equations can be proven by monicity of $out$ and then using \ref{D3} and the dual diagram for $\sigma$ which is a direct consequence of \ref{D3}:
|
||||
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgK0QoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzAsMSwiXFxoYXR7XFx0YXV9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywib3V0Il0sWzIsMywiaWQgKyBcXGhhdHtcXHRhdX0iLDJdLFswLDQsImlkIFxcdGltZXMgb3V0Il0sWzQsMiwiZHN0bCJdXQ==
|
||||
\[\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
|
||||
{D(X \times Y)} \&\&\&\& {X \times Y +D(X \times Y)}
|
||||
\arrow["{\hat{\tau}}", dashed, from=1-1, to=2-1]
|
||||
\arrow["{\sigma}", dashed, from=1-1, to=2-1]
|
||||
\arrow["out", from=2-1, to=2-5]
|
||||
\arrow["{id + \hat{\tau}}"', from=1-5, to=2-5]
|
||||
\arrow["{id + \sigma}"', from=1-5, to=2-5]
|
||||
\arrow["{id \times out}", from=1-1, to=1-3]
|
||||
\arrow["dstl", from=1-3, to=1-5]
|
||||
\end{tikzcd}\]
|
||||
|
|
|
|||
|
|
@ -81,7 +81,7 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
|
|||
Pre-Elgot monads on $\C$ form a category that is a subcategory of $\monads{\C}$.
|
||||
|
||||
\begin{definition}[Category of pre-Elgot monads]
|
||||
Let $\C$ be a category. We define the category $\preelgot{\C}$ where objects are pre-Elgot monads and a morphism between two pre-Elgot monads $(S, \eta^S, \mu^S, (-)^{\#_S})$ and $(T, \eta^T, \mu^T, (-)^{\#_T})$ is a natural transformation $\alpha : S \rightarrow T$ satisfying the following diagrams:
|
||||
Let $\C$ be a category. We define the category $\preelgot{\C}$ where objects are pre-Elgot monads and morphisms between two pre-Elgot monads $(S, \eta^S, \mu^S, (-)^{\#_S})$ and $(T, \eta^T, \mu^T, (-)^{\#_T})$ are natural transformations $\alpha : S \rightarrow T$ satisfying the following diagrams:
|
||||
% https://q.uiver.app/#q=WzAsMTEsWzAsMCwiWCJdLFsyLDAsIlNYIl0sWzIsMSwiVFgiXSxbMywwLCJTU1giXSxbNSwwLCJTVFgiXSxbMywxLCJTWCJdLFs1LDEsIlRUWCJdLFs0LDIsIlRYIl0sWzYsMCwiWCJdLFs4LDAsIlNBIl0sWzgsMSwiVEEiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl0sWzksMTAsIlxcYWxwaGEiXSxbOCw5LCJoXntcXCNfU30iXSxbOCwxMCwiKChcXGFscGhhICsgaWQpIFxcY2lyYyBmKV57XFwjX1R9IiwyXV0=
|
||||
\[\begin{tikzcd}
|
||||
X && SX & SSX && STX & X && SA \\
|
||||
|
|
@ -103,7 +103,7 @@ Pre-Elgot monads on $\C$ form a category that is a subcategory of $\monads{\C}$.
|
|||
|
||||
\todo[inline]{Category of (strong) pre-Elgot monads, introduce category of monads in preliminaries}
|
||||
|
||||
\section{The Initial Pre-Elgot Monad}
|
||||
\section{The Initial Strong Pre-Elgot Monad}
|
||||
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial pre-Elgot monad.
|
||||
|
||||
\begin{lemma}
|
||||
|
|
@ -181,11 +181,15 @@ Of course there is also a symmetric version of this:
|
|||
Given two morphisms $g, h : KY \times X \rightarrow A$ where $X, Y \in \obj{\C}, A \in \obj{\elgotalgs{\C}}$ to show that $g = h$ it suffices to find a morphism $f : Y \times X \rightarrow A$ such that $g$ and $h$ satisfy \ref{sharpl1} and \ref{sharpl2}.
|
||||
\end{remark}
|
||||
|
||||
\todo[inline]{Maybe do a helper proposition first that characterizes tau with the three laws in the file}
|
||||
|
||||
\begin{theorem}
|
||||
$\mathbf{K}$ is a strong monad.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
We define strength as $\tau : (\eta : X \times Y \rightarrow K(X \times Y))^\sharp : X \times KY \rightarrow K(X \times Y)$
|
||||
We define strength as $\tau = (\eta : X \times Y \rightarrow K(X \times Y))^\sharp : X \times KY \rightarrow K(X \times Y)$
|
||||
|
||||
\change[inline]{Maybe put complete proof}
|
||||
|
||||
To check naturality and the strength laws we will use remark~\ref{rem:proofbystability} and for brevity only state the needed unifying morphism by pasting \ref{sharpl1} into the required diagram. The proofs of \ref{sharpr1} and \ref{sharpr2} can then be looked up in the formalization.
|
||||
|
||||
|
|
@ -220,7 +224,7 @@ Of course there is also a symmetric version of this:
|
|||
The strength laws are proven similarly:
|
||||
|
||||
\begin{itemize}
|
||||
\item[\ref{S1}]
|
||||
\item[\ref{S1}] This is an instance of the following more general law that holds on $\mathbf{K}$:
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
|
||||
\[\begin{tikzcd}
|
||||
{X \times KY} && {K(X\times Y)} \\
|
||||
|
|
@ -232,7 +236,6 @@ Of course there is also a symmetric version of this:
|
|||
\arrow["{id \times \eta}"', from=3-1, to=1-1]
|
||||
\arrow["{\eta \circ \pi_2}"', from=3-1, to=3-3]
|
||||
\end{tikzcd}\]
|
||||
\todo{this is more general than S1}
|
||||
|
||||
\item[\ref{S2}]
|
||||
This is an instance of \ref{sharpr1}.
|
||||
|
|
@ -268,8 +271,6 @@ Of course there is also a symmetric version of this:
|
|||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
\change[inline]{Use sigma instead of hat(tau)}
|
||||
|
||||
\begin{theorem}
|
||||
$\mathbf{K}$ is a commutative monad.
|
||||
\end{theorem}
|
||||
|
|
@ -282,15 +283,16 @@ Of course there is also a symmetric version of this:
|
|||
& {K(X \times KY)} && {K(X \times Y)} \\
|
||||
{KX \times Y}
|
||||
\arrow["\tau", from=1-2, to=1-4]
|
||||
\arrow["{\hat{\tau}}"', from=1-2, to=3-2]
|
||||
\arrow["{\hat{\tau}^*}", from=1-4, to=3-4]
|
||||
\arrow["{\sigma}"', from=1-2, to=3-2]
|
||||
\arrow["{\sigma^*}", from=1-4, to=3-4]
|
||||
\arrow["{\tau^*}"', from=3-2, to=3-4]
|
||||
\arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2]
|
||||
\arrow["{\hat{\tau}}"', curve={height=12pt}, from=4-1, to=3-4]
|
||||
\arrow["{\sigma}"', curve={height=12pt}, from=4-1, to=3-4]
|
||||
\end{tikzcd}\]
|
||||
The proofs for \ref{sharpr1} and the proof that $\hat{\tau}^* \circ \tau$ is right iteration preserving are straightforward and can be looked up in the formalization.
|
||||
The proof that $\tau^* \circ \hat{\tau}$ is right iteration preserving is non-trivial, so we will look at it in more detail:
|
||||
Let $Z \in \obj{\C}, h : Z \rightarrow KY + Z$ and let us introduce a definition for brevity: $\psi = \tau^* \circ \hat{\tau}$. We now use remark~\ref{rem:proofbyleftstability} to show that $\psi$ is right iteration preserving:
|
||||
\todo[inline]{Maybe don't omit proofs, give them point by point?}
|
||||
The proofs for \ref{sharpr1} and the proof that $\sigma^* \circ \tau$ is right iteration preserving are straightforward and can be looked up in the formalization.
|
||||
The proof that $\tau^* \circ \sigma$ is right iteration preserving is non-trivial, so we will look at it in more detail:
|
||||
Let $Z \in \obj{\C}, h : Z \rightarrow KY + Z$ and let us introduce a definition for brevity: $\psi = \tau^* \circ \sigma$. We now use remark~\ref{rem:proofbyleftstability} to show that $\psi$ is right iteration preserving:
|
||||
|
||||
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
|
||||
\[\begin{tikzcd}
|
||||
|
|
@ -320,6 +322,6 @@ Of course there is also a symmetric version of this:
|
|||
$\mathbf{K}$ is the initial (strong) pre-Elgot monad.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
$\mathbf{K}$ is by definition a pre-Elgot monad, we are left to show that it is the initial one.
|
||||
Note that $\mathbf{K}$ is by definition a pre-Elgot monad.
|
||||
\todo[inline]{proof that K is initial strong pre-Elgot}
|
||||
\end{proof}
|
||||
Loading…
Reference in a new issue