24 lines
1.3 KiB
TeX
24 lines
1.3 KiB
TeX
\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
|
|
developments have, however, resulted in cubical type theory, which
|
|
permits a constructive proof of univalence. The programming language
|
|
Agda has been extended with capabilities for 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
|
|
the application of univalence, two formulations of monads will be
|
|
presented: Namely monads in the monoidal form and monads in the
|
|
Kleisli form. Using univalence, it will be shown 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 suggest how further work can
|
|
help alleviate some of these challenges.
|