diff --git a/doc/cubical.tex b/doc/cubical.tex
index 8ccd666..9bb74af 100644
--- a/doc/cubical.tex
+++ b/doc/cubical.tex
@@ -1,17 +1,18 @@
 \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
+Judgmental equality in Agda is a feature of the type-system. It's 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 $+$.
 
-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.
+On the other hand, propositional equality is something defined within the
+language itself. Propositional equality cannot be derived automatically. The
+normal definition of judgmental equality is an inductive data-type. Cubical Agda
+discards this type in favor of a new primitives that has certain computational
+properties exclusive to it.
 
 Exceprts of the source code relevant to this section can be found in appendix
-\ref{sec:app-cubical}.
+\S\ref{sec:app-cubical}.
 
 \subsection{The equality type}
 The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
@@ -21,7 +22,8 @@ two points of $A$; $a_0, a_1 \tp A$ we can form the type:
   a_0 \equiv a_1 \tp \MCU
 \end{align}
 %
-In Agda this is defined as an inductive data-type with the single constructor:
+In Agda this is defined as an inductive data-type with the single constructor
+for any $a \tp A$:
 %
 \begin{align}
   \refl \tp a \equiv a
@@ -29,7 +31,7 @@ In Agda this is defined as an inductive data-type with the single constructor:
 %
 For any $a \tp A$.
 
-There also exist a related notion of \emph{heterogeneous} equality where allows
+There also exist a related notion of \emph{heterogeneous} equality which 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:
 %
@@ -37,7 +39,8 @@ for equating points of different types. In this case given two types $A, B \tp
   a \cong b \tp \MCU
 \end{align}
 %
-This is likewise defined as an inductive data-type with a single constructors:
+This is likewise defined as an inductive data-type with a single constructors
+for any $a \tp A$:
 %
 \begin{align}
   \refl \tp a \cong a
@@ -47,11 +50,11 @@ 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:
+Judgmental equality in Cubical Agda is encapsulated with the type:
 %
-$$
+\begin{equation}
 \Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU
-$$
+\end{equation}
 %
 $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
@@ -62,11 +65,11 @@ 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 theory. 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:
+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
+p \tp \prod_{i \tp I} P\ i
 $$
 %
 Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the
@@ -77,16 +80,16 @@ endpoints. I.e.:
   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:
+The notion of ``homogeneous equalities'' is recovered when $P$ does not 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
+$a \equiv b$ when talking about non-dependent paths and use the notation
+$\Path\ (\lambda i \to P\ i)\ a\ b$ when the path-space is of particular
 interest.
 
 With this definition we can also recover reflexivity. That is, for any $A \tp
@@ -99,28 +102,63 @@ With this definition we can also recover reflexivity. That is, for any $A \tp
 \end{aligned}
 \end{equation}
 %
-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$.
+Here the path-space is $P \defeq \lambda i \to A$ and it satsifies $P\ i = A$
+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$.
 
-Paths have some other important properties, but they are not the focus of this
-thesis. \TODO{Refer the reader somewhere for more info.}
+It's 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
+%%   funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
+Functional extensionality is the proposition, given a type $A \tp \MCU$, a
+family of types $B \tp A \to \MCU$ and functions $f, g \tp \prod_{a \tp A}
+B\ a$:
 %
