From 3574ebc3235c8abe501beac886e55d5e7cdd2e26 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 10 May 2018 14:26:56 +0200 Subject: [PATCH] Add abstract --- doc/abstract.tex | 21 +++++++++++++++++++++ doc/introduction.tex | 16 ++-------------- doc/macros.tex | 1 + doc/main.tex | 2 +- 4 files changed, 25 insertions(+), 15 deletions(-) create mode 100644 doc/abstract.tex diff --git a/doc/abstract.tex b/doc/abstract.tex new file mode 100644 index 0000000..04e47d7 --- /dev/null +++ b/doc/abstract.tex @@ -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. diff --git a/doc/introduction.tex b/doc/introduction.tex index f6030f3..a3b5567 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -1,22 +1,11 @@ \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} % In the following two sections I present two examples that illustrate some limitations inherent in ITT and -- by extension -- Agda. % \subsection{Functional extensionality} -\label{sec:functional-extensionality} +\label{sec:functional-extensionality}% Consider the functions: % \begin{multicols}{2} @@ -30,11 +19,10 @@ Consider the functions: \end{multicols} % $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 $+$ which is: % -\newcommand{\suc}[1]{\mathit{suc}\ #1} \begin{align*} + & \tp \bN \to \bN \to \bN \\ n + 0 & \defeq n \\ diff --git a/doc/macros.tex b/doc/macros.tex index 16f47ad..1733db4 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -91,3 +91,4 @@ \newcommand\Endo[1]{\varindex{Endo}\ #1} \newcommand\EndoR{\mathcal{R}} \newcommand\funExt{\varindex{funExt}} +\newcommand{\suc}[1]{\mathit{suc}\ #1} diff --git a/doc/main.tex b/doc/main.tex index 9dfde95..4d01c3a 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -48,7 +48,7 @@ \frontmatter \myfrontmatter \maketitle -\addtocontents{toc}{\protect\thispagestyle{empty}} +\input{abstract.tex} \tableofcontents \mainmatter %