diff --git a/Makefile b/Makefile
index bec101b..6f8e63d 100644
--- a/Makefile
+++ b/Makefile
@@ -4,8 +4,10 @@ build: src/**.agda
 clean:
 	find src -name "*.agdai" -type f -delete
 
-html:
+html: src/**.agda
 	agda --html src/Cat.agda
 
 upload: html
 	scp -r html/ remote11.chalmers.se:www/cat/doc/
+
+.PHONY: upload clean
diff --git a/doc/.gitignore b/doc/.gitignore
index b4bbda9..4832088 100644
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -4,6 +4,7 @@
 *.log
 *.out
 *.pdf
+!assets/**
 *.bbl
 *.blg
 *.toc
@@ -11,4 +12,4 @@
 *.ilg
 *.ind
 *.nav
-*.snm
\ No newline at end of file
+*.snm
diff --git a/doc/BACKLOG.md b/doc/BACKLOG.md
index fc8de53..f6433d1 100644
--- a/doc/BACKLOG.md
+++ b/doc/BACKLOG.md
@@ -1,3 +1,13 @@
+Presentation
+====
+Find one clear goal.
+
+Remember crowd-control.
+
+Leave out:
+  lemPropF
+
+
 Talk about structure of library:
 ===
 
diff --git a/doc/abstract.tex b/doc/abstract.tex
index 17b3853..056dd94 100644
--- a/doc/abstract.tex
+++ b/doc/abstract.tex
@@ -1,18 +1,18 @@
 \chapter*{Abstract}
 The usual notion of propositional equality in intensional type-theory
-is restrictive. For instance it does not admit functional
-extensionality nor univalence. This poses a severe limitation on both
-what is \emph{provable} and the \emph{re-usability} of proofs. Recent
+is restrictive.  For instance it does not admit functional
+extensionality nor univalence.  This poses a severe limitation on both
+what is \emph{provable} and the \emph{re-usability} of proofs.  Recent
 developments have however resulted in cubical type theory which
-permits a constructive proof of these two important notions. The
+permits a constructive proof of these two important notions.  The
 programming language Agda has been extended with capabilities for
-working in such a cubical setting. This thesis will explore the
+working in such a cubical setting.  This thesis will explore the
 usefulness of this extension in the context of category theory.
 
 The thesis will motivate the need for univalence and explain why
 propositional equality in cubical Agda is more expressive than in
-standard Agda. Alternative approaches to Cubical Agda will be
-presented and their pros and cons will be explained. As an example of
+standard Agda.  Alternative approaches to Cubical Agda will be
+presented and their pros and cons will be explained.  As an example of
 the application of univalence two formulations of monads will be
 presented: Namely monads in the monoidal form and monads in the
 Kleisli form and under the univalent interpretation it will be shown
@@ -20,5 +20,5 @@ how these are equal.
 
 Finally the thesis will explain the challenges that a developer will
 face when working with cubical Agda and give some techniques to
-overcome these difficulties. It will also try to suggest how further
+overcome these difficulties.  It will also try to suggest how further
 work can help alleviate some of these challenges.
diff --git a/doc/acknowledgement.tex b/doc/acknowledgement.tex
deleted file mode 100644
index 5cd6cc3..0000000
--- a/doc/acknowledgement.tex
+++ /dev/null
@@ -1 +0,0 @@
-\chapter*{Acknowledgements}
diff --git a/doc/acknowledgements.tex b/doc/acknowledgements.tex
index e4c45e3..882d59b 100644
--- a/doc/acknowledgements.tex
+++ b/doc/acknowledgements.tex
@@ -7,7 +7,7 @@ can conjure up various proofs.  I also want to recognize the support
 of Knud Højgaards Fond who graciously sponsored me with a 20.000 DKK
 scholarship which helped toward sponsoring the two years I have spent
 studying abroad. I would also like to give a warm thanks to my fellow
-students Pierre Kraft and Nachiappan Villiappan who have made the time
+students Pierre~Kraft and Nachiappan~Valliappan who have made the time
 spent working on the thesis way more enjoyable. Lastly I would like to
-give a special thanks to Valentina Méndez who have been a great moral
+give a special thanks to Valentina~Méndez who have been a great moral
 support throughout the whole process.
diff --git a/doc/assets/logo_eng.pdf b/doc/assets/logo_eng.pdf
new file mode 100644
index 0000000..6292118
Binary files /dev/null and b/doc/assets/logo_eng.pdf differ
diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty
index ba7934a..db46ead 100644
--- a/doc/chalmerstitle.sty
+++ b/doc/chalmerstitle.sty
@@ -80,7 +80,7 @@ Master's thesis in Computer Science
 	
 	\vfill	
 	\centering
-	\includegraphics[width=0.2\pdfpagewidth]{logo_eng.pdf}
+	\includegraphics[width=0.2\pdfpagewidth]{assets/logo_eng.pdf}
   \vspace{5mm}
 	
 	\textsc{Department of Computer Science and Engineering}\\
diff --git a/doc/introduction.tex b/doc/introduction.tex
index 476b62c..b468ddd 100644
--- a/doc/introduction.tex
+++ b/doc/introduction.tex
@@ -75,8 +75,8 @@ some limitations inherent in ITT and -- by extension -- Agda.
 Consider the functions:
 %
 \begin{align*}%
-\var{zeroLeft}  & \defeq \lambda\; (n \tp \bN) \to (0 + n \tp \bN) \\
-\var{zeroRight} & \defeq \lambda\; (n \tp \bN) \to (n + 0 \tp \bN)
+\var{zeroLeft}  & \defeq λ\; (n \tp \bN) \to (0 + n \tp \bN) \\
+\var{zeroRight} & \defeq λ\; (n \tp \bN) \to (n + 0 \tp \bN)
 \end{align*}%
 %
 The term $n + 0$ is \nomenindex{definitionally} equal to $n$, which we
diff --git a/doc/presentation.tex b/doc/presentation.tex
index 85014b6..697b414 100644
--- a/doc/presentation.tex
+++ b/doc/presentation.tex
@@ -4,8 +4,12 @@
 %% \usecolortheme[named=seagull]{structure}
 
 \input{packages.tex}
+
 \input{macros.tex}
-\title[Univalent Categories]{Univalent Categories\\ \footnotesize A formalization of category theory in Cubical Agda}
+
+\title{Univalent Categories}
+\subtitle{A formalization of category theory in Cubical Agda}
+
 \newcommand{\myname}{Frederik Hangh{\o}j Iversen}
 \author[\myname]{
   \myname\\
@@ -74,14 +78,14 @@
   \framesubtitle{Definition}
   Heterogeneous paths
   \begin{equation*}
-    \Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU
+    \Path \tp (P \tp \I → \MCU) → P\ 0 → P\ 1 → \MCU
   \end{equation*}
   \pause
-  For $P \tp I → \MCU$, $A \tp \MCU$ and $a_0, a_1 \tp A$
+  For $P \tp \I → \MCU$, $A \tp \MCU$ and $a_0, a_1 \tp A$
   inhabitants of $\Path\ P\ a_0\ a_1$ are like functions
   %
   $$
-  p \tp ∏_{i \tp I} P\ i
+  p \tp ∏_{i \tp \I} P\ i
   $$
   %
   Which satisfy $p\ 0 & = a_0$ and $p\ 1 & = a_1$
@@ -255,13 +259,13 @@
   \end{align*}
   where
   $$
-  \phi\ f ≜ \identity
-  ( \lll f ≡ f )
+  \phi\ f ≜
+  ( \identity \lll f ≡ f )
   ×
   ( f \lll \identity ≡ f)
   $$
   \pause
-  Let $\approxeq$ denote ismorphism of objects. We can then construct
+  Let $\approxeq$ denote isomorphism of objects.  We can then construct
   the identity isomorphism in any category:
   $$
   \identity , \identity , \var{isIdentity} \tp A \approxeq A
@@ -326,7 +330,7 @@
   Use $\lemPropF$ for the latter.
   \pause
   %
-  Univalence is indexed by an identity proof. So $A ≜
+  Univalence is indexed by an identity proof.  So $A ≜
   IsIdentity\ identity$ and $B ≜ \var{Univalent}$.
   \pause
   %
@@ -379,7 +383,7 @@
   \end{align*}
   \pause
   %
-  Induction will be based at $A$. Let $\widetilde{B}$ and $\widetilde{p}
+  Induction will be based at $A$.  Let $\widetilde{B}$ and $\widetilde{p}
   \tp A ≡ \widetilde{B}$ be given.
   %
   \pause
@@ -582,7 +586,7 @@
   \end{align*}
   \pause
   %
-  Let $\fmap$ be the map on arrows of $\EndoR$. Likewise
+  Let $\fmap$ be the map on arrows of $\EndoR$.  Likewise
   $\pure$ and $\join$ are the maps of the natural transformations
   $\pureNT$ and $\joinNT$ respectively.
   %
@@ -643,7 +647,7 @@
   \join ≜ \bind\ \identity
   $$
   \pause
-  The laws are logically equivalent. So we get:
+  The laws are logically equivalent.  So we get:
   %
   $$
   \var{Monoidal} ≃ \var{Kleisli}
diff --git a/doc/title.tex b/doc/title.tex
index 83b90c0..1afc9b7 100644
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -37,7 +37,7 @@ Master's thesis in Computer Science
 	
 	\vfill	
 	\centering
-	\includegraphics[width=0.2\pdfpagewidth]{logo_eng.pdf}
+	\includegraphics[width=0.2\pdfpagewidth]{assets/logo_eng.pdf}
   \vspace{5mm}
 	
 	\textsc{Department of Computer Science and Engineering}\\