+\begin{equation}
+\label{eq:funExt}
+\var{funExt} \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g
+\end{equation}
+%
+%% p = λ i a → p a i
+So given $p \tp \prod_{a \tp A} f\ a \equiv g\ a$ we must give a path $f \equiv
+g$. That is a function $I \to \prod_{a \tp A} B\ a$. So let $i \tp I$ be given.
+We must now give an expression $\phi \tp \prod_{a \tp A} B\ a$ satisfying
+$\phi\ 0 \equiv f\ a$ and $\phi\ 1 \equiv g\ a$. This neccesitates that the
+expression must be a lambda-abstraction, so let $a \tp A$ be given. Now we can
+apply $a$ to $p$ and get the path $p\ a \tp f\ a \equiv g\ a$. And this exactly
+satisfied the conditions for $\phi$. In conclustion \ref{eq:funExt} is inhabited
+by the term:
+%
+\begin{equation}
+\label{eq:funExt}
+\var{funExt}\ p \defeq λ i\ a → p\ a\ i
+\end{equation}
+%
+With this we can now prove the desired equality $f \equiv g$ from section
+\S\ref{sec:functional-extensionality}:
+%
+\begin{align*}
+  p & \tp f \equiv g \\
+  p & \defeq \var{funExt}\ \lambda n \to \refl
+\end{align*}
+%
+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:
+don't have any interesting structure. This is referred to as Uniqueness of
+Identity Proofs (UIP). Unfortunately it is not possible to have a type-theory
+with both univalence and UIP. In stead we have a hierarchy of types with an
+increasing amount of homotopic structure. At the bottom of this hierarchy we
+have the set of contractible types:
 %
 \begin{equation}
 \begin{aligned}
 %% \begin{split}
-& \isContr    && \tp \MCU \to \MCU \\
+& \isContr    && \tp    \MCU \to \MCU \\
 & \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
 %% \end{split}
 \end{aligned}
@@ -128,8 +166,14 @@ types:
 %
 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$.
+be thought of as ``the true proposition $A$''. And indeed $\top$ is
+contractible:
+\begin{equation*}
+\var{tt} , \lambda x \to \refl \tp \isContr\ \top
+\end{equation*}
+%
+It is a theorem that if a type is contractible, then it is isomorphic to the
+unit-type.
 
 The next step in the hierarchy is the set of mere propositions:
 %
@@ -140,10 +184,18 @@ The next step in the hierarchy is the set of mere propositions:
 \end{aligned}
 \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!!}
+$\isProp\ A$ can be thought of as the set of true and false propositions. And
+indeed both $\top$ and $\bot$ are propositions:
+%
+\begin{align*}
+λ \var{tt}\ \var{tt} → refl & \tp \isProp\ ⊤ \\
+λ\varnothing\ \varnothing   & \tp \isProp\ ⊥
+\end{align*}
+%
+I've used $\varnothing$ here to denote an impossible pattern. It is a theorem
+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$.
@@ -157,10 +209,13 @@ Then comes the set of homotopical sets:
 \end{aligned}
 \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.
+I won't give an example of a set at this point. It turns out that proving e.g.
+$\isProp\ \bN$ is not so straight-forward (see \S3.1.4 in \ref{hott-2013}).
+There will be examples of sets later in this report. 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
+a proposition.
 
 The next step in the hierarchy is, as the reader might've guessed, the type:
 %
@@ -219,10 +274,13 @@ $$
 %
 We have the function:
 %
-$$
+\begin{equation}
 \pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
-$$
+\end{equation}
 %
+I will not give an example of using $\pathJ$ here. But we'll see an application
+of it in \ref{eq:pathJ-example}.
+
 \subsection{Paths over propositions}
 \label{sec:lemPropF}
 Another very useful combinator is $\lemPropF$:
diff --git a/doc/discussion.tex b/doc/discussion.tex
index 62564e6..c7c6693 100644
--- a/doc/discussion.tex
+++ b/doc/discussion.tex
@@ -26,7 +26,7 @@ disparate areas: The category-theoretic study of monads; and monads as in
 functional programming. Univalence thus allows one to reuse proofs. You could
 say that univalence gives the developer two proofs for the price of one.
 
-The introduction (section \ref{sec:context}) mentioned an often
+The introduction (section \S\ref{sec:context}) mentioned an often
 employed-technique for enabling extensional equalities is to use the
 setoid-interpretation. Nowhere in this formalization has this been necessary,
 $\Path$ has been used globally in the project as propositional equality. One
