diff --git a/tex/.chktexrc b/tex/.chktexrc
new file mode 100644
index 0000000..692aa0f
--- /dev/null
+++ b/tex/.chktexrc
@@ -0,0 +1,4 @@
+CmdLine = {
+  -n18
+  -n46
+}
diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt
index ba9cbdd..3c1488d 100644
--- a/tex/.vscode/ltex.dictionary.en-US.txt
+++ b/tex/.vscode/ltex.dictionary.en-US.txt
@@ -27,3 +27,8 @@ Epimorphisms
 Isomorphisms
 cancellative
 Coproducts
+poset
+iff
+posets
+coproduct
+monoid
diff --git a/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt
index d1b8528..cb4087c 100644
--- a/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt
+++ b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt
@@ -5,3 +5,6 @@
 {"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QFriedrich-Alexander-Universität Erlangen-Nürnberg\\E$"}
 {"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\QThis is a summary of the course “Algebra des Programmierens” taught by Prof. Dr. Stefan Milius in the winter term 2023/2024 at the FAU .\\E$"}
 {"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\Q\\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfies the following two rules law:natident Identity law:natfusion Fusion Lists.\\E$"}
+{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[cases] mycase Case .\\E$"}
+{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QIt seems that these proofs should somehow be constructable from each other\\E$"}
+{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QEvery categorical notion can thus be dualized by viewing it in the dual category, some examples include: Notion Dual Notion Initial Object Terminal Object Monomorphism Epimorphism Isomorphism Isomorphism\\E$"}
diff --git a/tex/.vscode/settings.json b/tex/.vscode/settings.json
index fdce008..3659725 100644
--- a/tex/.vscode/settings.json
+++ b/tex/.vscode/settings.json
@@ -23,5 +23,10 @@
         "latexmk-main"
       ]
     }
-  ]
+  ],
+  "ltex.latex.commands": {
+    "\\customlabel{}": "ignore",
+    "\\setminted[]{}": "ignore",
+    "\\setmintedinline[]{}": "ignore"
+  }
 }
\ No newline at end of file
diff --git a/tex/main.pdf b/tex/main.pdf
index dcf70af..94387b5 100644
Binary files a/tex/main.pdf and b/tex/main.pdf differ
diff --git a/tex/main.tex b/tex/main.tex
index fe024de..0981baa 100644
--- a/tex/main.tex
+++ b/tex/main.tex
@@ -1,9 +1,8 @@
-\documentclass[a4paper,11pt,titlepage]{scrartcl}
+\documentclass[a4paper,11pt,titlepage,numbers=noenddot]{scrbook}
 
 %%%% Document Setup
 \usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
-\usepackage{scrlayer-fancyhdr}
-\usepackage{extramarks}
+\usepackage{scrlayer-scrpage}
 \usepackage[ngerman, english]{babel}
 \babeltags{german=ngerman}
 \usepackage{anyfontsize}
@@ -13,14 +12,12 @@
 \usepackage{booktabs}
 \usepackage[scale=.85]{noto-mono} % TODO find better unicode mono font
 \usepackage[final]{hyperref}
