add kleisli cat

thesis/src/01_preliminaries.tex

@@ -9,6 +9,7 @@ We will also sometimes omit indices of the identity and of natural transformatio
 Let us first introduce notation for binary (co-)products by giving their usual diagrams:
 
 % TODO products bind stronger than coproducts irgendwo erwähnen
+% TODO notation $\mathcal{C}(X,Y)$ einführen
 
 \begin{figure}[ht]
 % https://q.uiver.app/#q=WzAsOCxbMiwwLCJBIFxcdGltZXMgQiJdLFswLDAsIkEiXSxbNCwwLCJCIl0sWzIsMiwiQyJdLFs4LDAsIkEgKyBCIl0sWzYsMCwiQSJdLFsxMCwwLCJCIl0sWzgsMiwiQyJdLFswLDEsIlxccGlfMSIsMl0sWzAsMiwiXFxwaV8yIl0sWzMsMiwiZyIsMl0sWzMsMSwiZiJdLFszLDAsIlxcZXhpc3RzISBcXGxhbmdsZSBmICwgZyBcXHJhbmdsZSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDQsImlfMSJdLFs2LDQsImlfMiIsMl0sWzUsNywiZiIsMl0sWzYsNywiZyJdLFs0LDcsIlxcZXhpc3RzICEgW2YgLCBnXSIsMV1d
@@ -138,17 +139,25 @@ For programmers a second equivalent definition is more useful:
   \end{alignat*}
 \end{definition}
 
-In functional programming languages like Haskell the Kleisli lifting $(-)^*$ is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and $\eta$ is called $return$. Given two morphisms $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation:
+In functional programming languages like Haskell the Kleisli lifting $(-)^*$ is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and $\eta$ is called $return$. Given two programs $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation:
 \begin{minted}{haskell}
   do y <- f x
      g y
 \end{minted}
 
-% TODO
+This results in the following:
+
 \begin{definition}[Kleisli Category]
+  Given a monad $T$ on a category $\mathcal{C}$, the Kleisli category $\mathcal{C}^T$ is defined as:
+  \begin{itemize}
+    \item $\vert \mathcal{C}^T \vert = \obj{C}$
+    \item $\mathcal{C^T}(X, Y) = \mathcal{C}(X, TY)$
+    \item composition of $f : X \rightarrow TY$ and $g : Y \rightarrow TZ$ is defined as $f \circ_{\mathcal{C}^T} g = f^* \circ_{\mathcal{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}
 
-% 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}
 \begin{proof}

thesis/src/03_partiality-monads.tex

@@ -173,7 +173,7 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
   \end{itemize}
 \end{proof}
 
-Since $DX$ is a final coalgebra we get the following proof principle:
+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$.