cat/doc/conclusion.tex

\chapter{Conclusion}
This thesis highlighted some of 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.

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
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
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.
%%
%% problem with inductive type
%% overcome with cubical
%% the path type
%% homotopy levels
%% depdendent paths
%%
%% category theory
%% algebra of functions ~ funExt
%% identify isomorphic types ~ univalence
%% using categories to prove properties
%% computational properties
%% reusability, compositional