Add abstract

This commit is contained in:
Frederik Hanghøj Iversen 2018-05-10 14:26:56 +02:00
parent 3d618c001b
commit 3574ebc323
4 changed files with 25 additions and 15 deletions

21
doc/abstract.tex Normal file
View file

@ -0,0 +1,21 @@
\chapter*{Abstract}
The usual notion of propositional equality in intensional type-theory is
restrictive. For instance it does not admit functional extensionality or
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 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 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. It will emphasize
why it is useful to have a constructive interpretation of univalence. As an
example of this two formulations of monads will be presented: Namely monaeds in
the monoidal form an monads in the Kleisli form.
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 furhter work can help allievate
some of these challenges.

View file

@ -1,22 +1,11 @@
\chapter{Introduction} \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 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
setting''. This thesis will explore the usefulness of this extension in the
context of category theory.
%
\section{Motivating examples} \section{Motivating examples}
% %
In the following two sections I present two examples that illustrate some In the following two sections I present two examples that illustrate some
limitations inherent in ITT and -- by extension -- Agda. limitations inherent in ITT and -- by extension -- Agda.
% %
\subsection{Functional extensionality} \subsection{Functional extensionality}
\label{sec:functional-extensionality} \label{sec:functional-extensionality}%
Consider the functions: Consider the functions:
% %
\begin{multicols}{2} \begin{multicols}{2}
@ -30,11 +19,10 @@ Consider the functions:
\end{multicols} \end{multicols}
% %
$n + 0$ is \nomen{definitionally} equal to $n$, which we write as $n + 0 = n$. $n + 0$ is \nomen{definitionally} equal to $n$, which we write as $n + 0 = n$.
This is also \called \nomen{judgmental} equality. We call it definitional This is also called \nomen{judgmental} equality. We call it definitional
equality because the \emph{equality} arises from the \emph{definition} of $+$ equality because the \emph{equality} arises from the \emph{definition} of $+$
which is: which is:
% %
\newcommand{\suc}[1]{\mathit{suc}\ #1}
\begin{align*} \begin{align*}
+ & \tp \bN \to \bN \to \bN \\ + & \tp \bN \to \bN \to \bN \\
n + 0 & \defeq n \\ n + 0 & \defeq n \\

View file

@ -91,3 +91,4 @@
\newcommand\Endo[1]{\varindex{Endo}\ #1} \newcommand\Endo[1]{\varindex{Endo}\ #1}
\newcommand\EndoR{\mathcal{R}} \newcommand\EndoR{\mathcal{R}}
\newcommand\funExt{\varindex{funExt}} \newcommand\funExt{\varindex{funExt}}
\newcommand{\suc}[1]{\mathit{suc}\ #1}

View file

@ -48,7 +48,7 @@
\frontmatter \frontmatter
\myfrontmatter \myfrontmatter
\maketitle \maketitle
\addtocontents{toc}{\protect\thispagestyle{empty}} \input{abstract.tex}
\tableofcontents \tableofcontents
\mainmatter \mainmatter
% %