diff --git a/doc/cubical.tex b/doc/cubical.tex
index c9c6ece..d45c1fd 100644
--- a/doc/cubical.tex
+++ b/doc/cubical.tex
@@ -1,6 +1,6 @@
 \chapter{Cubical Agda}
 \section{Propositional equality}
-Judgmental equality in Agda is a feature of the type-system. It's something that
+Judgmental equality in Agda is a feature of the type-system. Its something that
 can be checked automatically by the type-checker: In the example from the
 introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the
 definition of $+$.
@@ -81,7 +81,7 @@ endpoints. I.e.:
 \end{align*}
 %
 The notion of ``homogeneous equalities'' is recovered when $P$ does not depend
-on it's argument:
+on its argument:
 %
 $$
 a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1
@@ -107,7 +107,7 @@ definitionally. So to inhabit it, is to give a path $I \to A$ which is
 judgmentally $a$ at either endpoint. This is satisfied by the constant path;
 i.e. the path that stays at $a$ at any index $i$.
 
-It's also surpisingly easy to show functional extensionality with which we can
+It is also surpisingly easy to show functional extensionality with which we can
 construct a path between $f$ and $g$ -- the function defined in the introduction
 (section \S\ref{sec:functional-extensionality}).
 %% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where
@@ -335,8 +335,8 @@ $$
 \subsection{Pairs over propositions}
 \label{sec:propSig}
 %
-$\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
+$\sum$-types preserve propositionality whenever its first component is a
+proposition, and its second component is a proposition for all points of in the
 left type.
 %
 $$
diff --git a/doc/implementation.tex b/doc/implementation.tex
index 676fa60..6e91000 100644
--- a/doc/implementation.tex
+++ b/doc/implementation.tex
@@ -70,7 +70,7 @@ constituents of a category and can be found in typical mathematical expositions
 on the topic. We, however, impose one further requirement on what it means to be
 a category, namely that the type of arrows form a set.
 
-Such categories are called \nomen{1-categories}. It's possible to relax this
+Such categories are called \nomen{1-categories}. It is possible to relax this
 requirement. This would lead to the notion of higher categories (\cite[p.
   307]{hott-2013}). For the purpose of this project, however, this report will
 restrict itself to 1-categories. Making based on higher categories would be a
@@ -367,7 +367,7 @@ $$
 \fiber\ f\ b \defeq \sum_{a \tp A} \left( b \equiv f\ a \right)
 $$
 %
-I give it's definition here mainly for completeness, because as I stated we can
+I give its definition here mainly for completeness, because as I stated we can
 move away from this specific instantiation and think about it more abstractly
 once we have shown that this definition actually works as an equivalence.
 
@@ -420,7 +420,7 @@ $$
 $$
 %
 That is, we must demonstrate that there is an isomorphism (on types) between
-equalities and isomorphisms (on arrows). It's worthwhile to dwell on this for a
+equalities and isomorphisms (on arrows). It is worthwhile to dwell on this for a
 few seconds. This type looks very similar to univalence for types and is
 therefore perhaps a bit more intuitive to grasp the implications of. Of course
 univalence for types (which is a proposition -- i.e. provable) does not imply
@@ -525,7 +525,7 @@ And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
 \subsection{Opposite category}
 \label{op-cat}
 The first category I'll present is a pure construction on categories. Given some
-category we can construct it's dual, called the opposite category. Starting with
+category we can construct its dual, called the opposite category. Starting with
 a simple example allows us to focus on how we work with equivalences and
 univalence in a very simple category where the structure of the category is
 rather simple.
@@ -566,12 +566,12 @@ section \S\ref{sec:equiv} gave us some tools to work with equivalences. We saw
 that we can prove this category univalent by giving an inverse to
 $\wideoverbar{\idToIso} \tp (A \equiv B) \to (A \wideoverbar{\approxeq} B)$.
 From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong
-B)$ is an isomorphism. Let us denote it's inverse with $\isoToId \tp (A
+B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A
 \approxeq B) \to (A \equiv B)$. If we squint we can see what we need is a way to
 go between $\wideoverbar{\approxeq}$ and $\approxeq$.
 
 An inhabitant of $A \approxeq B$ is simply an arrow $f \tp \Arrow\ A\ B$
-and it's inverse $g \tp \Arrow\ B\ A$. In the opposite category $g$ will
+and its inverse $g \tp \Arrow\ B\ A$. In the opposite category $g$ will
 play the role of the isomorphism and $f$ will be the inverse. Similarly we can
 go in the opposite direction. I name these maps $\shuffle \tp (A \approxeq
 B) \to (A \wideoverbar{\approxeq} B)$ and $\shuffle^{-1} \tp (A
@@ -832,7 +832,7 @@ $\pi$ is called the product (arrow) of $f$ and $g$.
 \newcommand\pairB{\mathcal{B}}
 Given a base category $\bC$ and two objects in this category $\pairA$ and
 $\pairB$ we can construct the ``pair category'': \TODO{This is a working title,
-  it's nice to have a name for this thing to refer back to}
+  it is nice to have a name for this thing to refer back to}
 
 The type of objects in this category will be an object in the underlying
 category, $X$, and two arrows (also from the underlying category)
@@ -1291,7 +1291,7 @@ The Kleisli-formulation consists of the following data:
 %
 The objects $X$ and $Y$ are implicitly universally quantified.
 
-It's interesting to note here that this formulation does not talk about natural
+It is interesting to note here that this formulation does not talk about natural
 transformations or other such constructs from category theory. All we have here
 is a regular maps on objects and a pair of arrows.
 %
diff --git a/doc/sources.tex b/doc/sources.tex
index 0646482..080e875 100644
--- a/doc/sources.tex
+++ b/doc/sources.tex
@@ -1,4 +1,4 @@
-\chapter{Source code}
+\chapter{Source code excerpts}
 \label{ch:app-sources}
 In the following a few of the definitions mentioned in the report are included.
 The following is \emph{not} a verbatim copy of individual modules from the
@@ -6,7 +6,6 @@ implementation. Rather, this is a redacted and pre-formatted designed for
 presentation purposes. It's provided here as a convenience. The actual sources
 are the only authoritative source. Is something is not clear, please refer to
 those.
-\clearpage
 \section{Cubical}
 \label{sec:app-cubical}
 \begin{figure}[h]
@@ -24,6 +23,7 @@ module _ {ℓ} {A : Set ℓ} where
 \end{Verbatim}
 \caption{Excerpt from the cubical library. Definition of the path-type.}
 \end{figure}
+\clearpage
 %
 \begin{figure}[h]
 \begin{Verbatim}