diff --git a/.gitignore b/.gitignore
index 8bcaf3b..c71d3b6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,3 +55,4 @@ slides/_minted-main/
 thesis/main.bbl-SAVE-ERROR
 thesis/main.bcf-SAVE-ERROR
 thesis/main.tdo
+main.synctex(busy)
diff --git a/thesis/.vscode/ltex.dictionary.en-US.txt b/thesis/.vscode/ltex.dictionary.en-US.txt
index ef4ac44..2fc126b 100644
--- a/thesis/.vscode/ltex.dictionary.en-US.txt
+++ b/thesis/.vscode/ltex.dictionary.en-US.txt
@@ -47,3 +47,6 @@ Quotienting
 bisimilarity
 corecursively
 coproduct
+adjunction
+counit
+epi
diff --git a/thesis/src/01_preliminaries.tex b/thesis/src/01_preliminaries.tex
index 7786279..c98a5ea 100644
--- a/thesis/src/01_preliminaries.tex
+++ b/thesis/src/01_preliminaries.tex
@@ -114,14 +114,30 @@ The internal logic of cartesian closed categories is the simply typed $\lambda$-
 
 \section{Coalgebras}
 \todo[inline]{Maybe introduce (co-)induction here via (co-)algebras}
-\todo[inline]{Introduce (terminal) coalgebras, proof Lambek's lemma}
+\todo[inline]{Introduce (terminal) coalgebras, prove Lambek's lemma}
 
 \section{Adjunctions and Free Objects}
-\todo[inline]{Introduce adjunctions}
+\todo[inline]{Add text}
+
+\begin{definition}[Adjoint Functors]\label{def:adjoint}
+  Let $\C$ and $\D$ be two categories. Two functors $L : \C \rightarrow \D$ and $R : \D \rightarrow \C$ are called adjoint to each other if there exist natural transformations $\eta : Id \rightarrow R \circ L$ (called unit) and $\epsilon : L \circ R \rightarrow Id$ (called counit) such that the following diagrams commute:
+  % https://q.uiver.app/#q=WzAsNixbMCwwLCJMWCJdLFsyLDAsIkxSTFgiXSxbMiwxLCJMWCJdLFszLDAsIlJYIl0sWzUsMCwiUkxSWCJdLFs1LDEsIlJYIl0sWzAsMSwiTFxcZXRhIl0sWzEsMiwiXFxlcHNpbG9uIl0sWzAsMiwiaWQiLDJdLFs0LDUsIlJcXGVwc2lsb24iXSxbMyw0LCJcXGV0YSJdLFszLDUsImlkIiwyXV0=
+  \[\begin{tikzcd}[ampersand replacement=\&]
+    LX \&\& LRLX \& RX \&\& RLRX \\
+    \&\& LX \&\&\& RX
+    \arrow["L\eta", from=1-1, to=1-3]
+    \arrow["\epsilon", from=1-3, to=2-3]
+    \arrow["id"', from=1-1, to=2-3]
+    \arrow["R\epsilon", from=1-6, to=2-6]
+    \arrow["\eta", from=1-4, to=1-6]
+    \arrow["id"', from=1-4, to=2-6]
+  \end{tikzcd}\]
+  We write $L \dashv R$ and call $L$ the left adjoint of $R$.
+\end{definition}
 
 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]
+\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 the following universal property holds for any $Y \in \obj{\C}$ and $f : X \rightarrow UY$:
 % https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxleGlzdHMhXFxsbGJyYWNrZXQgZiBcXHJyYnJhY2tldCIsMl1d
 \[\begin{tikzcd}
@@ -133,6 +149,70 @@ Let $\C, \D$ be categories and $U : \C \rightarrow \D$ be a forgetful functor (w
 \end{tikzcd}\]
 \end{definition}
 
+\begin{theorem}\label{thm:foladj}
+  Let $\C$ and $\D$ be two categories and let $U : \C \rightarrow \D$ be a forgetful functor between these categories.
+  Existence of all free objects on $\D$ yields a left adjoint to the forgetful functor that is called the free functor.
+\end{theorem}
+\begin{proof}
+  First we define the free functor $F : \D \rightarrow \C$. $F$ maps objects of $\D$ to the corresponding $FX$ in $\C$ (where $FX$ is the underlying object in Definition~\ref{def:free}).
+  For any morphism $f : X \rightarrow Y$ in $\D$ we take $Ff = \llbracket\eta \circ f\rrbracket$.
+  This is a functor because:
+  \begin{enumerate}
+    \item The identity law:
+    \[Fid = \llbracket \eta \circ id \rrbracket = \llbracket \eta \rrbracket = id\]
+    follows by uniqueness of $\llbracket \eta \rrbracket$ since $id$ satisfies $id \circ \eta = \eta$.
+    \item Let $f : X \rightarrow Y$ and $g : Y \rightarrow Z$. The compositional law:
+    \[F(g \circ f) = \llbracket \eta \circ g \circ f \rrbracket = \llbracket \eta \circ g \rrbracket \circ \llbracket \eta \circ f \rrbracket = Fg \circ Ff \]
+    follows by uniqueness of $\llbracket \eta \circ g \circ f \rrbracket$ since:
+    \[\llbracket \eta \circ g \rrbracket \circ \llbracket \eta \circ f \rrbracket \circ \eta = \llbracket \eta \circ g \rrbracket \circ \eta \circ f = \eta \circ g \circ f\]
+  \end{enumerate}
+
+  We are left to show that $F$ is left adjoint to $U$. The free object $\eta$ extends to a family of morphisms $(\eta_X : X \rightarrow UFX)_{X \in \obj{D}}$ yielding the unit of the adjunction. For naturality of $\eta$ we need to check:
+  \[\eta \circ f = \llbracket \eta \circ f \rrbracket \circ \eta = UFf \circ \eta\]
+  which follows by the universal property of free objects.
+
+  As the counit take $\epsilon = \llbracket id \rrbracket : FU \rightarrow Id$. For naturality of $\epsilon$ we show:
+  \[\llbracket id \rrbracket \circ FU f = \llbracket Uf \rrbracket = f \circ \llbracket id \rrbracket\]
+  where $f : X \rightarrow Y$.
+  
+  Using uniqueness of $\llbracket Uf \rrbracket$ we are done by:
+
+
+  \begin{alignat*}{1}
+    &U (\llbracket id \rrbracket \circ FUf) \circ \eta\\
+    =\;&U \llbracket id \rrbracket \circ UFUf \circ \eta\\
+    =\;&U \llbracket id \rrbracket \circ \eta \circ Uf\\
+    =\;&id \circ Uf\\
+    =\;&Uf
+  \end{alignat*}
+  % \[U (\llbracket id \rrbracket \circ FUf) \circ \eta = U \llbracket id \rrbracket \circ UFUf \circ \eta = U \llbracket id \rrbracket \circ \eta \circ Uf = id \circ Uf = Uf\]
+  and
+  \begin{alignat*}{1}
+    &U (f \circ \llbracket id \rrbracket) \circ \eta\\
+    =\;&Uf \circ U\llbracket id \rrbracket \circ \eta\\
+    =\;&Uf \circ id\\
+    =\;&Uf
+  \end{alignat*}
+  % \[U (f \circ \llbracket id \rrbracket) \circ \eta = Uf \circ U\llbracket id \rrbracket \circ \eta = Uf \circ id = Uf \]
+
+  Let us finally check the triangle identities. The first one can be proven via:
+  \[\epsilon \circ F\eta = \llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket = \llbracket \eta \rrbracket = id \]
+  where the only step missing is $\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket = \llbracket \eta \rrbracket$ which holds since:
+  \begin{alignat*}{1}
+    &\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket \circ \eta\\
+    =\;&\llbracket id \rrbracket \circ \eta \circ \eta\\
+    =\;&id \circ \eta\\
+    =\;&\eta
+  \end{alignat*}
+  % \[\llbracket id \rrbracket \circ \llbracket \eta \circ \eta \rrbracket \circ \eta = \llbracket id \rrbracket \circ \eta \circ \eta = id \circ \eta = \eta\]
+
+  The second triangle identity is a direct consequence of the universal property of free objects:
+  \[U\epsilon \circ \eta = U \llbracket id \rrbracket \circ \eta = id\]
+
+  We have thereby proven that indeed $F \dashv U$.
+
+\end{proof}
+
 \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}.
 
@@ -163,6 +243,24 @@ Monads are widely known among programmers as a way of modelling effects in pure
   \end{tikzcd}\]
 \end{definition}
 
+The following theorem makes the relationship of monads and adjoint functors apparent:
+\begin{theorem}\label{thm:adjmon}
+  For every adjunction $L \dashv R$ the triple $(R \circ L, \eta, R\epsilon L)$ is a monad.
+\end{theorem}
+\begin{proof}
+  We check the monad laws:
+  \begin{itemize}
+    \item[\ref{M1}]
+    Follows by naturality of $\epsilon$:
+    \[ R\epsilon L \circ RLR\epsilon L = R(\epsilon L \circ LR\epsilon L) = R (\epsilon L \circ \epsilon L) = R\epsilon L \circ R\epsilon L\]
+    \item[\ref{M2}]
+    Follows by the second diagram in Definition~\ref{def:adjoint}:
+    \[R\epsilon L \circ \eta = id\]
+    \item[\ref{M3}] Follows by the first diagram in Definition~\ref{def:adjoint}:
+    \[R\epsilon L \circ RL\eta = R(\epsilon L \circ L\eta) = R(id) = id\]
+  \end{itemize}
+\end{proof}
+
 Morphisms between monads are natural transformations that respect the monad operations:
 
 \change[inline]{