-\pagestyle{fancy}
-\lhead{\DocTitle}
-\chead{\UniCourse}
-\rhead{\firstxmark}
-\lfoot{\lastxmark}
-\cfoot{\thepage}
-\renewcommand\headrulewidth{0.4pt}
-\renewcommand\footrulewidth{0.4pt}
+\usepackage{scrhack}
+\automark{chapter}
+\renewcommand{\sectionmark}[1]{\markright{\thesection\ #1}}
+\renewcommand{\subsectionmark}[1]{\markright{\thesubsection\ #1}}
+\pagestyle{scrheadings}
+
 %%%%
 
 %%%% Metadata
@@ -51,7 +48,13 @@
 \setmintedinline[haskell]{
     style=bw
 }
+%%%%
 
+%%%% Spacing
+\setlength{\parindent}{0pt}
+\setlength{\parskip}{6pt}
+\setlength{\marginparsep}{0cm}
+\AtBeginEnvironment{minted}{\setlength{\parskip}{0pt}}
 %%%%
 
 %%%% Math packages
@@ -59,7 +62,8 @@
 \usepackage{thmtools}
 \usepackage{tikz}
 \usetikzlibrary{cd, babel, quotes}
-\declaretheorem[name=Definition,style=definition,numberwithin=section]{definition}
+\usepackage{quiver}
+\declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition}
 \declaretheorem[name=Example,style=definition,sibling=definition]{example}
 \declaretheorem[style=definition,numbered=no]{exercise}
 \declaretheorem[name=Remark,style=definition,sibling=definition]{remark}
@@ -76,7 +80,7 @@
 \makeatletter
 \hypersetup{
   pdfauthor={\@author},
-  pdftitle={\@title},
+  pdftitle={\UniCourse},
   % kill those ugly red rectangles around links
   hidelinks,
 }
@@ -127,20 +131,23 @@
 %%% Notation
 %% Category C
 \newcommand{\C}{\ensuremath{\mathscr{C}}}
+%% Objects of category
 \newcommand{\obj}[1]{\ensuremath{\vert #1 \vert}}
-
+%% Dual category
+\newcommand{\dual}[1]{\ensuremath{#1^{op}}}
 %%%
 %%%%
 
 \begin{document}
 %% Titlepage
 \maketitle
+\thispagestyle{empty}
+\null\newpage
 \setcounter{page}{1}
 %%
 
 %% TOC
 \tableofcontents
-\pagebreak
 %%
 
 %% Contents
diff --git a/tex/quiver.sty b/tex/quiver.sty
new file mode 100644
index 0000000..b0b4e06
--- /dev/null
+++ b/tex/quiver.sty
@@ -0,0 +1,40 @@
+% *** quiver ***
+% A package for drawing commutative diagrams exported from https://q.uiver.app.
+%
+% This package is currently a wrapper around the `tikz-cd` package, importing necessary TikZ
+% libraries, and defining a new TikZ style for curves of a fixed height.
+%
+% Version: 1.4.2
+% Authors:
+% - varkor (https://github.com/varkor)
+% - AndréC (https://tex.stackexchange.com/users/138900/andr%C3%A9c)
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{quiver}[2021/01/11 quiver]
+
+% `tikz-cd` is necessary to draw commutative diagrams.
+\RequirePackage{tikz-cd}
+% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
+% \RequirePackage{amssymb}
+% `calc` is necessary to draw curved arrows.
+\usetikzlibrary{calc}
+% `pathmorphing` is necessary to draw squiggly arrows.
+\usetikzlibrary{decorations.pathmorphing}
+
+% A TikZ style for curved arrows of a fixed height, due to AndréC.
+\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
+          .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
+          and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
+          .. (\tikztotarget)\tikztonodes}},
+  settings/.code={\tikzset{quiver/.cd,#1}
+      \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
+  quiver/.cd,pos/.initial=0.35,height/.initial=0}
+
+% TikZ arrowhead/tail styles.
+\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
+\tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}}
+\tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}}
+% TikZ arrow styles.
+\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}
+
+\endinput
diff --git a/tex/sections/01_introduction.tex b/tex/sections/01_introduction.tex
index 6c76159..f61dffc 100644
--- a/tex/sections/01_introduction.tex
+++ b/tex/sections/01_introduction.tex
@@ -1,11 +1,10 @@
-% chktex-file 46
-\section{Introduction}
+\chapter{Introduction}
 This is a summary of the course ``Algebra des Programmierens'' taught by Prof.\ Dr.\ Stefan Milius in the winter term 2023/2024 at the FAU~\footnote{Friedrich-Alexander-Universität Erlangen-Nürnberg}.
 The course is based on~\cite{poll1999algebra} with~\cite{adamek1990abstract} as a reference for category theory.
 
 Goal of the course is to develop a mathematical theory for semantics of data types and their accompanying proof principles. The chosen environment is the field of category theory.
 
-\subsection{Functions}
+\section{Functions}
 A function $f : X \rightarrow Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$).
 More concretely $f$ is a relation $f \subseteq X \times Y$ which is
 \begin{itemize}
@@ -32,7 +31,7 @@ Often, one is also interested in the symmetrical properties, a function is calle
   \end{enumerate}
 \end{example}
 
-\subsection{Data Types}
+\section{Data Types}
 
 Programs work with data that should ideally be organized in a useful manner.
 A useful representation for data in functional programming is by means of \emph{algebraic data types}.
@@ -54,7 +53,7 @@ These data types are declared by means of constructors, yielding concrete descri
 Such data types (parametric or non-parametric) usually come with a principle for defining functions called recursion and in richer type systems (e.g.\ in a dependently typed setting) with a principle for proving facts about recursive functions called induction.
 Equivalently, every function defined by recursion can be defined via a \emph{fold}-function which satisfies an identity and fusion law, which replace the induction principle. Let us now consider two examples of data types and illustrate this.
 
-\subsubsection{Natural Numbers}
+\subsection{Natural Numbers}
 The type of natural numbers comes with a fold function $foldn : C \rightarrow (Nat \rightarrow C) \rightarrow Nat \rightarrow C$ for every $C$, defined by
 \begin{alignat*}{2}
    & foldn\;c\;h\;zero     &  & = c                   \\
@@ -182,7 +181,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
     \end{tikzcd}\]
   trivially commutes.
 \end{example}
-\subsubsection{Lists}
+\subsection{Lists}
 We will now look at the $List$ type and examine it for similar properties. Let us start with the fold function $foldr : C \rightarrow (A \rightarrow C \rightarrow C) \rightarrow List\;A \rightarrow C$, which is defined by
 \begin{alignat*}{2}
    & foldr\;c\;h\;nil           &  & = c                       \\
diff --git a/tex/sections/02_categories.tex b/tex/sections/02_categories.tex
index 8dffa83..7794157 100644
--- a/tex/sections/02_categories.tex
+++ b/tex/sections/02_categories.tex
@@ -1,10 +1,9 @@
-% chktex-file 46
-\section{Category Theory}
+\chapter{Category Theory}
 
 Categories consist of objects and morphisms between those objects, that can be composed in a coherent way.
-This yields a framework for abstracting many mathematical concepts for reasoning on a very abstract level.
+This yields a framework for abstraction of many mathematical concepts that enables us to reason on a very abstract level.
 
-\begin{definition} A category \C consists of
+\begin{definition}[Category] A category \C consists of
   \begin{itemize}
     \item a class of objects denoted $\obj{\C}$,
     \item for every pair of objects $A,B \in \obj{\C}$ a set of morphisms $\C(A,B)$ called the hom-set,
@@ -28,13 +27,13 @@ This yields a framework for abstracting many mathematical concepts for reasoning
     \end{tabular}
   \end{center}
 \end{example}
-\subsection{Special Objects}
+\section{Special Objects}
 Special objects play an important role in category theory.
 In this chapter we will characterize (finite) products and coproducts, as well as special morphisms such as isomorphisms, monomorphisms and epimorphisms.
 
-\subsubsection{Initial and Terminal Objects}
+\section{Initial and Terminal Objects}
 
-\begin{definition} The following is the categorical abstraction of ``empty set'' and ``singleton set'' respectively.
+\begin{definition}[Initial and Terminal Objects] The following is the categorical abstraction of ``empty set'' and ``singleton set'' respectively.
   \begin{enumerate}
     \item An object $0 \in \obj{\C}$ is called initial if for every $B \in \obj{C}$ there is a unique morphism $¡ : 0 \rightarrow B$.
     \item An object $1 \in \obj{\C}$ is called terminal if for every $A \in \obj{C}$ there is a unique morphism $! : A \rightarrow 1$.
@@ -53,10 +52,10 @@ In this chapter we will characterize (finite) products and coproducts, as well a
 \end{example}
 
 
-\subsubsection{Special Morphisms}
+\section{Special Morphisms}
 Now let us characterize special morphisms.
 
-\begin{definition}
+\begin{definition}[Special Morphisms]
   Let $f : A \rightarrow B$ be a morphism. $f$ is called
   \begin{itemize}
     \item an \emph{isomorphism} (\emph{iso}), if there exists an inverse $f^{-1} : B \rightarrow A$ such that $f \circ g = id_B$ and $g \circ f = id_A$;
@@ -76,37 +75,201 @@ Now let us characterize special morphisms.
   \end{center}
 \end{example}
 
-\begin{proposition}
-  % TODO
-  iso is mono and epi
+\begin{proposition} Every isomorphism is a monomorphism and an epimorphism.
 \end{proposition}
+\begin{proof}
+  Let $f$ be an isomorphism.
+  \begin{itemize}
+    \item $f \circ g = f \circ h$ implies $g = f^{-1} \circ f \circ g = f^{-1} \circ f \circ h = h$, thus $f$ is a monomorphism.
+    \item $g \circ f = h \circ f$ implies $g = g \circ f \circ f^{-1} = h \circ f \circ f^{-1} = h$, thus $f$ is an epimorphism.
+  \end{itemize}
+\end{proof}
+\begin{proposition}\label{prop:monosplitting} If $f \circ m$ is a monomorphism then $m$ is also a monomorphism.
+\end{proposition}
+\begin{proof}
+  Let $m \circ g = m \circ h$. To show that $g = h$ it suffices to show that $f \circ m \circ g = f \circ m \circ h$, which indeed follows by assumption.
+\end{proof}
+\begin{proposition}\label{prop:episplitting} If $e \circ f$ is an epimorphism then $e$ is also an epimorphism.
+\end{proposition}
+\begin{proof}
+  Let $g \circ e = h \circ e$. To show that $g = h$ it suffices to show that $g \circ e \circ f = h \circ e \circ f$, which again follows by assumption.
+\end{proof}
+
+Categorical structures like initial objects are usually not uniquely identified, there might be multiple initial objects in a category. However, all initial objects in a category are isomorphic, we call this ``unique up to isomorphism''.
+
+\begin{proposition}\label{prop:init_up_to} Initial objects are unique up to isomorphism.
+\end{proposition}
+\begin{proof}
+  Let $0, 0' \in \obj{\C}$ be two initial objects of $\C$ with the unique morphisms $¡_A : 0 \rightarrow A$ and ${¡'}_A : 0' \rightarrow A$.
+  The isomorphism is:
+  % https://q.uiver.app/#q=WzAsMixbMCwwLCIwIl0sWzIsMCwiMCciXSxbMSwwLCJ7wqEnfV8wIiwyLHsiY3VydmUiOi0yfV0sWzAsMSwiwqFfezAnfSIsMCx7ImN1cnZlIjotMn1dXQ==
+  \[
+    \begin{tikzcd}
+      0 && {0'}
+      \arrow["{{¡'}_0}"', curve={height=-12pt}, from=1-3, to=1-1]
+      \arrow["{¡_{0'}}", curve={height=-12pt}, from=1-1, to=1-3]
+    \end{tikzcd}
+  \]
+  Note that by uniqueness $¡_{0'} \circ {¡'}_0 = {¡'}_{0'} = id_{0'}$ and ${¡'}_0 \circ ¡_{0'} = ¡_0 = id_0$.
+\end{proof}
+\begin{proposition}\label{prop:term_up_to} Terminal objects are unique up to isomorphism.
+\end{proposition}
+\begin{proof}
+  Let $1, 1' \in \obj{\C}$ be two terminal objects of $\C$ with the unique morphisms $!_A : A \rightarrow 1$ and ${!'}_A : A \rightarrow 1'$.
+  The isomorphism is:
+  % https://q.uiver.app/#q=WzAsMixbMCwwLCIxIl0sWzIsMCwiMSciXSxbMCwxLCJ7ISd9XzEiLDAseyJjdXJ2ZSI6LTJ9XSxbMSwwLCIhX3sxJ30iLDAseyJjdXJ2ZSI6LTJ9XV0=
+  \[
+    \begin{tikzcd}
+      1 && {1'}
+      \arrow["{{!'}_1}", curve={height=-12pt}, from=1-1, to=1-3]
+      \arrow["{!_{1'}}", curve={height=-12pt}, from=1-3, to=1-1]
+    \end{tikzcd}
+  \]
+  Note that by uniqueness ${!'}_1 \circ !_{1'} = {!'}_{1'} = id_{1'}$ and $!_{1'} \circ {!'}_1 = !_1 = id_1$.
+\end{proof}
+
+\section{Duality}
+Notice how similar the proofs of \autoref{prop:monosplitting} and \autoref{prop:episplitting} as well as \autoref{prop:init_up_to} and \autoref{prop:term_up_to} are to each other.
+It seems that we should somehow be able to construct one proof from the other, such that the work required would be halved.
+This is actually the case, we can for example say that \autoref{prop:episplitting} follows from \autoref{prop:monosplitting} by \emph{duality}.
+
+\begin{definition}[Dual Category]
+  Every category $\C$ has a \emph{dual category} $\dual{\C}$ defined by
+  \begin{itemize}
+    \item $\obj{\dual{\C}} = \obj{\C}$
+    \item $\dual{\C}(A,B) = \C(B,A)$
+  \end{itemize}
+\end{definition}
+\begin{example} Examples are:
+  \begin{enumerate}
+    \item In a poset the order relation gets reversed.
+    \item \emph{\dual{Rel}} is isomorphic to \emph{Rel}, since subsets of $A \times B$ are in bijection with subsets of $B \times A$
+    \item $\dual{(\dual{\C})} = \C$
+  \end{enumerate}
+\end{example}
+
+Every categorical notion can thus be dualized by viewing it in the dual category, some examples include:
+\begin{center}
+  \begin{tabular}{l l}
+    Notion         & Dual Notion     \\\midrule
+    Initial Object & Terminal Object \\
+    Monomorphism   & Epimorphism     \\
+    Isomorphism    & Isomorphism
+  \end{tabular}
+\end{center}
+
+This yields a proof principle ``by duality'', where every theorem yields another theorem by duality.
+
+\section{Products and Coproducts}
+The categorical abstraction of Cartesian products is:
+\begin{definition}[Product]
+  The \emph{product} of two objects $A, B \in \obj{\C}$ is an object that we call $A \times B$ together with morphisms $\pi_1 : A \times B \rightarrow A$ and $\pi_2 : A \times B \rightarrow B$ (the projections), where the following property holds:
+  % https://q.uiver.app/#q=WzAsNCxbMiwyLCJBIFxcdGltZXMgQiJdLFs0LDIsIkIiXSxbMCwyLCJBIl0sWzIsMCwiQyJdLFswLDIsIlxccGlfMSJdLFswLDEsIlxccGlfMiIsMl0sWzMsMiwiZiIsMl0sWzMsMSwiZyJdLFszLDAsIlxcZXhpc3RzIVxcbGFuZ2xlIGYsIGcgXFxyYW5nbGUiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
+  \[
+    \begin{tikzcd}
+      && C \\
+      \\
+      A && {A \times B} && B
+      \arrow["{\pi_1}", from=3-3, to=3-1]
+      \arrow["{\pi_2}"', from=3-3, to=3-5]
+      \arrow["f"', from=1-3, to=3-1]
+      \arrow["g", from=1-3, to=3-5]
+      \arrow["{\exists!\langle f, g \rangle}", dashed, from=1-3, to=3-3]
+    \end{tikzcd}
+  \]
+\end{definition}
+\begin{example} Some examples include:
+  \begin{enumerate}
+    \item \emph{Set}: The product of two sets $A$ and $B$ is the Cartesian product $A \times B = \{ (a,b)\;\vert\;a \in A, b \in B\}$.
+    \item \emph{Gra}: The product of two graphs has as vertices the Cartesian product of the vertices of both graphs and an edge $(v_1, u_1) \rightarrow (v_2, u_2)$ iff there exists edges $v_1 \rightarrow v_2$ and $u_1 \rightarrow u_2$.
+    \item \emph{Pos}: Given two posets $(A, \leq), (B, \leq)$, the product is the Cartesian product of $A$ and $B$ where $(a,b) \leq (a', b') \iff a \leq a' \land b \leq b'$.
+    \item Let $(X, \leq)$ be a poset, the product of $a, b \in X$ is the greatest lower bound of $a$ and $b$.
+  \end{enumerate}
+\end{example}
+Dual to products are:
+\begin{definition}[Coproduct]
+  The \emph{coproduct} of two objects $A, B \in \obj{\C}$ is an object that we call $A + B$ together with morphisms $i_1 : A \rightarrow A + B$ and $i_2 : B \rightarrow A + B$ (the injections), where the following property holds:
+  % https://q.uiver.app/#q=WzAsNCxbMiwwLCJBK0IiXSxbMCwwLCJBIl0sWzQsMCwiQiJdLFsyLDIsIkMiXSxbMSwwLCJpXzEiXSxbMiwwLCJpXzIiLDJdLFsxLDMsImYiLDJdLFsyLDMsImciXSxbMCwzLCJcXGV4aXN0cyFbZixnXSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
+  \[
+    \begin{tikzcd}
+      A && {A+B} && B \\
+      \\
+      && C
+      \arrow["{i_1}", from=1-1, to=1-3]
+      \arrow["{i_2}"', from=1-5, to=1-3]
+      \arrow["f"', from=1-1, to=3-3]
+      \arrow["g", from=1-5, to=3-3]
+      \arrow["{\exists![f,g]}", dashed, from=1-3, to=3-3]
+    \end{tikzcd}
+  \]
+\end{definition}
+\begin{example} Examples include:
+  \begin{enumerate}
+    \item \emph{Set}: The coproduct of two sets $A$ and $B$ is the disjoint union $A + B = \{ (a,0)\;\vert\;a \in A \} \cup \{ (b, 1) \vert b \in B \}$.
+    \item \emph{Pos}: The coproduct of ordered sets $(A, \leq)$ and $(B, \leq)$ is the disjoint union $A+B$ where $z \leq z'$ iff $z, z' \in A$ and $z \leq z'$ or $z, z' \in B$ and $z \leq z'$.
+    \item \emph{Gra}: Analogous to \emph{Pos}.
+    \item Let $(X, \leq)$ be a poset, the coproduct of $a,b \in X$ is the least upper bound of $a$ and $b$.
+    \item \emph{Rel}: Analogous to \emph{Set} the coproduct is the disjoint union. Since $\emph{Rel} \cong \dual{\emph{Rel}}$ we know that the product is also the disjoint union.
+  \end{enumerate}
+\end{example}
 
 \begin{proposition}
-  % TODO
-  $f \circ m$ mono then $m$ mono.
+  Products are unique up to isomorphism.
 \end{proposition}
+\begin{proof}
+  The usual proof is somewhat analogous to the proof of \autoref{prop:term_up_to}. Instead, we will prove it like this:
+
+  Consider the category $\emph{span}_{\C}(A,B)$ where objects are triples $A \overset{f}{\leftarrow} C \overset{g}{\rightarrow} B$ and morphisms $(C, f, g) \rightarrow (C', f', g')$ are morphisms $k : C \rightarrow C'$ in $\C$ such that
+  % https://q.uiver.app/#q=WzAsNCxbMiwwLCJDIl0sWzAsMiwiQSJdLFs0LDIsIkIiXSxbMiw0LCJDJyJdLFswLDEsImYiLDJdLFswLDIsImciXSxbMywxLCJmJyJdLFszLDIsImcnIiwyXSxbMCwzLCJrIl1d
+  \[
+    \begin{tikzcd}
+      && C \\
+      \\
+      A &&&& B \\
+      \\
+      && {C'}
+      \arrow["f"', from=1-3, to=3-1]
+      \arrow["g", from=1-3, to=3-5]
+      \arrow["{f'}", from=5-3, to=3-1]
+      \arrow["{g'}"', from=5-3, to=3-5]
+      \arrow["k", from=1-3, to=5-3]
+    \end{tikzcd}
+  \]
+  commutes. Products of $A$ and $B$ are the final objects in $\emph{span}_{\C}(A,B)$ and are thus unique up to isomorphism.
+\end{proof}
+By duality, we get:
 \begin{proposition}
-  % TODO
-  $e \circ f$ epi then $e$ epi.
+  Coproducts are unique up to isomorphism.
 \end{proposition}
-% TODO explain up to iso
+
+We can now characterize products (and later dually coproducts) as a commutative monoid:
 
 \begin{proposition}
-  % TODO
-  Initial object up to iso
+  $1$ is a unit of $\times$, i.e.\ $A \cong A \times 1$ for any $A \in \obj{\C}$.
+\end{proposition}
+% TODO proof
+\begin{proposition}
+  $\times$ is associative, i.e.\ $A \times (B \times C) \cong (A \times B) \times C$ for any $A,B,C \in \obj{\C}$.
+\end{proposition}
+% TODO proof
+\begin{proposition}
+  $\times$ is commutative, i.e.\ $A \times B \cong B \times A$ for any $A, B \in \obj{\C}$.
+\end{proposition}
+% TODO proof
+
+Duality instantly yields to commutative monoid structure of coproducts:
+\begin{proposition}
+  $0$ is the unit of $+$, i.e.\ $A \cong A + 0$ for any $A \in \obj{\C}$.
 \end{proposition}
 \begin{proposition}
-  % TODO
-  Terminal object up to iso
+  $+$ is associative, i.e.\ $A + (B + C) \cong (A + B) + C$ for any $A,B,C \in \obj{\C}$.
+\end{proposition}
+\begin{proposition}
+  $+$ is commutative, i.e.\ $A + B \cong B + A$ for any $A, B \in \obj{\C}$.
 \end{proposition}
 
-
-\subsubsection{Products and Coproducts}
-% TODO
-
-\subsection{Duality}
-\subsection{Functors}
-\subsection{Natural Transformations}
-\subsection{Functor Algebras}
-\subsection{Functor Coalgebras}
-\subsection{(co)Limits} % chktex 36
\ No newline at end of file
+\section{Functors}
+\section{Natural Transformations}
+\section{Functor Algebras}
+\section{Functor Coalgebras}
+\section{(co)Limits} % chktex 36
\ No newline at end of file
diff --git a/tex/sections/03_constructions.tex b/tex/sections/03_constructions.tex
index 4190d84..ddf04f5 100644
--- a/tex/sections/03_constructions.tex
+++ b/tex/sections/03_constructions.tex
@@ -1,4 +1,4 @@
-\section{Constructions}
-\subsection{CPO}
-\subsection{Initial Algebra Construction}
-\subsection{Terminal Coalgebra Construction}
\ No newline at end of file
+\chapter{Constructions}
+\section{CPO}
+\section{Initial Algebra Construction}
+\section{Terminal Coalgebra Construction}
\ No newline at end of file