diff --git a/doc/implementation.tex b/doc/implementation.tex
index 2ce0d4e..271b30b 100644
--- a/doc/implementation.tex
+++ b/doc/implementation.tex
@@ -53,9 +53,15 @@ given type.
 For the rest of this chapter I will present some of these results. For didactic
 reasons no source-code has been included in this chapter. To see the formal
 definitions excerpts of the implementation have been included in appendix
-\ref{ch:app-sources}.
+\S\ref{ch:app-sources}:
+Appendix
+\S\ref{sec:app-categories} corresponds to section \S\ref{sec:categories},
+appendix \S\ref{sec:app-products} to section \S\ref{sec:products}
+and appendix \S\ref{sec:app-monads} to section \S\ref{sec:monads}.
+
 
 \section{Categories}
+\label{sec:categories}
 The data for a category consist of a type for the sort of objects; a type for
 the sort of arrows; an identity arrow and a composition operation for arrows.
 Another record encapsulates some laws about this data: associativity of
@@ -85,9 +91,9 @@ definitions: If we let $p$ be a witness to the identity law, which formally is:
 Then we can construct the identity isomorphism $\var{idIso} \tp \identity,
 \identity, p \tp A \approxeq A$ for any object $A$. Here $\approxeq$ denotes
 isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will
-be elaborated further on in sections \ref{sec:equiv} and \ref{sec:univalence}.
-Moreover, due to substitution for paths we can construct an isomorphism from
-\emph{any} path:
+be elaborated further on in sections \S\ref{sec:equiv} and
+\S\ref{sec:univalence}. Moreover, due to substitution for paths we can construct
+an isomorphism from \emph{any} path:
 %
 \begin{equation}
 \var{idToIso} \tp A ≡ B → A ≊ B
@@ -106,14 +112,14 @@ Note that \ref{eq:cat-univ} is \emph{not} the same as:
 %
 \begin{equation}
 \label{eq:cat-univalence}
-\tag{Univalence, category}
+%% \tag{Univalence, category}
 (A \equiv B) \simeq (A \approxeq B)
 \end{equation}
 %
 However the two are logically equivalent: One can construct the latter from the
 former simply by ``forgetting'' that $\idToIso$ plays the role of the
 equivalence. The other direction is more involved and will be discussed in
-section \ref{sec:univalence}.
+section \S\ref{sec:univalence}.
 
 In summary, the definition of a category is the following collection of data:
 %
@@ -127,14 +133,14 @@ In summary, the definition of a category is the following collection of data:
 And laws:
 %
 \begin{align}
-\tag{associativity}
+%% \tag{associativity}
 h \lll (g \lll f) ≡ (h \lll g) \lll f \\
-\tag{identity}
+%% \tag{identity}
 \identity \lll f ≡ f \x
 f \lll \identity ≡ f
 \\
 \label{eq:arrows-are-sets}
-\tag{arrows are sets}
+%% \tag{arrows are sets}
 \isSet\ (\Arrow\ A\ B)\\
 \tag{\ref{eq:cat-univ}}
 \isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso
@@ -159,7 +165,7 @@ Proving that \ref{eq:identity} is a mere proposition:
 %
 There are multiple ways to prove this. Perhaps one of the more intuitive proofs
 is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections
-\ref{sec:propPi} and \ref{sec:propSig}:
+\S\ref{sec:propPi} and \S\ref{sec:propSig}:
 %
 \begin{align*}
 \var{propPi} & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
@@ -279,7 +285,7 @@ we have shown, $\IsPreCategory$ is a proposition. However, even though
 $\Univalent$ is also a proposition, we cannot use this directly to show the
 latter. This is because $\isProp$ talks about non-dependent paths. So we need to
 'promote' the result that univalence is a proposition to a heterogeneous path.
-To this end we can use $\lemPropF$, which was introduced in \ref{sec:lemPropF}.
+To this end we can use $\lemPropF$, which was introduced in \S\ref{sec:lemPropF}.
 
 In this case $A = \var{IsIdentity}\ \identity$ and $B = \var{Univalent}$. We've
 shown that being a category is a proposition, a result that holds for any choice
