Add conclusion

doc/conclusion.tex

@@ -1,42 +1,45 @@
 \chapter{Conclusion}
-This thesis highlighted some of issues with the standard inductive definition of
+This thesis highlighted some issues with the standard inductive definition of
 propositional equality used in Agda. Functional extensionality and univalence
-are two examples not admissible in Intensional Type Theory (ITT). This issue is
-overcome with an extension to Agda's type system called Cubical Agda. With
-Cubical Agda both functional extensionality and univalence are admissible.
-Cubical Agda is more expressive, but there are certain issues that arise that
-are not present in standard Agda. For one thing ITT and standard Agda enjoys
-Uniqueness of Identity Proofs (UIP). This is not the case in Cubical Agda. In
-stead there exists a hierarchy of types with increasing \nomen{homotopical
-  structure}. It turns out to be useful to built the formalization with this in
-mind as it can simplify proofs considerably. Another issue one must overcome in
-Cubical Agda is when a type has a field whose type depends on a previous field.
-In this case paths between such types will be heterogeneous paths which in
-practice turns out to be considerably more difficult to work with than
-homogeneous paths. The thesis also demonstrated how to use appropriate
-abstraction techniques for dealing with this, such as based path-induction.
+are examples of two propositions not admissible in Intensional Type Theory
+(ITT). This has a big impact on what is provable and the reusability of proofs.
+This issue is overcome with an extension to Agda's type system called Cubical
+Agda. With Cubical Agda both functional extensionality and univalence are
+admissible. Cubical Agda is more expressive, but there are certain issues that
+arise that are not present in standard Agda. For one thing ITT and standard Agda
+enjoys Uniqueness of Identity Proofs (UIP). This is not the case in Cubical
+Agda. In stead there exists a hierarchy of types with increasing
+\nomen{homotopical structure}. It turns out to be useful to built the
+formalization with this hierarchy in mind as it can simplify proofs
+considerably. Another issue one must overcome in Cubical Agda is when a type has
+a field whose type depends on a previous field. In this case paths between such
+types will be heterogeneous paths. This problem is related to Cubical Agda not
+having the K-rule \TODO{Not mentioned anywhere in the report}. In practice it
+turns out to be considerably more difficult to work heterogeneous paths than
+with homogeneous paths. The thesis demonstrated some techniques to overcome
+these difficulties, such as based path-induction.
 
 This thesis formalized some of the core concepts from category theory including;
 categories, functors, products, exponentials, Cartesian closed categories,
-natural transformations, the yoneda embedding and monads. Category theory is an
-interesting case-study for the application of Cubical Agda for two reasons in
-particular: Because category theory is the study of abstract algebra of
+natural transformations, the yoneda embedding, monads and more. Category theory
+is an interesting case-study for the application of Cubical Agda for two reasons
+in particular: Because category theory is the study of abstract algebra of
 functions, meaning that functional extensionality is particularly relevant.
-Another reason is that in category theory it is commonplace to identity
-isomorphic structures and univalence allows us to make this notion precise. The
+Another reason is that in category theory it is commonplace to identify
+isomorphic structures and univalence allows for making this notion precise. This
 thesis also demonstrated another technique that is common in category theory;
 namely to define categories to prove properties of other structures.
 Specifically a category was defined to demonstrate that any two product objects
 in a category are isomorphic. Furthermore the thesis showed two formulations of
-monads and proved that they indeed are equivalent: Namely monoidal- and Kleisli-
-monads. The monoidal formulation is more typical to category theoretic
-formulations and the Kleisli formulation will be more familiar to functional
-programmers. In the formulation we also saw how paths can be used to extract
-functions. A path between two types induce an isomorphism between the two types.
-This e.g. permits developers to write a monad instance for a given type using
-the Kleisli formulation. By transporting this formulation to become a monoidal
-monad one can reuse all results about monoidal monads on the Kleisli
-formulation.
+monads and proved that they indeed are equivalent: Namely monads in the
+monoidal- and Kleisli- form. The monoidal formulation is more typical to
+category theoretic formulations and the Kleisli formulation will be more
+familiar to functional programmers. In the formulation we also saw how paths can
+be used to extract functions. A path between two types induce an isomorphism
+between the two types. This e.g. permits developers to write a monad instance
+for a given type using the Kleisli formulation. By transporting along the path
+between the monoidal- and Kleisli- formulation one can reuse all the operations
+and results shown for monoidal- monads in the context of kleisli monads.
 %%
 %% problem with inductive type
 %% overcome with cubical

doc/introduction.tex

@@ -1,9 +1,9 @@
 \chapter{Introduction}
 Functional extensionality and univalence is not expressible in
 \nomen{Intensional Martin Löf Type Theory} (ITT). This poses a severe limitation
-on both i. what is \emph{provable} and ii. the \emph{re-usability} of proofs.
-Recent developments have, however, resulted in \nomen{Cubical Type Theory} (CTT)
-which permits a constructive proof of these two important notions.
+on both what is \emph{provable} and the \emph{re-usability} of proofs. Recent
+developments have, however, resulted in \nomen{Cubical Type Theory} (CTT) which
+permits a constructive proof of these two important notions.
 
 Furthermore an extension has been implemented for the proof assistant Agda
 (\cite{agda}, \cite{cubical-agda}) that allows us to work in such a ``cubical
@@ -22,10 +22,10 @@ Consider the functions:
 \begin{multicols}{2}
   \noindent
   \begin{equation*}
-    f \defeq (n \tp \bN) \mapsto (0 + n \tp \bN)
+    f \defeq (n \tp \bN) \mto (0 + n \tp \bN)
   \end{equation*}
   \begin{equation*}
-    g \defeq (n \tp \bN) \mapsto (n + 0 \tp \bN)
+    g \defeq (n \tp \bN) \mto (n + 0 \tp \bN)
   \end{equation*}
 \end{multicols}
 %
@@ -63,14 +63,14 @@ show that representable functors are indeed functors. The representable functor
 for a category $\bC$ and a fixed object in $A \in \bC$ is defined to be:
 %
 \begin{align*}
-\fmap \defeq X \mapsto \Hom_{\bC}(A, X)
+\fmap \defeq X \mto \Hom_{\bC}(A, X)
 \end{align*}
 %
 The proof obligation that this satisfies the identity law of functors
 ($\fmap\ \idFun \equiv \idFun$) thus becomes:
 %
 \begin{align*}
-\Hom(A, \idFun_{\bX}) = (g \mapsto \idFun \comp g) \equiv \idFun_{\Sets}
+\Hom(A, \idFun_{\bX}) = (g \mto \idFun \comp g) \equiv \idFun_{\Sets}
 \end{align*}
 %
 One needs functional extensionality to ``go under'' the function arrow and apply

doc/macros.tex

@@ -12,7 +12,8 @@
 \newcommand{\bC}{\mathbb{C}}
 \newcommand{\bX}{\mathbb{X}}
 % \newcommand{\to}{\rightarrow}
-\newcommand{\mto}{\mapsto}
+%% \newcommand{\mto}{\mapsto}
+\newcommand{\mto}{\rightarrow}
 \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
 \let\type\UU
 \newcommand{\MCU}{\UU}