Work on thesis

thesis/bib.bib

@@ -39,6 +39,28 @@
   journal   = {Logical Methods in Computer Science}
 }
 
+@inproceedings{Lane1971,
+  title  = {Categories for the Working Mathematician},
+  author = {Saunders Mac Lane},
+  year   = {1971},
+  url    = {https://api.semanticscholar.org/CorpusID:122892655}
+}
+
+ @article{moggi,
+  title    = {Notions of computation and monads},
+  journal  = {Information and Computation},
+  volume   = {93},
+  number   = {1},
+  pages    = {55-92},
+  year     = {1991},
+  note     = {Selections from 1989 IEEE Symposium on Logic in Computer Science},
+  issn     = {0890-5401},
+  doi      = {https://doi.org/10.1016/0890-5401(91)90052-4},
+  url      = {https://www.sciencedirect.com/science/article/pii/0890540191900524},
+  author   = {Eugenio Moggi},
+  abstract = {The λ-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs for a wide range of notions of computation.}
+}
+
 @inproceedings{uni-elgot2021,
   doi       = {10.4230/LIPICS.ICALP.2021.131},
   url       = {https://drops.dagstuhl.de/opus/volltexte/2021/14200/},
@@ -49,4 +71,4 @@
   publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
   year      = {2021},
   copyright = {Creative Commons Attribution 4.0 International license}
-}
+}

thesis/main.tex

@@ -34,6 +34,8 @@
   \chaptermark{#1}%
   \addcontentsline{toc}{chapter}{#1}}
 
+\newcommand\C{\mathcal{C}}
+
 \declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition}
 \declaretheorem[name=Example,style=definition,sibling=definition]{example}
 \declaretheorem[style=definition,numbered=no]{exercise}

thesis/src/01_preliminaries.tex

@@ -1,4 +1,37 @@
 \chapter{Preliminaries}
+We assume familiarity with basic concepts of category theory that should be taught in any introductory course, or can be looked up in~\cite{Lane1971}. In particular we will need the notions of category, functor, functor algebra, natural transformation, product and coproduct.
+
+In the rest of this section we will look at other categorical notions that are either less well-known, or crucial for this thesis and therefore require special attention.
+
 \section{Stable Natural Numbers Object}
+
 \section{Extensive and Distributive Categories}
-\section{Strong and Commutative Monads}
+
+\section{Monads}
+Monads are widely known among programmers as a way of modelling effects in pure languages. Categorically a Monad is a monoid in the category of endofunctors of a category, or in more accessible terms:
+
+\begin{definition}[Monad~\cite{Lane1971}]
+  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{enumerate}
+    % TODO add quantifiers
+    \item $\mu_X \circ \mu_{FX} = \mu_X \circ F\mu_X$
+    \item $\mu_X \circ \eta_{FX} = id_{FX}$
+    \item $\mu_X \circ F\eta_X = id_{FX}$
+  \end{enumerate}
+\end{definition}
+
+For programmers a second equivalent definition is more useful:
+
+\begin{definition}[Kleisli triple~\cite{moggi}]
+  A kleisli triple on a category $\C$ is a triple $(F, \eta, _*)$, where $F : \vert \C \vert \rightarrow \vert \C \vert$ is a mapping on objects, $(\eta_X : X \rightarrow FX)_{X\in\vert\C\vert}$ 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. With the following laws:
+  \begin{enumerate}
+    % TODO add quantifiers
+    \item $\eta_X^* = id_{FX}$
+    \item $\eta_X \circ f^* = f$
+    \item $f^* \circ g* = (f \circ g^*)^*$ 
+  \end{enumerate}
+\end{definition}
+
+% todo change moggi citation to manes, once I got the original
+\begin{theorem}[\cite{moggi}] The notions of Kleisli triple and monad are equivalent.
+\end{theorem}