@@ -476,33 +482,43 @@ what we're trying to prove but talks about paths rather than isomorphisms:
 \end{equation}
 %
 Again $p_{\var{dom}}$ denotes the path $\var{Arrow}\ A\ X \equiv
-\var{Arrow}\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$
-be given and then invoke based-path-induction. The induction will be based at $A
-\tp \var{Object}$, so let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp
-A \equiv \widetilde{B}$ be given. The family that we perform induction over will
+\var{Arrow}\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$ be
+given and then invoke based-path-induction. The induction will be based at $A
+\tp \var{Object}$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A
+\equiv \widetilde{B}$ be given. The family that we perform induction over will
 be:
 %
-$$
-\var{coe}\ {\widetilde{p}}^*\ f
+\begin{align}
+D\ \widetilde{B}\ \widetilde{p} \defeq
+  %% \prod_{\widetilde{B} \tp \Object}
+  %% \prod_{\widetilde{p} \tp A \equiv \widetilde{B}}
+  \var{coe}\ {\widetilde{p}}^*\ f
 \equiv
 f \lll \inv{(\var{idToIso}\ \widetilde{p})}
-$$
-The base-case therefore becomes:
+\end{align}
+The base-case therefore becomes
+$d \tp \var{coe}\ \refl^*\ f \equiv f \lll \inv{(\var{idToIso}\ \refl)}$
+and is inhabited by:
 \begin{align*}
-\var{coe}\ {\widetilde{\refl}}^*\ f
-& \equiv f \\
+\var{coe}\ \refl^*\ f
+& \equiv f
+  && \text{$\refl$ is a neutral element for $\var{coe}$}\\
 & \equiv f \lll \var{identity} \\
-& \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})}
+& \equiv f \lll \var{subst}\ \var{refl}\ \var{identity}
+  && \text{$\refl$ is a neutral element for $\var{subst}$}\\
+& \equiv f \lll \inv{(\var{idToIso}\ \refl)}
+  && \text{By definition of $\var{idToIso}$}\\
 \end{align*}
 %
-The first step follows because reflexivity is a neutral element for coercion.
-The second step is the identity law in the category. The last step has to do
-with the fact that $\var{idToIso}$ is constructed by substituting according to
-the supplied path and since reflexivity is also the neutral element for
-substitutions we arrive at the desired expression. To close the
-based-path-induction we must supply the value ``at the other''. In this case
-this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have.
-
+To close the based-path-induction we must supply the value ``at the other''. In
+this case this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have.
+In summary the proof of \ref{eq:coeDomIso} is the term:
+%
+\begin{equation}
+\label{eq:pathJ-example}
+\var{pathJ}\ D\ d\ B\ p
+\end{equation}
+%
 And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
 %
 \section{Categories}
@@ -546,7 +562,7 @@ arguments. Or in other words; since $\Arrow\ A\ B$ is a set for all $A\;B \tp
 \Object$ then so is $Arrow\ B\ A$.
 
 Now, to show that this category is univalent is not as straight-forward. Luckily
-section \ref{sec:equiv} gave us some tools to work with equivalences. We saw
+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
@@ -635,7 +651,7 @@ $$
 (\var{hA} \equiv \var{hB}) \simeq (\var{hA} \approxeq \var{hB})
 $$
 %
-Which, as we saw in section \ref{sec:univalence}, is sufficient to show that the
+Which, as we saw in section \S\ref{sec:univalence}, is sufficient to show that the
 category is univalent. The way that I have shown this is with a three-step
 process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show the following chain
 of equivalences:
@@ -721,7 +737,7 @@ choose:
   & \tp \var{Isomorphism}\ f \to \isEquiv\ f
 \end{align*}
 %
