64 lines
3.5 KiB
TeX
64 lines
3.5 KiB
TeX
\chapter{Conclusion}
|
|
This thesis highlighted some issues with the standard inductive
|
|
definition of propositional equality used in Agda. Functional
|
|
extensionality and univalence 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 Agda enjoys Uniqueness of Identity Proofs (UIP) though a flag
|
|
exists to turn this off. This feature is not present in Cubical Agda.
|
|
Rather than having unique identity proofs cubical Agda gives rise to a
|
|
hierarchy of types with increasing \nomen{homotopical
|
|
structure}{homotopy levels}. It turns out to be useful to build 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. In
|
|
practice it turns out to be considerably more difficult to work with
|
|
heterogeneous paths than with homogeneous paths. This thesis
|
|
demonstrated the application of some techniques to overcome these
|
|
difficulties, such as based path induction.
|
|
|
|
This thesis formalizes some of the core concepts from category theory
|
|
including: categories, functors, products, exponentials, Cartesian
|
|
closed categories, 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. One reason
|
|
is 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 identify isomorphic structures. 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 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. It would have been very
|
|
difficult to make a similar proof with setoids and the proof would be
|
|
very difficult to read. 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
|
|
%% 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
|