diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt
index 3c1488d..81fe0a3 100644
--- a/tex/.vscode/ltex.dictionary.en-US.txt
+++ b/tex/.vscode/ltex.dictionary.en-US.txt
@@ -32,3 +32,7 @@ iff
 posets
 coproduct
 monoid
+hom-functor
+monoids
+n-ary
+Cocartesian
diff --git a/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt
index cb4087c..1f34694 100644
--- a/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt
+++ b/tex/.vscode/ltex.hiddenFalsePositives.en-US.txt
@@ -8,3 +8,4 @@
 {"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$"}
+{"rule":"ADJECTIVE_ADVERB","sentence":"^\\QThe rest of the proof then amounts to easy rewriting.\\E$"}
diff --git a/tex/main.pdf b/tex/main.pdf
index 94387b5..6ae860e 100644
Binary files a/tex/main.pdf and b/tex/main.pdf differ
diff --git a/tex/main.tex b/tex/main.tex
index 0981baa..eb1092a 100644
--- a/tex/main.tex
+++ b/tex/main.tex
@@ -17,6 +17,7 @@
 \renewcommand{\sectionmark}[1]{\markright{\thesection\ #1}}
 \renewcommand{\subsectionmark}[1]{\markright{\thesubsection\ #1}}
 \pagestyle{scrheadings}
+\newcounter{resumeenum} % for resuming enumerated lists, https://tex.stackexchange.com/a/1702
 
 %%%%
 
@@ -129,8 +130,9 @@
 %%%
 
 %%% Notation
-%% Category C
+%% Categories
 \newcommand{\C}{\ensuremath{\mathscr{C}}}
+\newcommand{\D}{\ensuremath{\mathscr{D}}}
 %% Objects of category
 \newcommand{\obj}[1]{\ensuremath{\vert #1 \vert}}
 %% Dual category
diff --git a/tex/sections/01_introduction.tex b/tex/sections/01_introduction.tex
index f61dffc..11f2fc8 100644
--- a/tex/sections/01_introduction.tex
+++ b/tex/sections/01_introduction.tex
@@ -181,7 +181,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
     \end{tikzcd}\]
   trivially commutes.
 \end{example}
-\subsection{Lists}
+\subsection{Lists}\label{subsec: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 7794157..a55d496 100644
--- a/tex/sections/02_categories.tex
+++ b/tex/sections/02_categories.tex
@@ -247,17 +247,31 @@ We can now characterize products (and later dually coproducts) as a commutative
 \begin{proposition}
   $1$ is a unit of $\times$, i.e.\ $A \cong A \times 1$ for any $A \in \obj{\C}$.
 \end{proposition}
-% TODO proof
+\begin{proof}
+  Take $\langle id_A , !_A \rangle : A \rightarrow A \times 1$ and $\pi_1 : A \times 1 \rightarrow A$, this indeed constitutes an isomorphism, since
+  \[\pi_1 \circ \langle id_A , !_A \rangle = id_A \]
+  by definition and
+  \[\langle id_A , !_A \rangle \circ \pi_1 = \langle \pi_1 , !_A \rangle = \langle \pi_1 , \pi_2 \rangle = id_{A \times 1},\]
+  because $\pi_2 = !_A : A \times 1 \rightarrow 1$ by uniqueness of $!_A$.
+\end{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{proof}
+  Take \[\alpha = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : A \times (B \times C) \rightarrow (A \times B) \times C\]
+  and \[\alpha^{-1} = \langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle : (A \times B) \times C \rightarrow A \times (B \times C).\]
+  The rest of the proof then amounts to simply rewriting.
+\end{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
+\begin{proof}
+  Take \[\langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A\]
+  and \[\langle \pi_2 , \pi_1 \rangle : B \times A \rightarrow A \times B.\]
+  Indeed, $\langle \pi_2 , \pi_1 \rangle \circ \langle \pi_2 , \pi_1 \rangle = \langle \pi_2 \circ \langle \pi_2 , \pi_1 \rangle , \pi_1 \circ \langle \pi_2 , \pi_1 \rangle \rangle = \langle \pi_1 , \pi_2 \rangle = id$.
+\end{proof}
 
-Duality instantly yields to commutative monoid structure of coproducts:
+Duality instantly yields the 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}
@@ -268,7 +282,102 @@ Duality instantly yields to commutative monoid structure of coproducts:
   $+$ is commutative, i.e.\ $A + B \cong B + A$ for any $A, B \in \obj{\C}$.
 \end{proposition}
 
+\begin{remark}
+  If a category has a terminal object and binary products one can form arbitrary n-ary products (finite products), such a category is called \emph{Cartesian}. Dually a category with an initial object and binary coproducts is called \emph{Cocartesian}.
+\end{remark}
+
 \section{Functors}
+Functors are morphisms between categories, concretely:
+\begin{definition}[Functor]
+  A functor $F : \C \rightarrow \D$ consists of
+  \begin{itemize}
+    \item a mapping $F : \obj{\C} \rightarrow \obj{\D}$ on objects and
+    \item a mapping $F : \C(A,B) \rightarrow \C(FA,FB)$ on morphisms,
+  \end{itemize}
+  such that $F(id_A) = id_{FA}$ and $F(g \circ f) = Fg \circ Ff$.
+\end{definition}
+\begin{example} Usual examples of functors include
+  \begin{enumerate}
+    \item Constant functors mapping to a single object: $D! : \C \rightarrow \D, D \in \obj{\D}$ with
+          \[D!(C) = D, \qquad D!(f) = id_D.\]
+    \item Identity functor: $Id_\C : \C \rightarrow \C$ with
+          \[Id_\C(C) = C, \qquad Id_\C(f) = f.\]
+    \item Composition of functors: $(FG)(X) = F(GX), (FG)(f) = F(Gf)$
+    \item Square functor on $\emph{Set}$: $Q : \emph{Set} \rightarrow \emph{Set}$ with
+          \[QX = X \times X, \qquad Qf = f \times f.\]
+    \item $list : Set \rightarrow Set$, see \autoref{subsec:lists}.
+    \item For $A \in \obj{\C}$ there is the hom-functor $\C(A,-) : \C \rightarrow Set$ given by
+          \[ \C(A,B), \qquad \C(A,f : B \rightarrow B')(h : A \rightarrow B) = f \circ h : \C(A,B').\]
+    \item Functors between posets are monotonous maps, which in turn are the morphisms in $\emph{Pos}$.
+    \item Functors between monoids are monoid homomorphisms, which in turn are the morphisms in $\emph{Mon}$.
+    \item The power set functor $\mathscr{P} : \emph{Set} \rightarrow \emph{Set}$ defined by
+          \begin{alignat*}{2}
+             & \mathscr{P}X    &  & = \{ Y\;\vert\; Y \subseteq X \}                 \\
+             & (\mathscr{P}f)Y &  & = f[Y] \subseteq X', \text{ for } Y \subseteq X.
+          \end{alignat*}
+    \item If $\C$ is a category that adds some structure to sets (like \emph{Mon} or \emph{Pos}) one usually can construct a \emph{forgetful functor} $U : \C \rightarrow \emph{Set}$, e.g.
+          \begin{alignat*}{4}
+             & U_{\emph{Pos}} : \emph{Pos} &  & \rightarrow \emph{Set}; \qquad &  & (X, \leq)     &  & \mapsto X \\
+             & U_{\emph{Mon}} : \emph{Mon} &  & \rightarrow \emph{Set}; \qquad &  & (M, \cdot, e) &  & \mapsto M
+          \end{alignat*}
+          \setcounter{resumeenum}{\value{enumi}}
+  \end{enumerate}
+\end{example}
+
+Using functors as morphisms, one can \emph{almost} build a category $\emph{CAT}$ of \emph{all} categories, however the collection of all categories is not a class (as required) but a \emph{conglomerate}, thus $\emph{CAT}$ is called a \emph{quasi-category}. The small categories (i.e.\ where the collection of objects is a set) form a `real' category $\emph{Cat}$.
+
+We can however consider structures like products and isomorphisms in the quasi-category $\emph{CAT}$:
+\begin{definition}[Products of Categories]
+  The product of two categories $\C, \D$ consists of
+  \begin{itemize}
+    \item $\obj{\C \times \D} = \obj{\C} \times \obj{\D}$,
+    \item $(\C \times \D)((A_1, A_2),(B_1,B_2)) = \C(A_1, B_1) \times D(A_2, B_2)$,
+  \end{itemize}
+  with projection functors $\pi_1 : \C \times \D \rightarrow \C, \pi_2 : \C \times \D \rightarrow \D$.
+\end{definition}
+\begin{example} More examples of functors include:
+  \begin{enumerate} \setcounter{enumi}{\value{resumeenum}}
+    \item The Cartesian product functor: $-\times- : \emph{Set} \times \emph{Set} \rightarrow \emph{Set}$.
+    \item The binary hom-functor $\C(-,-) : \dual{\C} \times \C \rightarrow \emph{Set}$ with
+          \[\C(A,B), \qquad \C(g : X' \rightarrow X, f : Y \rightarrow Y')(h : X \rightarrow Y) = f \circ h \circ g : \C(X',Y').\]
+          \setcounter{resumeenum}{\value{enumi}}
+  \end{enumerate}
+\end{example}
+
+\begin{definition}[Covariant and Contravariant Functors]
+  A functor $F : \dual{\C} \rightarrow \D$ is called a \emph{contravariant} functor $\C \rightarrow \D$. For differentiation, we call `normal' functors $\C \rightarrow \D$ \emph{covariant}.
+\end{definition}
+\begin{example} Examples of contravariant functors include:
+  \begin{enumerate} \setcounter{enumi}{\value{resumeenum}}
+    \item For every $Y \in \obj{\C}$ there is a contravariant hom-functor $\C(-,Y) : \dual{\C} \rightarrow \emph{Set}$ given by
+          \[\C(X,Y), \qquad \C(f : X' \rightarrow X, Y)(h : X \rightarrow Y) = h \circ f : \C(X', Y).\]
+    \item $2^{(-)} : \dual{\emph{Set}} \rightarrow \emph{Set}$ where
+          \[2^X = \{ f : X \rightarrow 2 \} \cong \mathscr{P}X\]
+          and
+          \[2^{(f : X \rightarrow Y)} : 2^Y \rightarrow 2^X \cong \mathscr{P}Y \rightarrow \mathscr{P}X, \qquad Z \mapsto \{ x \;\vert\; fx \in Z \} = f^{-1}[Z] \subseteq X.\]
+    \item For every functor $F : \C \rightarrow \D$ the identical functor $\dual{F} : \dual{\C} \rightarrow \dual{\D}$, given by
+          \[\dual{F}C = FC, \qquad \dual{F}f = Ff.\]
+  \end{enumerate}
+\end{example}
+
+Isomorphisms of categories are the isomorphisms in the quasi-category $\emph{CAT}$, thus a functor is an isomorphism iff he is bijective on both objects and morphisms. However, oftentimes categories are not isomorphic but instead \emph{equivalent} in the following sense:
+
+\begin{definition}[Equivalence Functors]
+  A functor $F : \C \rightarrow \D$ is called
+  \begin{itemize}
+    \item \emph{full} if every $F : \C(A,B) \rightarrow \D(FA,FB)$ is surjective,
+    \item \emph{faithful} if every $F : \C(A,B) \rightarrow \D(FA,FB)$ is injective,
+    \item \emph{essentially surjective (dense)} if for every $D \in \D$ there exists a $C \in \C$ such that $D \cong FC$,
+    \item an \emph{equivalence} if $F$ is full, faithful and dense.
+  \end{itemize}
+\end{definition}
+\begin{example} Let us consider two examples of equivalent categories:
+  \begin{enumerate}
+    \item The category $\emph{Par}$ is equivalent to $\emph{Set}_p$, which is the category of pointed sets, where objects are tuples $(X,p), p \in X$ and morphisms are point-preserving.
+    \item The product category $\emph{Set} \times \emph{Set}$ is equivalent to the \emph{slice category} $\emph{Set}/2$, where objects are maps $X \rightarrow 2$ and morphisms $h : (X \overset{f}{\rightarrow} 2) \rightarrow (Y \overset{g}{\rightarrow} 2)$ are maps $h : X \rightarrow Y$ such that $g \circ h = f$.
+  \end{enumerate}
+\end{example}
+
 \section{Natural Transformations}
 \section{Functor Algebras}
 \section{Functor Coalgebras}