-As mentioned in section \ref{sec:equiv}. These maps are not in general inverses
+As mentioned in section \S\ref{sec:equiv}. These maps are not in general inverses
 of each other. In stead, we will use the fact that $A$ and $B$ are sets. The first thing we must prove is:
 %
 \begin{align*}
@@ -777,6 +793,7 @@ where we have a witness to this being a category. This is useful if this library
 is later extended to talk about higher categories.
 
 \section{Products}
+\label{sec:products}
 In the following I'll demonstrate a technique for using categories to prove
 properties. The goal in this section is to show that products are propositions:
 %
@@ -1214,6 +1231,7 @@ That in any category:
 \end{align}
 %
 \section{Monads}
+\label{sec:monads}
 In this section I present two formulations of monads. The two representations
 are referred to as the monoidal- and Kleisli- representation respectively or
 simply monoidal monads and Kleisli monads for short. We then show that the two
diff --git a/doc/introduction.tex b/doc/introduction.tex
index 12ad3b3..6dc252b 100644
--- a/doc/introduction.tex
+++ b/doc/introduction.tex
@@ -16,6 +16,7 @@ In the following two sections I present two examples that illustrate some
 limitations inherent in ITT and -- by extension -- Agda.
 %
 \subsection{Functional extensionality}
+\label{sec:functional-extensionality}
 Consider the functions:
 %
 \begin{multicols}{2}
@@ -92,7 +93,7 @@ be performed in ITT.
 
 More specifically what we are interested in is a way of identifying
 \nomen{equivalent} types. I will return to the definition of equivalence later
-in section \ref{sec:equiv}, but for now it is sufficient to think of an
+in section \S\ref{sec:equiv}, but for now it is sufficient to think of an
 equivalence as a one-to-one correspondence. We write $A \simeq B$ to assert that
 $A$ and $B$ are equivalent types. The principle of univalence says that:
 %
diff --git a/doc/macros.tex b/doc/macros.tex
index a5e03db..fad8523 100644
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -31,7 +31,7 @@
   \resizebox{\@tempdima}{\height}{=}%
 }
 \makeatother
-\newcommand{\var}[1]{\ensuremath{\mathit{#1}}}
+\newcommand{\var}[1]{\ensuremath{\mathit{#1}}\index{#1}}
 \newcommand{\Hom}{\var{Hom}}
 \newcommand{\fmap}{\var{fmap}}
 \newcommand{\bind}{\var{bind}}
@@ -86,3 +86,4 @@
 \newcommand\NT[2]{\NTsym\ #1\ #2}
 \newcommand\Endo[1]{\var{Endo}\ #1}
 \newcommand\EndoR{\mathcal{R}}
+\newcommand\funExt{\var{funExt}}
diff --git a/doc/main.tex b/doc/main.tex
index ce8bf7f..fbd7030 100644
--- a/doc/main.tex
+++ b/doc/main.tex
@@ -68,6 +68,7 @@
 \nocite{coquand-2013}
 
 \bibliography{refs}
+%% \printindex
 \begin{appendices}
 \setcounter{page}{1}
 \pagenumbering{roman}
diff --git a/doc/packages.tex b/doc/packages.tex
index 19837af..bc903cb 100644
--- a/doc/packages.tex
+++ b/doc/packages.tex
@@ -16,7 +16,8 @@
 \usepackage[toc,page]{appendix}
 \usepackage{xspace}
 \usepackage[a4paper]{geometry}
-
+\usepackage{makeidx}
+\makeindex
 % \setlength{\parskip}{10pt}
 
 % \usepackage{tikz}
diff --git a/doc/sources.tex b/doc/sources.tex
index d270c1f..0646482 100644
--- a/doc/sources.tex
+++ b/doc/sources.tex
@@ -10,6 +10,7 @@ those.
 \section{Cubical}
 \label{sec:app-cubical}
 \begin{figure}[h]
+\label{fig:path}
 \begin{Verbatim}
 postulate
   PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