diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty
index 9c55586..64ddad3 100644
--- a/doc/chalmerstitle.sty
+++ b/doc/chalmerstitle.sty
@@ -41,6 +41,7 @@
 \newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm}
 \begingroup
 \usepackage{noto}
+\fontseries{sb}
 %% \fontfamily{noto}\selectfont
 {\Huge\@title}\\[.5cm]
 {\Large A formalization of category theory in Cubical Agda}\\[.5cm]
diff --git a/doc/cubical.tex b/doc/cubical.tex
new file mode 100644
index 0000000..0fc8cbb
--- /dev/null
+++ b/doc/cubical.tex
@@ -0,0 +1,275 @@
+\chapter{Cubical Agda}
+\section{Propositional equality}
+In Agda judgmental equality is a feature of the type-system. It's a property of
+types that can be checked by computational means. In the example from the
+introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the
+definition of $+$.
+
+Propositional equality on the other hand is defined within the language itself.
+Cubical Agda extends the underlying type system (\TODO{Cite someone smarter than
+me with a good resource on this}) but introduces a data-type within the
+languages.
+
+\subsection{The equality type}
+The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
+two points of $A$; $a_0, a_1 \tp A$ we can form the type:
+%
+\begin{align}
+  a_0 \equiv a_1 \tp \MCU
+\end{align}
+%
+In Agda this is defined as an inductive data-type with the single constructor:
+%
+\begin{align}
+  \refl \tp a \equiv a
+\end{align}
+%
+For any $a \tp A$.
+
+There also exist a related notion of \emph{heterogeneous} equality where allows
+for equating points of different types. In this case given two types $A, B \tp
+\MCU$ and two points $a \tp A$, $b \tp B$ we can construct the type:
+%
+\begin{align}
+  a \cong b \tp \MCU
+\end{align}
+%
+This is likewise defined as an inductive data-type with a single constructors:
+%
+\begin{align}
+  \refl \tp a \cong a
+\end{align}
+%
+In Cubical Agda these two notions are paralleled with homogeneous- and
+heterogeneous paths respectively.
+%
+\subsection{The path type}
+In Cubical Agda judgmental equality is encapsulated with the type:
+%
+$$
+\Path \tp (P : I → \MCU) → P\ 0 → P\ 1 → \MCU
+$$
+%
+$I$ is a special data-type (\TODO{that also has special computational properties
+  AFAIK}) called the index set. $I$ can be thought of simply as the interval on
+the real numbers from $0$ to $1$. $P$ is a family of types over the index set
+$I$. I will sometimes refer to $P$ as the ``path-space'' of some path $p \tp
+\Path\ P\ a\ b$. By this token $P\ 0$ then corresponds to the type at the
+left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called
+$\Path$ because it is connected with paths in homotopy thoery. The intuition
+behind this is that $\Path$ describes paths in $\MCU$ -- i.e. between types. For
+a path $p$ for the point $p\ i$ the index $i$ describes how far along the path
+one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-)
+function, $p$, from the index-space to the path-space:
+%
+$$
+p \tp I \to P\ i
+$$
+%
+Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the
+endpoints. I.e.:
+%
+\begin{align*}
+  p\ 0 & = a_0 \\
+  p\ 1 & = a_1
+\end{align}
+%
+The notion of ``homogeneous equalities'' can be recovered by not letting the
+path-space $P$ depend on it's argument:
+%
+$$
+a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1
+$$
+%
+For $A \tp \MCU$, $a_0, a_1 \tp A$. I will generally prefer to use the notation
+$a_0 \equiv a_1$ when talking about non-dependent paths and use the notation
+$\Path\ (\lambda i \to A)\ a_0\ a_1$ when the path-space is of particular
+interest.
+
+With this definition we can also recover reflexivity. That is, for any $A \tp
+\MCU$ and $a \tp A$:
+%
+\begin{align}
+\refl & \tp \Path (\lambda i \to A)\ a\ a \\
+\refl & \defeq \lambda i \to a
+\end{align}
+%
+Or, in other terms; reflexivity is the path in $A$ that is $a$ at the left
+endpoint as well as at the right endpoint. It is inhabited by the path which
+stays constantly at $a$ at any index $i$.
+
+Paths have some other important properties, but they are not the focus of this
+thesis. \TODO{Refer the reader somewhere for more info.}
+%
+\section{Homotopy levels}
+In ITT all equality proofs are identical (in a closed context). This means that,
+in some sense, any two inhabitants of $a \equiv b$ are ``equally good'' -- they
+don't have any interesting structure. This is referred to as uniqueness of
+identity proofs. Unfortunately this is orthogonal to univalence that only makes
+sense in the absence of UIP.
+
+In homotopy type theory we have a hierarchy of types based on their ``internal
+structure''. At the bottom of this hierarchy we have the set of contractible
+types:
+%
+\begin{equation}
+\begin{alignat}{2}
+& \isContr    && \tp \MCU \to \MCU \\
+& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
+\end{alignedat}
+\end{equation}
+%
+The first component of $\isContr\ A$ is called ``the center of contraction''.
+Under the propositions-as-types interpretation of type-theory $\isContr\ A$ can
+be thought of as ``the true proposition $A$''. It is a theorem that if a type is
+contractible, then it is isomorphic to the unit-type $\top$.
+
+The next step in the hierarchy is the set of mere propositions:
+%
+\begin{equation}
+\begin{alignat}{2}
+& \isProp    && \tp \MCU \to \MCU \\
+& \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1
+\end{alignedat}
+\end{equation}
+%
+$\isProp\ A$ can be thought of as the set of true and false propositions. It is
+a result that if a mere proposition $A$ is inhabited, then so is it
+contractible. If it is not inhabited it is equivalent to the empty-type (or
+false proposition).\TODO{Cite!!}
+
+I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to
+stress that we have $\isProp\ A$.
+
+Then comes the set of homotopical sets:
+%
+\begin{equation}
+\begin{alignat}{2}
+& \isSet    && \tp \MCU \to \MCU \\
+& \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1)
+\end{alignedat}
+\end{equation}
+%
+At this point it should be noted that the term ``set'' is somewhat conflated;
+there is the notion of sets from set-theory, in Agda types are denoted
+\texttt{Set}. I will use it consistently to refer to a type $A$ as a set exactly
+if $\isSet\ A$ is inhabited.
+
+The next step in the hierarchy is, as you might've guessed, the type:
+%
+\begin{equation}
+\begin{alignat}{2}
+& \isGroupoid    && \tp \MCU \to \MCU \\
+& \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1)
+\end{alignedat}
+\end{equation}
+%
+And so it continues. In fact we can generalize this family of types by indexing
+them with a natural number. For historical reasons, though, the bottom of the
+hierarchy, the contractible tyes, is said to be a \nomen{-2-type}, propositions
+are \nomen{-1-types}, (homotopical) sets are \nomen{0-types} and so on\ldots
+
+Just as with paths, homotopical sets are not at the center of focus for this
+thesis. But I mention here some properties that will be relevant for this
+exposition:
+
+Proposition: Homotopy levels are cumulative. That is, if $A \tp \MCU$ has
+homotopy level $n$ then so does it have $n + 1$.
+
+Let $\left\Vert A \right\Vert = n$ denote that the level of $A$ is $n$.
+Proposition: For any homotopic level $n$ this is a mere proposition.
+%
+\section{A few lemmas}
+Rather than getting into the nitty-gritty details of Agda I venture to take a
+more ``combinators-based'' approach. That is, I will use theorems about paths
+already that have already been formalized. Specifically the results come from
+the Agda library \texttt{cubical} (\TODO{Cite}). I have used a handful of
+results from this library as well as contributed a few lemmas myself.\footnote{The module \texttt{Cat.Prelude} lists the upstream dependencies. As well my contribution to \texttt{cubical} can be found in the git logs \TODO{Cite}.}
+
+These theorems are all purely related to homotopy theory and cubical agda and as
+such not specific to the formalization of Category Theory. I will present a few
+of these theorems here, as they will be used later in chapter
+\ref{ch:implementation} throughout.
+
+\subsection{Path induction}
+The induction principle for paths intuitively gives us a way to reason about a
+type-family indexed by a path by only considering if said path is $\refl$ (the
+``base-case''). For \emph{based path induction}, that equaility is \emph{based}
+at some element $a \tp A$.
+
+Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types:
+%
+$$
+P \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} \MCU
+$$
+%
+And an inhabitant of $P$ at $\refl$:
+%
+$$
+p \tp P\ a\ \refl
+$$
+%
+We have the function:
+%
+$$
+\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
+$$
+%
+\subsection{Paths over propositions}
+Another very useful combinator is $\lemPropF$:
+
+To `promote' this to a dependent path we can use another useful combinator;
+$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $P \tp A \to
+\MCU$. Let $\var{propP} \tp \prod_{x \tp A} \isProp\ (P\ x)$ be the proof that
+$P$ is a mere proposition for all elements of $A$. Furthermore say we have a
+path between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can built
+a heterogeneous path between any two elements of $p_0 \tp P\ a_0$ and $p_1 \tp
+P\ a_1$:
+%
+$$
+\lemPropF\ \var{propP}\ p \defeq \Path\ (\lambda\; i \mto P\ (p\ i))\ p_0\ p_1
+$$
+%
+This is quite a mouthful. So let me try to show how this is a very general and
+useful result.
+
+Often when proving equalities between elements of some dependent types
+$\lemPropF$ can be used to boil this complexity down to showing that the
+dependent parts of the type are mere propositions. For instance, saw we have a type:
+%
+$$
+T \defeq \sum_{a : A} P\ a
+$$
+%
+For some proposition $P \tp A \to \MCU$. If we want to prove $t_0 \equiv t_1$
+for two elements $t_0, t_1 \tp T$ then this will be a pair of paths:
+%
+%
+\begin{align*}
+  p \tp & \fst\ t_0 \equiv \fst\ t_1 \\
+        & \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
+\end{align*}
+%
+Here $\lemPropF$ directly allow us to prove the latter of these:
+%
+$$
+\lemPropF\ \var{propP}\ p
+  \tp \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
+$$
+%
+\subsection{Functions over propositions}
+$\prod$-types preserve propositionality when the co-domain is always a
+proposition.
+%
+$$
+\mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
+$$
+\subsection{Pairs over propositions}
+%
+$\sum$-types preserve propositionality whenever it's first component is a
+proposition, and it's second component is a proposition for all points of in the
+left type.
+%
+$$
+\mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
+$$
diff --git a/doc/implementation.tex b/doc/implementation.tex
index 9194bae..f1ad008 100644
--- a/doc/implementation.tex
+++ b/doc/implementation.tex
@@ -1,5 +1,6 @@
-\chapter{Implementation}
-This implementation formalizes the following concepts $>\!\!>\!\!=$:
+\chapter{Category Theory}
+\label{ch:implementation}
+This implementation formalizes the following concepts:
 %
 \begin{itemize}
 \item Core categorical concepts
@@ -224,19 +225,18 @@ $$
 \isoToId \tp (A \approxeq B) \to (A \equiv B)
 $$
 %
-One application of this, and a perhaps somewhat surprising result, is that
-terminal objects are propositional. Intuitively; they do not
-have any interesting structure:
+A perhaps somewhat surprising application of this is that we can show that
+terminal objects are propositional:
 %
 \begin{align}
 \label{eq:termProp}
 \isProp\ \var{Terminal}
 \end{align}
 %
-The proof of this follows from the usual
-observation that any two terminal objects are isomorphic. The proof is omitted
-here, but the curious reader can check the implementation for the details.
-\TODO{The proof is a bit fun, should I include it?}
+It follows from the usual observation that any two terminal objects are
+isomorphic - and since categories are univalent, so are they equal. The proof is
+omitted here, but the curious reader can check the implementation for the
+details. \TODO{The proof is a bit fun, should I include it?}
 
 \section{Equivalences}
 \label{sec:equiv}
@@ -477,21 +477,21 @@ direction. I name these maps $\mathit{shuffle} \tp (A \approxeq B) \to (A
 \approxeq B)$ respectively.
 
 As the inverse of $\idToIso_{\mathit{Op}}$ I will pick $\zeta \defeq \eta \comp
-\mathit{shuffle}$. The proof that they are inverses go as follows:
+\var{shuffle}$. The proof that they are inverses go as follows:
 %
 \begin{align*}
 \zeta \comp \idToIso & \equiv
-\eta \comp \shuffle \comp \idToIso
+\eta \comp \var{shuffle} \comp \idToIso
 && \text{by definition} \\
 %% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\
 %
 & \equiv
-\eta \comp \shuffle \comp \inv{\shuffle} \comp \idToIso
+\eta \comp \var{shuffle} \comp \inv{\var{shuffle}} \comp \idToIso
 && \text{lemma} \\
 %%   ≡⟨⟩ \\
 & \equiv
 \eta \comp \idToIso_{\bC}
-&& \text{$\shuffle$ is an isomorphism} \\
+&& \text{$\var{shuffle}$ is an isomorphism} \\
 %%   ≡⟨ (λ i → verso-recto i x) ⟩ \\
 & \equiv
 \identity
@@ -500,7 +500,7 @@ As the inverse of $\idToIso_{\mathit{Op}}$ I will pick $\zeta \defeq \eta \comp
 %
 The other direction is analogous.
 
-The lemma used in this proof states that $\idToIso \equiv \inv{\shuffle} \comp
+The lemma used in this proof states that $\idToIso \equiv \inv{\var{shuffle}} \comp
 \idToIso_{\bC}$ it's a rather straight-forward proof since being-an-inverse-of
 is a proposition.
 
diff --git a/doc/introduction.tex b/doc/introduction.tex
index 97306de..24442e9 100644
--- a/doc/introduction.tex
+++ b/doc/introduction.tex
@@ -155,16 +155,3 @@ all judgemental equalites of type theory, is cumbersome to work with in practice
 (\cite[p. 4]{huber-2016}) and makes equational proofs less reusable since
 equational proofs $a \sim_{X} b$ are inherently `local' to the extensional set
 $(X , \sim)$.
-%
-\section{The equality type}
-The usual definition of equality in Agda is an inductive data-type with a single
-constructor:
-%
-%% \VerbatimInput{../libs/main.tex}
-% \def\verbatim@font{xits}
-\begin{verbatim}
-data _≡_ {a} {A : Set a} (x : A) : A → Set a where
-  instance refl : x ≡ x
-\end{verbatim}
-%
-I shall refer to this as the (usual) inductive equality type.
diff --git a/doc/macros.tex b/doc/macros.tex
index 23ce2c3..0ce9273 100644
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -47,6 +47,8 @@
 \newcommand{\idToIso}{\var{idToIso}}
 \newcommand{\isSet}{\var{isSet}}
 \newcommand{\isContr}{\var{isContr}}
+\newcommand{\isGroupoid}{\var{isGroupoid}}
+\newcommand{\pathJ}{\var{pathJ}}
 \newcommand\Object{\var{Object}}
 \newcommand\Functor{\var{Functor}}
 \newcommand\isProp{\var{isProp}}
diff --git a/doc/main.tex b/doc/main.tex
index b0946e1..76ea1b8 100644
--- a/doc/main.tex
+++ b/doc/main.tex
@@ -43,6 +43,7 @@
 \researchgroup{Programming Logic Group}
 \bibliographystyle{plain}
 
+
 \begin{document}
 
 \pagenumbering{roman}
@@ -51,6 +52,7 @@
 %
 \pagenumbering{arabic}
 \input{introduction.tex}
+\input{cubical.tex}
 \input{implementation.tex}
 
 \nocite{cubical-demo}