fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Merge branch 'dev'

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-10 14:29:41 +02:00
parent a5571de191 3574ebc323
commit 513d91ae4f
15 changed files with 431 additions and 254 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
README.md
View file

@ -2,11 +2,17 @@ Description
===========
This project aims to formalize some parts of category theory using cubical agda
— an extension to agda permitting univalence. To learn more about this
[readthedocs](https://agda.readthedocs.io/en/latest/language/cubical.html).
[read the docs](https://agda.readthedocs.io/en/latest/language/cubical.html).
This project draws a lot of inspiration from [the
HoTT-book](https://homotopytypetheory.org/book/).
If you want more information about this project, then you're in luck. This is my
masters thesis. Go ahead and read it:
cd doc/
make read
Installation
============
@ -18,7 +24,8 @@ To succesfully compile the following is needed:
* [Agda Standard Library](https://github.com/agda/agda-stdlib)
* [Cubical](https://github.com/Saizan/cubical-demo/)
[^1]: At least version >= [`707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43)
[^1]: At least version >=
[`707ce6042`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43)
The version of the libraries that this depends on can be shown by
executing the following command in the root directory of the project:
@ -31,13 +38,6 @@ versions of these libraries that are compatible with this
project. Since this information is only provided as documentation it
may also noot be up-to-date so beware.
It's important to have the right version of these - but which one is the right
is in constant flux. It's most likely the newest one.
I've used git submodules to manage dependencies. Unfortunately Agda does not
allow specifying libraries to be used only as local dependencies. So the
submodules are mostly used for documentation.
You can let Agda know about these libraries by appending them to your global
libraries file like so: (NB!: There is a good reason this is not in a
makefile. So please verify that you know what you are doing, you probably

3
doc/.gitignore vendored
View file

@ -7,3 +7,6 @@
*.bbl
*.blg
*.toc
*.idx
*.ilg
*.ind

3
doc/Makefile
View file

@ -48,3 +48,6 @@ cleanall:
clean:
latexmk -c
read: all
xdg-open $(PROJNAME).pdf

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.

11
doc/chalmerstitle.sty
View file

@ -40,11 +40,11 @@
\newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}}
%% FRONTMATTER
\newcommand*{\myfrontmatter}{%
\newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm}
%% \newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm}
\begingroup
\thispagestyle{empty}
{\Huge\@title}\\[.5cm]
{\Large A formalization of category theory in Cubical Agda}\\[2.5cm]
{\Large A formalization of category theory in Cubical Agda}\\[6cm]
\begin{center}
\includegraphics[width=\linewidth,keepaspectratio]{isomorphism.png}
\end{center}
@ -66,7 +66,7 @@ Master's thesis in Computer Science
}
\renewcommand*{\maketitle}{%
\begin{titlepage}
%% \begin{titlepage}
% TITLE PAGE
\newpage
@ -131,5 +131,6 @@ Telephone +46 31 772 1000 \setlength{\parskip}{0.5cm}\\
%Printed by [Name of printing company]\\
Gothenburg, Sweden \the\year
\restoregeometry
\end{titlepage}}
%% \restoregeometry
%% \end{titlepage}
}

54
doc/conclusion.tex
View file

@ -1,3 +1,55 @@
\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 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 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. This problem is related to Cubical Agda not
having the K-rule \TODO{Not mentioned anywhere in the report}. In practice it
turns out to be considerably more difficult to work heterogeneous paths than
with homogeneous paths. The thesis demonstrated some techniques to overcome
these difficulties, such as based path-induction.
\TODO{\ldots}
This thesis formalized 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: 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 and 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. 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

154
doc/cubical.tex
View file

@ -1,17 +1,18 @@
\chapter{Cubical Agda}
\section{Propositional equality}
In Agda judgmental equality is a feature of the type-system. It's a property of
types that can be checked by computational means. In the example from the
Judgmental equality in Agda is a feature of the type-system. Its something that
can be checked automatically by the type-checker: In the example from the
introduction $n + 0$ can be judged to be equal to $n$ simply by expanding the
definition of $+$.
Propositional equality on the other hand is defined within the language itself.
Cubical Agda extends the underlying type system (\TODO{Cite someone smarter than
me with a good resource on this}) but introduces a data-type within the
languages.
On the other hand, propositional equality is something defined within the
language itself. Propositional equality cannot be derived automatically. The
normal definition of judgmental equality is an inductive data-type. Cubical Agda
discards this type in favor of a new primitives that has certain computational
properties exclusive to it.
Exceprts of the source code relevant to this section can be found in appendix
\ref{sec:app-cubical}.
\S\ref{sec:app-cubical}.
\subsection{The equality type}
The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
@ -21,7 +22,8 @@ two points of $A$; $a_0, a_1 \tp A$ we can form the type:
a_0 \equiv a_1 \tp \MCU
\end{align}
%
In Agda this is defined as an inductive data-type with the single constructor:
In Agda this is defined as an inductive data-type with the single constructor
for any $a \tp A$:
%
\begin{align}
\refl \tp a \equiv a
@ -29,7 +31,7 @@ In Agda this is defined as an inductive data-type with the single constructor:
%
For any $a \tp A$.
There also exist a related notion of \emph{heterogeneous} equality where allows
There also exist a related notion of \emph{heterogeneous} equality which allows
for equating points of different types. In this case given two types $A, B \tp
\MCU$ and two points $a \tp A$, $b \tp B$ we can construct the type:
%
@ -37,7 +39,8 @@ for equating points of different types. In this case given two types $A, B \tp
a \cong b \tp \MCU
\end{align}
%
This is likewise defined as an inductive data-type with a single constructors:
This is likewise defined as an inductive data-type with a single constructors
for any $a \tp A$:
%
\begin{align}
\refl \tp a \cong a
@ -47,11 +50,11 @@ In Cubical Agda these two notions are paralleled with homogeneous- and
heterogeneous paths respectively.
%
\subsection{The path type}
In Cubical Agda judgmental equality is encapsulated with the type:
Judgmental equality in Cubical Agda is encapsulated with the type:
%
$$
\begin{equation}
\Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU
$$
\end{equation}
%
$I$ is a special data-type (\TODO{that also has special computational properties
AFAIK}) called the index set. $I$ can be thought of simply as the interval on
@ -62,11 +65,11 @@ left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called
$\Path$ because it is connected with paths in homotopy theory. The intuition
behind this is that $\Path$ describes paths in $\MCU$ -- i.e. between types. For
a path $p$ for the point $p\ i$ the index $i$ describes how far along the path
one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-)
function, $p$, from the index-space to the path-space:
one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-) function,
$p$, from the index-space to the path-space:
%
$$
p \tp I \to P\ i
p \tp \prod_{i \tp I} P\ i
$$
%
Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the
@ -77,16 +80,16 @@ endpoints. I.e.:
p\ 1 & = a_1
\end{align*}
%
The notion of ``homogeneous equalities'' can be recovered by not letting the
path-space $P$ depend on it's argument:
The notion of ``homogeneous equalities'' is recovered when $P$ does not depend
on its argument:
%
$$
a_0 \equiv a_1 \defeq \Path\ (\lambda i \to A)\ a_0\ a_1
$$
%
For $A \tp \MCU$, $a_0, a_1 \tp A$. I will generally prefer to use the notation
$a_0 \equiv a_1$ when talking about non-dependent paths and use the notation
$\Path\ (\lambda i \to A)\ a_0\ a_1$ when the path-space is of particular
$a \equiv b$ when talking about non-dependent paths and use the notation
$\Path\ (\lambda i \to P\ i)\ a\ b$ when the path-space is of particular
interest.
With this definition we can also recover reflexivity. That is, for any $A \tp
@ -99,28 +102,63 @@ With this definition we can also recover reflexivity. That is, for any $A \tp
\end{aligned}
\end{equation}
%
Or, in other terms; reflexivity is the path in $A$ that is $a$ at the left
endpoint as well as at the right endpoint. It is inhabited by the path which
stays constantly at $a$ at any index $i$.
Here the path-space is $P \defeq \lambda i \to A$ and it satsifies $P\ i = A$
definitionally. So to inhabit it, is to give a path $I \to A$ which is
judgmentally $a$ at either endpoint. This is satisfied by the constant path;
i.e. the path that stays at $a$ at any index $i$.
Paths have some other important properties, but they are not the focus of this
thesis. \TODO{Refer the reader somewhere for more info.}
It is also surpisingly easy to show functional extensionality with which we can
construct a path between $f$ and $g$ -- the function defined in the introduction
(section \S\ref{sec:functional-extensionality}).
%% module _ {ℓa ℓb} {A : Set ℓa} {B : A → Set ℓb} where
%% funExt : {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) → f ≡ g
Functional extensionality is the proposition, given a type $A \tp \MCU$, a
family of types $B \tp A \to \MCU$ and functions $f, g \tp \prod_{a \tp A}
B\ a$:
%
\begin{equation}
\label{eq:funExt}
\funExt \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g
\end{equation}
%
%% p = λ i a → p a i
So given $p \tp \prod_{a \tp A} f\ a \equiv g\ a$ we must give a path $f \equiv
g$. That is a function $I \to \prod_{a \tp A} B\ a$. So let $i \tp I$ be given.
We must now give an expression $\phi \tp \prod_{a \tp A} B\ a$ satisfying
$\phi\ 0 \equiv f\ a$ and $\phi\ 1 \equiv g\ a$. This neccesitates that the
expression must be a lambda-abstraction, so let $a \tp A$ be given. Now we can
apply $a$ to $p$ and get the path $p\ a \tp f\ a \equiv g\ a$. And this exactly
satisfied the conditions for $\phi$. In conclustion \ref{eq:funExt} is inhabited
by the term:
%
\begin{equation}
\label{eq:funExt}
\funExt\ p \defeq λ i\ a → p\ a\ i
\end{equation}
%
With this we can now prove the desired equality $f \equiv g$ from section
\S\ref{sec:functional-extensionality}:
%
\begin{align*}
p & \tp f \equiv g \\
p & \defeq \funExt\ \lambda n \to \refl
\end{align*}
%
Paths have some other important properties, but they are not the focus of
this thesis. \TODO{Refer the reader somewhere for more info.}
\section{Homotopy levels}
In ITT all equality proofs are identical (in a closed context). This means that,
in some sense, any two inhabitants of $a \equiv b$ are ``equally good'' -- they
don't have any interesting structure. This is referred to as uniqueness of
identity proofs. Unfortunately this is orthogonal to univalence that only makes
sense in the absence of UIP.
In homotopy type theory we have a hierarchy of types based on their ``internal
structure''. At the bottom of this hierarchy we have the set of contractible
types:
do not have any interesting structure. This is referred to as Uniqueness of
Identity Proofs (UIP). Unfortunately it is not possible to have a type-theory
with both univalence and UIP. In stead we have a hierarchy of types with an
increasing amount of homotopic structure. At the bottom of this hierarchy we
have the set of contractible types:
%
\begin{equation}
\begin{aligned}
%% \begin{split}
& \isContr && \tp \MCU \to \MCU \\
& \isContr && \tp \MCU \to \MCU \\
& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
%% \end{split}
\end{aligned}
@ -128,8 +166,14 @@ types:
%
The first component of $\isContr\ A$ is called ``the center of contraction''.
Under the propositions-as-types interpretation of type-theory $\isContr\ A$ can
be thought of as ``the true proposition $A$''. It is a theorem that if a type is
contractible, then it is isomorphic to the unit-type $\top$.
be thought of as ``the true proposition $A$''. And indeed $\top$ is
contractible:
\begin{equation*}
\var{tt} , \lambda x \to \refl \tp \isContr\ \top
\end{equation*}
%
It is a theorem that if a type is contractible, then it is isomorphic to the
unit-type.
The next step in the hierarchy is the set of mere propositions:
%
@ -140,10 +184,18 @@ The next step in the hierarchy is the set of mere propositions:
\end{aligned}
\end{equation}
%
$\isProp\ A$ can be thought of as the set of true and false propositions. It is
a result that if a mere proposition $A$ is inhabited, then so is it
contractible. If it is not inhabited it is equivalent to the empty-type (or
false proposition).\TODO{Cite!!}
$\isProp\ A$ can be thought of as the set of true and false propositions. And
indeed both $\top$ and $\bot$ are propositions:
%
\begin{align*}
λ \var{tt}\ \var{tt} → refl & \tp \isProp\ ⊤ \\
λ\varnothing\ \varnothing & \tp \isProp\ ⊥
\end{align*}
%
$\varnothing$ is used here to denote an impossible pattern. It is a theorem that
if a mere proposition $A$ is inhabited, then so is it contractible. If it is not
inhabited it is equivalent to the empty-type (or false
proposition).\TODO{Cite!!}
I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to
stress that we have $\isProp\ A$.
@ -157,12 +209,15 @@ Then comes the set of homotopical sets:
\end{aligned}
\end{equation}
%
At this point it should be noted that the term ``set'' is somewhat conflated;
there is the notion of sets from set-theory, in Agda types are denoted
\texttt{Set}. I will use it consistently to refer to a type $A$ as a set exactly
if $\isSet\ A$ is inhabited.
I will not give an example of a set at this point. It turns out that proving
e.g. $\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}).
There will be examples of sets later in this report. At this point it should be
noted that the term ``set'' is somewhat conflated; there is the notion of sets
from set-theory, in Agda types are denoted \texttt{Set}. I will use it
consistently to refer to a type $A$ as a set exactly if $\isSet\ A$ is a
proposition.
The next step in the hierarchy is, as the reader might've guessed, the type:
As the reader may have guessed the next step in the hierarchy is the type:
%
\begin{equation}
\begin{aligned}
@ -219,10 +274,13 @@ $$
%
We have the function:
%
$$
\begin{equation}
\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
$$
\end{equation}
%
I will not give an example of using $\pathJ$ here. An application can be found
later in \ref{eq:pathJ-example}.
\subsection{Paths over propositions}
\label{sec:lemPropF}
Another very useful combinator is $\lemPropF$:
@ -277,8 +335,8 @@ $$
\subsection{Pairs over propositions}
\label{sec:propSig}
%
$\sum$-types preserve propositionality whenever it's first component is a
proposition, and it's second component is a proposition for all points of in the
$\sum$-types preserve propositionality whenever its first component is a
proposition, and its second component is a proposition for all points of in the
left type.
%
$$

8
doc/discussion.tex
View file

@ -7,9 +7,9 @@ to very complicated goals. One technique for alleviating this was to prove that
certain types are mere propositions.
\subsection{Computational properties}
Another aspect (\TODO{That I actually didn't highlight very well in the previous
chapter}) is the computational nature of paths. Say we have formalized this
common result about monads:
Another aspect (\TODO{That I actually did not highlight very well in the
previous chapter}) is the computational nature of paths. Say we have
formalized this common result about monads:
\TODO{Some equation\ldots}
@ -26,7 +26,7 @@ disparate areas: The category-theoretic study of monads; and monads as in
functional programming. Univalence thus allows one to reuse proofs. You could
say that univalence gives the developer two proofs for the price of one.
The introduction (section \ref{sec:context}) mentioned an often
The introduction (section \S\ref{sec:context}) mentioned an often
employed-technique for enabling extensional equalities is to use the
setoid-interpretation. Nowhere in this formalization has this been necessary,
$\Path$ has been used globally in the project as propositional equality. One

234
doc/implementation.tex
View file

@ -53,9 +53,15 @@ given type.
For the rest of this chapter I will present some of these results. For didactic
reasons no source-code has been included in this chapter. To see the formal
definitions excerpts of the implementation have been included in appendix
\ref{ch:app-sources}.
\S\ref{ch:app-sources}:
Appendix
\S\ref{sec:app-categories} corresponds to section \S\ref{sec:categories},
appendix \S\ref{sec:app-products} to section \S\ref{sec:products}
and appendix \S\ref{sec:app-monads} to section \S\ref{sec:monads}.
\section{Categories}
\label{sec:categories}
The data for a category consist of a type for the sort of objects; a type for
the sort of arrows; an identity arrow and a composition operation for arrows.
Another record encapsulates some laws about this data: associativity of
@ -64,7 +70,7 @@ constituents of a category and can be found in typical mathematical expositions
on the topic. We, however, impose one further requirement on what it means to be
a category, namely that the type of arrows form a set.
Such categories are called \nomen{1-categories}. It's possible to relax this
Such categories are called \nomen{1-categories}. It is possible to relax this
requirement. This would lead to the notion of higher categories (\cite[p.
307]{hott-2013}). For the purpose of this project, however, this report will
restrict itself to 1-categories. Making based on higher categories would be a
@ -82,15 +88,15 @@ definitions: If we let $p$ be a witness to the identity law, which formally is:
\id \comp f \equiv f \x f \comp \id \equiv f
\end{equation}
%
Then we can construct the identity isomorphism $\var{idIso} \tp \identity,
Then we can construct the identity isomorphism $\idIso \tp \identity,
\identity, p \tp A \approxeq A$ for any object $A$. Here $\approxeq$ denotes
isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will
be elaborated further on in sections \ref{sec:equiv} and \ref{sec:univalence}.
Moreover, due to substitution for paths we can construct an isomorphism from
\emph{any} path:
be elaborated further on in sections \S\ref{sec:equiv} and
\S\ref{sec:univalence}. Moreover, due to substitution for paths we can construct
an isomorphism from \emph{any} path:
%
\begin{equation}
\var{idToIso} \tp A ≡ B → A ≊ B
\idToIso \tp A ≡ B → A ≊ B
\end{equation}
%
The univalence criterion for categories states that this map must be an
@ -106,14 +112,14 @@ Note that \ref{eq:cat-univ} is \emph{not} the same as:
%
\begin{equation}
\label{eq:cat-univalence}
\tag{Univalence, category}
%% \tag{Univalence, category}
(A \equiv B) \simeq (A \approxeq B)
\end{equation}
%
However the two are logically equivalent: One can construct the latter from the
former simply by ``forgetting'' that $\idToIso$ plays the role of the
equivalence. The other direction is more involved and will be discussed in
section \ref{sec:univalence}.
section \S\ref{sec:univalence}.
In summary, the definition of a category is the following collection of data:
%
@ -127,14 +133,14 @@ In summary, the definition of a category is the following collection of data:
And laws:
%
\begin{align}
\tag{associativity}
%% \tag{associativity}
h \lll (g \lll f) ≡ (h \lll g) \lll f \\
\tag{identity}
%% \tag{identity}
\identity \lll f ≡ f \x
f \lll \identity ≡ f
\\
\label{eq:arrows-are-sets}
\tag{arrows are sets}
%% \tag{arrows are sets}
\isSet\ (\Arrow\ A\ B)\\
\tag{\ref{eq:cat-univ}}
\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso
@ -159,12 +165,12 @@ Proving that \ref{eq:identity} is a mere proposition:
%
There are multiple ways to prove this. Perhaps one of the more intuitive proofs
is by way of the `combinators' $\propPi$ and $\propSig$ presented in sections
\ref{sec:propPi} and \ref{sec:propSig}:
\S\ref{sec:propPi} and \S\ref{sec:propSig}:
%
\begin{align*}
\var{propPi} & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
\propPi & \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
\\
\var{propSig} & \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
\propSig & \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
\end{align*}
%
So the proof goes like this: We `eliminate' the 3 function abstractions by
@ -180,11 +186,11 @@ us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp
set.
This example illustrates nicely how we can use these combinators to reason about
`canonical' types like $\sum$ and $\prod$. Similar combinators can be defined
at the other homotopic levels. These combinators are however not applicable in
situations where we want to reason about other types - e.g. types we've defined
ourselves. For instance, after we've proven that all the projections of
pre-categories are propositions, then we would like to bundle this up to show
`canonical' types like $\sum$ and $\prod$. Similar combinators can be defined at
the other homotopic levels. These combinators are however not applicable in
situations where we want to reason about other types - e.g. types we have
defined ourselves. For instance, after we have proven that all the projections
of pre-categories are propositions, then we would like to bundle this up to show
that the type of pre-categories is also a proposition. Formally:
%
\begin{equation}
@ -196,14 +202,13 @@ Where The definition of $\IsPreCategory$ is the triple:
%
\begin{align*}
\var{isAssociative} & \tp \var{IsAssociative}\\
\var{isIdentity} & \tp \var{IsIdentity}\\
\isIdentity & \tp \var{IsIdentity}\\
\var{arrowsAreSets} & \tp \var{ArrowsAreSets}
\end{align*}
%
Each corresponding to the first three laws for categories. Note that since
$\IsPreCategory$ is not formulated with a chain of sigma-types we wont have any
combinators available to help us here. In stead we'll have to use the path-type
directly.
combinators available to help us here. In stead the paths must be used directly.
\ref{eq:propIsPreCategory} is judgmentally the same as
%
@ -239,21 +244,21 @@ $i$ becomes the triple:
\begin{aligned}
& \var{propIsAssociative} && a.\var{isAssociative}\
&& b.\var{isAssociative} && i \\
& \var{propIsIdentity} && a.\var{isIdentity}\
&& b.\var{isIdentity} && i \\
& \propIsIdentity && a.\isIdentity\
&& b.\isIdentity && i \\
& \var{propArrowsAreSets} && a.\var{arrowsAreSets}\
&& b.\var{arrowsAreSets} && i
\end{aligned}
\end{equation}
%
I've found this to be a general pattern when proving things in homotopy type
I have found this to be a general pattern when proving things in homotopy type
theory, namely that you have to wrap and unwrap equalities at different levels.
It is worth noting that proving this theorem with the regular inductive equality
type would already not be possible, since we at least need extensionality (the
projections are all $\prod$-types). Assuming we had functional extensionality
available to us as an axiom, we would use functional extensionality (in
reverse?) to retrieve the equalities in $a$ and $b$, pattern-match on them to
see that they are both $\var{refl}$ and then close the proof with $\var{refl}$.
see that they are both $\refl$ and then close the proof with $\refl$.
Of course this theorem is not so interesting in the setting of ITT since we know
a priori that equality proofs are unique.
@ -279,16 +284,16 @@ we have shown, $\IsPreCategory$ is a proposition. However, even though
$\Univalent$ is also a proposition, we cannot use this directly to show the
latter. This is because $\isProp$ talks about non-dependent paths. So we need to
'promote' the result that univalence is a proposition to a heterogeneous path.
To this end we can use $\lemPropF$, which was introduced in \ref{sec:lemPropF}.
To this end we can use $\lemPropF$, which was introduced in \S\ref{sec:lemPropF}.
In this case $A = \var{IsIdentity}\ \identity$ and $B = \var{Univalent}$. We've
In this case $A = \var{IsIdentity}\ \identity$ and $B = \Univalent$. We have
shown that being a category is a proposition, a result that holds for any choice
of identity proof. Finally we must provide a proof that the identity proofs at
$a$ and $b$ are indeed the same, this we can extract from $p$ by applying
congruence of paths:
%
$$
\congruence\ \var{isIdentity}\ p
\congruence\ \isIdentity\ p
$$
%
And this finishes the proof that being-a-category is a mere proposition
@ -361,7 +366,7 @@ $$
\fiber\ f\ b \defeq \sum_{a \tp A} \left( b \equiv f\ a \right)
$$
%
I give it's definition here mainly for completeness, because as I stated we can
I give its definition here mainly for completeness, because as I stated we can
move away from this specific instantiation and think about it more abstractly
once we have shown that this definition actually works as an equivalence.
@ -414,7 +419,7 @@ $$
$$
%
That is, we must demonstrate that there is an isomorphism (on types) between
equalities and isomorphisms (on arrows). It's worthwhile to dwell on this for a
equalities and isomorphisms (on arrows). It is worthwhile to dwell on this for a
few seconds. This type looks very similar to univalence for types and is
therefore perhaps a bit more intuitive to grasp the implications of. Of course
univalence for types (which is a proposition -- i.e. provable) does not imply
@ -441,8 +446,8 @@ an isomorphism $A \approxeq B$ in some category $\bC$ be given. Name the
isomorphism $\iota \tp A \to B$ and its inverse $\inv{\iota} \tp B \to A$.
Since $\bC$ is a category (and therefore univalent) the isomorphism induces a
path $p \tp A \equiv B$. From this equality we can get two further paths:
$p_{\var{dom}} \tp \var{Arrow}\ A\ X \equiv \var{Arrow}\ B\ X$ and
$p_{\var{cod}} \tp \var{Arrow}\ X\ A \equiv \var{Arrow}\ X\ B$. We
$p_{\var{dom}} \tp \Arrow\ A\ X \equiv \Arrow\ B\ X$ and
$p_{\var{cod}} \tp \Arrow\ X\ A \equiv \Arrow\ X\ B$. We
then have the following two theorems:
%
\begin{align}
@ -459,58 +464,68 @@ I will give the proof of the first theorem here, the second one is analogous.
%
\begin{align*}
\var{coe}\ p_{\var{dom}}\ f
& \equiv f \lll \inv{(\var{idToIso}\ p)} && \text{lemma} \\
& \equiv f \lll \inv{(\idToIso\ p)} && \text{lemma} \\
& \equiv f \lll \inv{\iota}
&& \text{$\var{idToIso}$ and $\var{isoToId}$ are inverses}\\
&& \text{$\idToIso$ and $\isoToId$ are inverses}\\
\end{align*}
%
In the second step we use the fact that $p$ is constructed from the isomorphism
$\iota$ -- $\inv{(\var{idToIso}\ p)}$ denotes the map $B \to A$ induced by the
isomorphism $\var{idToIso}\ p \tp A \cong B$. The helper-lemma is similar to
what we're trying to prove but talks about paths rather than isomorphisms:
$\iota$ -- $\inv{(\idToIso\ p)}$ denotes the map $B \to A$ induced by the
isomorphism $\idToIso\ p \tp A \cong B$. The helper-lemma is similar to
what we are trying to prove but talks about paths rather than isomorphisms:
%
\begin{equation}
\label{eq:coeDomIso}
\prod_{f \tp \var{Arrow}\ A\ B} \prod_{p \tp A \equiv B}
\var{coe}\ p_{\var{dom}}\ f \equiv f \lll \inv{(\var{idToIso}\ p)}
\prod_{f \tp \Arrow\ A\ B} \prod_{p \tp A \equiv B}
\var{coe}\ p_{\var{dom}}\ f \equiv f \lll \inv{(\idToIso\ p)}
\end{equation}
%
Again $p_{\var{dom}}$ denotes the path $\var{Arrow}\ A\ X \equiv
\var{Arrow}\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$
be given and then invoke based-path-induction. The induction will be based at $A
\tp \var{Object}$, so let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp
A \equiv \widetilde{B}$ be given. The family that we perform induction over will
Again $p_{\var{dom}}$ denotes the path $\Arrow\ A\ X \equiv
\Arrow\ B\ X$ induced by $p$. To prove this statement I let $f$ and $p$ be
given and then invoke based-path-induction. The induction will be based at $A
\tp \Object$ Let $\widetilde{B} \tp \Object$ and $\widetilde{p} \tp A
\equiv \widetilde{B}$ be given. The family that we perform induction over will
be:
%
$$
\var{coe}\ {\widetilde{p}}^*\ f
\begin{align}
D\ \widetilde{B}\ \widetilde{p} \defeq
%% \prod_{\widetilde{B} \tp \Object}
%% \prod_{\widetilde{p} \tp A \equiv \widetilde{B}}
\var{coe}\ {\widetilde{p}}^*\ f
\equiv
f \lll \inv{(\var{idToIso}\ \widetilde{p})}
$$
The base-case therefore becomes:
f \lll \inv{(\idToIso\ \widetilde{p})}
\end{align}
The base-case therefore becomes
$d \tp \var{coe}\ \refl^*\ f \equiv f \lll \inv{(\idToIso\ \refl)}$
and is inhabited by:
\begin{align*}
\var{coe}\ {\widetilde{\refl}}^*\ f
& \equiv f \\
& \equiv f \lll \var{identity} \\
& \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})}
\var{coe}\ \refl^*\ f
& \equiv f
&& \text{$\refl$ is a neutral element for $\var{coe}$}\\
& \equiv f \lll \identity \\
& \equiv f \lll \var{subst}\ \refl\ \identity
&& \text{$\refl$ is a neutral element for $\var{subst}$}\\
& \equiv f \lll \inv{(\idToIso\ \refl)}
&& \text{By definition of $\idToIso$}\\
\end{align*}
%
The first step follows because reflexivity is a neutral element for coercion.
The second step is the identity law in the category. The last step has to do
with the fact that $\var{idToIso}$ is constructed by substituting according to
the supplied path and since reflexivity is also the neutral element for
substitutions we arrive at the desired expression. To close the
based-path-induction we must supply the value ``at the other''. In this case
this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have.
To close the based-path-induction we must supply the value ``at the other''. In
this case this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have.
In summary the proof of \ref{eq:coeDomIso} is the term:
%
\begin{equation}
\label{eq:pathJ-example}
\pathJ\ D\ d\ B\ p
\end{equation}
%
And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}.
%
\section{Categories}
\subsection{Opposite category}
\label{op-cat}
The first category I'll present is a pure construction on categories. Given some
category we can construct it's dual, called the opposite category. Starting with
a simple example allows us to focus on how we work with equivalences and
The first category I will present is a pure construction on categories. Given
some category we can construct its dual, called the opposite category. Starting
with a simple example allows us to focus on how we work with equivalences and
univalence in a very simple category where the structure of the category is
rather simple.
@ -521,7 +536,7 @@ an arrow from $B$ to $A$ in the underlying category. The identity arrow is the
same as the one in the underlying category (they have the same type). Function
composition will be reverse function composition from the underlying category.
I'll refer to things in terms of the underlying category, unless they have an
I will refer to things in terms of the underlying category, unless they have an
over-bar. So e.g. $\idToIso$ is a function in the underlying category and the
corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite
category.
@ -536,7 +551,7 @@ Since $\rrr$ is reverse function composition this is just the symmetric version
of associativity.
%
$$
\var{identity} \rrr f \equiv f \x f \rrr identity \equiv f
\identity \rrr f \equiv f \x f \rrr identity \equiv f
$$
%
This is just the swapped version of identity.
@ -546,38 +561,38 @@ arguments. Or in other words; since $\Arrow\ A\ B$ is a set for all $A\;B \tp
\Object$ then so is $Arrow\ B\ A$.
Now, to show that this category is univalent is not as straight-forward. Luckily
section \ref{sec:equiv} gave us some tools to work with equivalences. We saw
section \S\ref{sec:equiv} gave us some tools to work with equivalences. We saw
that we can prove this category univalent by giving an inverse to
$\wideoverbar{\idToIso} \tp (A \equiv B) \to (A \wideoverbar{\approxeq} B)$.
From the original category we have that $\idToIso \tp (A \equiv B) \to (A \cong
B)$ is an isomorphism. Let us denote it's inverse with $\isoToId \tp (A
B)$ is an isomorphism. Let us denote its inverse with $\isoToId \tp (A
\approxeq B) \to (A \equiv B)$. If we squint we can see what we need is a way to
go between $\wideoverbar{\approxeq}$ and $\approxeq$.
An inhabitant of $A \approxeq B$ is simply an arrow $f \tp \var{Arrow}\ A\ B$
and it's inverse $g \tp \var{Arrow}\ B\ A$. In the opposite category $g$ will
An inhabitant of $A \approxeq B$ is simply an arrow $f \tp \Arrow\ A\ B$
and its inverse $g \tp \Arrow\ B\ A$. In the opposite category $g$ will
play the role of the isomorphism and $f$ will be the inverse. Similarly we can
go in the opposite direction. I name these maps $\var{shuffle} \tp (A \approxeq
B) \to (A \wideoverbar{\approxeq} B)$ and $\var{shuffle}^{-1} \tp (A
go in the opposite direction. I name these maps $\shuffle \tp (A \approxeq
B) \to (A \wideoverbar{\approxeq} B)$ and $\shuffle^{-1} \tp (A
\wideoverbar{\approxeq} B) \to (A \approxeq B)$ respectively.
As the inverse of $\wideoverbar{\idToIso}$ I will pick $\wideoverbar{\isoToId}
\defeq \isoToId \comp \var{shuffle}$. The proof that they are inverses go as
\defeq \isoToId \comp \shuffle$. The proof that they are inverses go as
follows:
%
\begin{align*}
\wideoverbar{\isoToId} \comp \wideoverbar{\idToIso} & =
\isoToId \comp \var{shuffle} \comp \wideoverbar{\idToIso}
\isoToId \comp \shuffle \comp \wideoverbar{\idToIso}
\\
%% ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩ \\
%
& \equiv
\isoToId \comp \var{shuffle} \comp \inv{\var{shuffle}} \comp \idToIso
\isoToId \comp \shuffle \comp \inv{\shuffle} \comp \idToIso
&& \text{lemma} \\
%% ≡⟨⟩ \\
& \equiv
\isoToId \comp \idToIso
&& \text{$\var{shuffle}$ is an isomorphism} \\
&& \text{$\shuffle$ is an isomorphism} \\
& \equiv
\identity
&& \text{$\isoToId$ is an isomorphism}
@ -586,7 +601,7 @@ follows:
The other direction is analogous.
The lemma used in step 2 of this proof states that $\wideoverbar{idToIso} \equiv
\inv{\var{shuffle}} \comp \idToIso$. This is a rather straight-forward proof
\inv{\shuffle} \comp \idToIso$. This is a rather straight-forward proof
since being-an-inverse-of is a proposition, so it suffices to show that their
first components are equal, but this holds judgmentally.
@ -594,12 +609,12 @@ This finished the proof that the opposite category is in fact a category. Now,
to prove that that opposite-of is an involution we must show:
%
$$
\prod_{\bC \tp \var{Category}} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC
\prod_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC
$$
%
As we've seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite
involved.\footnote{We haven't even seen the full story because we've used this
`interface' for equivalences.} Luckily since being-a-category is a mere
As we have seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite
involved.\footnote{We have not even seen the full story because we have used
this `interface' for equivalences.} Luckily since being-a-category is a mere
proposition, we need not concern ourselves with this bit when proving the above.
We can use the equality principle for categories that let us prove an equality
just by giving an equality on the data-part. So, given a category $\bC$ all we
@ -635,7 +650,7 @@ $$
(\var{hA} \equiv \var{hB}) \simeq (\var{hA} \approxeq \var{hB})
$$
%
Which, as we saw in section \ref{sec:univalence}, is sufficient to show that the
Which, as we saw in section \S\ref{sec:univalence}, is sufficient to show that the
category is univalent. The way that I have shown this is with a three-step
process. For objects $(A, s_A)\; (B, s_B) \tp \Set$ I show the following chain
of equivalences:
@ -669,11 +684,11 @@ lemma:
Which says that if two type-families are equivalent at all points, then pairs
with identical first components and these families as second components will
also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq
\var{Isomorphism}$. So we must finally prove:
\Isomorphism$. So we must finally prove:
%
\begin{align}
\label{eq:equivIso}
\prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \var{Isomorphism}\ f \right)
\prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \Isomorphism\ f \right)
\end{align}
First, lets prove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because
@ -716,12 +731,12 @@ choose:
%
\begin{align*}
\var{toIso}
& \tp \isEquiv\ f \to \var{Isomorphism}\ f \\
& \tp \isEquiv\ f \to \Isomorphism\ f \\
\var{fromIso}
& \tp \var{Isomorphism}\ f \to \isEquiv\ f
& \tp \Isomorphism\ f \to \isEquiv\ f
\end{align*}
%
As mentioned in section \ref{sec:equiv}. These maps are not in general inverses
As mentioned in section \S\ref{sec:equiv}. These maps are not in general inverses
of each other. In stead, we will use the fact that $A$ and $B$ are sets. The first thing we must prove is:
%
\begin{align*}
@ -732,11 +747,11 @@ For this we can use the fact that being-an-equivalence is a mere proposition.
For the other direction:
%
\begin{align*}
\var{toIso} \comp \var{fromIso} \equiv \identity_{\var{Isomorphism}\ f}
\var{toIso} \comp \var{fromIso} \equiv \identity_{\Isomorphism\ f}
\end{align*}
%
We will show that $\var{Isomorphism}\ f$ is also a mere proposition. To this
end, let $X\;Y \tp \var{Isomorphism}\ f$ be given. Name the maps $x\;y \tp B
We will show that $\Isomorphism\ f$ is also a mere proposition. To this
end, let $X\;Y \tp \Isomorphism\ f$ be given. Name the maps $x\;y \tp B
\to A$ respectively. Now, the proof that $X$ and $Y$ are the same is a pair of
paths: $p \tp x \equiv y$ and $\Path\ (\lambda\; i \to
\var{AreInverses}\ f\ (p\ i))\ \mathcal{X}\ \mathcal{Y}$ where $\mathcal{X}$
@ -777,8 +792,10 @@ where we have a witness to this being a category. This is useful if this library
is later extended to talk about higher categories.
\section{Products}
In the following I'll demonstrate a technique for using categories to prove
properties. The goal in this section is to show that products are propositions:
\label{sec:products}
In the following a technique for using categories to prove properties will be
demonstrated. The goal in this section is to show that products are
propositions:
%
$$
\prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B)
@ -789,7 +806,7 @@ and $B$ in the category $\bC$. I do this by constructing a category whose
terminal objects are equivalent to products in $\bC$, and since terminal objects
are propositional in a proper category and equivalences preserve homotopy level,
then we know that products also are propositions. But before we get to that,
let's recall the definition of products.
we recall the definition of products.
\subsection{Definition of products}
Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the
@ -815,7 +832,7 @@ $\pi$ is called the product (arrow) of $f$ and $g$.
\newcommand\pairB{\mathcal{B}}
Given a base category $\bC$ and two objects in this category $\pairA$ and
$\pairB$ we can construct the ``pair category'': \TODO{This is a working title,
it's nice to have a name for this thing to refer back to}
it is nice to have a name for this thing to refer back to}
The type of objects in this category will be an object in the underlying
category, $X$, and two arrows (also from the underlying category)
@ -991,7 +1008,7 @@ isomorphism, and create a path from this:
\end{split}
\end{align}
%
Where $\widetilde{p} \defeq \var{isoToId}\ \var{iso} \tp X \equiv Y$.
Where $\widetilde{p} \defeq \isoToId\ \var{iso} \tp X \equiv Y$.
Finally we have the type:
%
@ -1063,8 +1080,8 @@ equality principle for arrows in this category (\ref{eq:productEqPrinc}) gives
us that it suffices to show that $f$ and $\inv{f}$, this is exactly
$\var{inv}_f$.
This concludes the first direction of the isomorphism that we're constructing.
For the other direction we're given just given the isomorphism
This concludes the first direction of the isomorphism that we are constructing.
For the other direction we are given the isomorphism:
%
$$
(f, \inv{f}, \var{inv}_f)
@ -1134,7 +1151,7 @@ gory details.
%
\subsection{Propositionality of products}
%
Now that we've constructed the ``pair category'' I'll demonstrate how to use
Now that we have constructed the ``pair category'' I will demonstrate how to use
this to prove that products are propositional. I will do this by showing that
terminal objects in this category are equivalent to products:
%
@ -1145,7 +1162,7 @@ terminal objects in this category are equivalent to products:
And as always we do this by constructing an isomorphism:
%
In the direction $\var{Terminal} → \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$
we're given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and
we are given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and
$x_𝒜, x_ℬ$ will be the product arrows, so it just remains to verify that this is
indeed a product. That is, for an object $Y$ and two arrows $y_𝒜 \tp
\Arrow\ Y\ 𝒜$, $y_ℬ\ \Arrow\ Y\ ℬ$ we must find a unique arrow $f \tp
@ -1214,6 +1231,7 @@ That in any category:
\end{align}
%
\section{Monads}
\label{sec:monads}
In this section I present two formulations of monads. The two representations
are referred to as the monoidal- and Kleisli- representation respectively or
simply monoidal monads and Kleisli monads for short. We then show that the two
@ -1230,8 +1248,8 @@ The monoidal formulation of monads consists of the following data:
\label{eq:monad-monoidal-data}
\begin{split}
\EndoR & \tp \Endo ℂ \\
\var{pure} & \tp \NT{\EndoR^0}{\EndoR} \\
\var{join} & \tp \NT{\EndoR^2}{\EndoR}
\pure & \tp \NT{\EndoR^0}{\EndoR} \\
\join & \tp \NT{\EndoR^2}{\EndoR}
\end{split}
\end{align}
%
@ -1246,10 +1264,10 @@ following laws:
\begin{align}
\label{eq:monad-monoidal-laws}
\begin{split}
\var{join} \lll \fmap\ \var{join}
& ≡ \var{join} \lll \var{join}\ \fmap \\
\var{join} \lll \var{pure}\ \fmap & ≡ \identity \\
\var{join} \lll \fmap\ \var{pure} & ≡ \identity
\join \lll \fmap\ \join
& ≡ \join \lll \join\ \fmap \\
\join \lll \pure\ \fmap & ≡ \identity \\
\join \lll \fmap\ \pure & ≡ \identity
\end{split}
\end{align}
%
@ -1273,7 +1291,7 @@ The Kleisli-formulation consists of the following data:
%
The objects $X$ and $Y$ are implicitly universally quantified.
It's interesting to note here that this formulation does not talk about natural
It is interesting to note here that this formulation does not talk about natural
transformations or other such constructs from category theory. All we have here
is a regular maps on objects and a pair of arrows.
%

25
doc/introduction.tex
View file

@ -1,30 +1,20 @@
\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 i. what is \emph{provable} and ii. 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}%
Consider the functions:
%
\begin{multicols}{2}
\noindent
\begin{equation*}
f \defeq (n \tp \bN) \mapsto (0 + n \tp \bN)
f \defeq (n \tp \bN) \mto (0 + n \tp \bN)
\end{equation*}
\begin{equation*}
g \defeq (n \tp \bN) \mapsto (n + 0 \tp \bN)
g \defeq (n \tp \bN) \mto (n + 0 \tp \bN)
\end{equation*}
\end{multicols}
%
@ -33,7 +23,6 @@ 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 \\
@ -55,21 +44,21 @@ equivalence of $f$ and $g$ -- even though we can prove them equal for all
points. This is exactly the notion of equality of functions that we are
interested in; that they are equal for all inputs. We call this
\nomen{point-wise equality}, where the \emph{points} of a function refers
to it's arguments.
to its arguments.
In the context of category theory functional extensionality is e.g. needed to
show that representable functors are indeed functors. The representable functor
for a category $\bC$ and a fixed object in $A \in \bC$ is defined to be:
%
\begin{align*}
\fmap \defeq X \mapsto \Hom_{\bC}(A, X)
\fmap \defeq X \mto \Hom_{\bC}(A, X)
\end{align*}
%
The proof obligation that this satisfies the identity law of functors
($\fmap\ \idFun \equiv \idFun$) thus becomes:
%
\begin{align*}
\Hom(A, \idFun_{\bX}) = (g \mapsto \idFun \comp g) \equiv \idFun_{\Sets}
\Hom(A, \idFun_{\bX}) = (g \mto \idFun \comp g) \equiv \idFun_{\Sets}
\end{align*}
%
One needs functional extensionality to ``go under'' the function arrow and apply
@ -92,7 +81,7 @@ be performed in ITT.
More specifically what we are interested in is a way of identifying
\nomen{equivalent} types. I will return to the definition of equivalence later
in section \ref{sec:equiv}, but for now it is sufficient to think of an
in section \S\ref{sec:equiv}, but for now it is sufficient to think of an
equivalence as a one-to-one correspondence. We write $A \simeq B$ to assert that
$A$ and $B$ are equivalent types. The principle of univalence says that:
%

BIN
doc/isomorphism.png
View file

Binary file not shown.
Side by side Swipe Overlay

Before

Width:  |  Height:  |  Size: 344 KiB

After

Width:  |  Height:  |  Size: 266 KiB

102
doc/macros.tex
View file

@ -12,7 +12,8 @@
\newcommand{\bC}{\mathbb{C}}
\newcommand{\bX}{\mathbb{X}}
% \newcommand{\to}{\rightarrow}
\newcommand{\mto}{\mapsto}
%% \newcommand{\mto}{\mapsto}
\newcommand{\mto}{\rightarrow}
\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
\let\type\UU
\newcommand{\MCU}{\UU}
@ -32,57 +33,62 @@
}
\makeatother
\newcommand{\var}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\Hom}{\var{Hom}}
\newcommand{\fmap}{\var{fmap}}
\newcommand{\bind}{\var{bind}}
\newcommand{\join}{\var{join}}
\newcommand{\omap}{\var{omap}}
\newcommand{\pure}{\var{pure}}
\newcommand{\idFun}{\var{id}}
\newcommand{\Sets}{\var{Sets}}
\newcommand{\Set}{\var{Set}}
\newcommand{\hSet}{\var{hSet}}
\newcommand{\id}{\var{id}}
\newcommand{\isEquiv}{\var{isEquiv}}
\newcommand{\idToIso}{\var{idToIso}}
\newcommand{\isSet}{\var{isSet}}
\newcommand{\isContr}{\var{isContr}}
\newcommand{\isGroupoid}{\var{isGroupoid}}
\newcommand{\pathJ}{\var{pathJ}}
\newcommand\Object{\var{Object}}
\newcommand\Functor{\var{Functor}}
\newcommand\isProp{\var{isProp}}
\newcommand\propPi{\var{propPi}}
\newcommand\propSig{\var{propSig}}
\newcommand\PreCategory{\var{PreCategory}}
\newcommand\IsPreCategory{\var{IsPreCategory}}
\newcommand\isIdentity{\var{isIdentity}}
\newcommand\propIsIdentity{\var{propIsIdentity}}
\newcommand\IsCategory{\var{IsCategory}}
\newcommand\Gl{\var{\lambda}}
\newcommand\lemPropF{\var{lemPropF}}
\newcommand\isPreCategory{\var{isPreCategory}}
\newcommand\congruence{\var{cong}}
\newcommand\identity{\var{identity}}
\newcommand\isequiv{\var{isequiv}}
\newcommand\qinv{\var{qinv}}
\newcommand\fiber{\var{fiber}}
\newcommand\shuffle{\var{shuffle}}
\newcommand\Univalent{\var{Univalent}}
\newcommand\refl{\var{refl}}
\newcommand\isoToId{\var{isoToId}}
\newcommand\Isomorphism{\var{Isomorphism}}
\newcommand{\varindex}[1]{\ensuremath{\mathit{#1}}\index{#1}}
\newcommand{\Hom}{\varindex{Hom}}
\newcommand{\fmap}{\varindex{fmap}}
\newcommand{\bind}{\varindex{bind}}
\newcommand{\join}{\varindex{join}}
\newcommand{\omap}{\varindex{omap}}
\newcommand{\pure}{\varindex{pure}}
\newcommand{\idFun}{\varindex{id}}
\newcommand{\Sets}{\varindex{Sets}}
\newcommand{\Set}{\varindex{Set}}
\newcommand{\hSet}{\varindex{hSet}}
\newcommand{\id}{\varindex{id}}
\newcommand{\isEquiv}{\varindex{isEquiv}}
\newcommand{\idToIso}{\varindex{idToIso}}
\newcommand{\idIso}{\varindex{idIso}}
\newcommand{\isSet}{\varindex{isSet}}
\newcommand{\isContr}{\varindex{isContr}}
\newcommand{\isGroupoid}{\varindex{isGroupoid}}
\newcommand{\pathJ}{\varindex{pathJ}}
\newcommand\Object{\varindex{Object}}
\newcommand\Functor{\varindex{Functor}}
\newcommand\isProp{\varindex{isProp}}
\newcommand\propPi{\varindex{propPi}}
\newcommand\propSig{\varindex{propSig}}
\newcommand\PreCategory{\varindex{PreCategory}}
\newcommand\IsPreCategory{\varindex{IsPreCategory}}
\newcommand\isIdentity{\varindex{isIdentity}}
\newcommand\propIsIdentity{\varindex{propIsIdentity}}
\newcommand\IsCategory{\varindex{IsCategory}}
\newcommand\Gl{\varindex{\lambda}}
\newcommand\lemPropF{\varindex{lemPropF}}
\newcommand\isPreCategory{\varindex{isPreCategory}}
\newcommand\congruence{\varindex{cong}}
\newcommand\identity{\varindex{identity}}
\newcommand\isequiv{\varindex{isequiv}}
\newcommand\qinv{\varindex{qinv}}
\newcommand\fiber{\varindex{fiber}}
\newcommand\shuffle{\varindex{shuffle}}
\newcommand\Univalent{\varindex{Univalent}}
\newcommand\refl{\varindex{refl}}
\newcommand\isoToId{\varindex{isoToId}}
\newcommand\Isomorphism{\varindex{Isomorphism}}
\newcommand\rrr{\ggg}
\newcommand\fish{\mathrel{\wideoverbar{\rrr}}}
\newcommand\fst{\var{fst}}
\newcommand\snd{\var{snd}}
\newcommand\Path{\var{Path}}
\newcommand\Category{\var{Category}}
\newcommand\fst{\varindex{fst}}
\newcommand\snd{\varindex{snd}}
\newcommand\Path{\varindex{Path}}
\newcommand\Category{\varindex{Category}}
\newcommand\TODO[1]{TODO: \emph{#1}}
\newcommand*{\QED}{\hfill\ensuremath{\square}}%
\newcommand\uexists{\exists!}
\newcommand\Arrow{\var{Arrow}}
\newcommand\NTsym{\var{NT}}
\newcommand\Arrow{\varindex{Arrow}}
\newcommand\NTsym{\varindex{NT}}
\newcommand\NT[2]{\NTsym\ #1\ #2}
\newcommand\Endo[1]{\var{Endo}\ #1}
\newcommand\Endo[1]{\varindex{Endo}\ #1}
\newcommand\EndoR{\mathcal{R}}
\newcommand\funExt{\varindex{funExt}}
\newcommand{\suc}[1]{\mathit{suc}\ #1}

13
doc/main.tex
View file

@ -42,19 +42,15 @@
\institution{\chalmers}
\department{Department of Computer Science and Engineering}
\researchgroup{Programming Logic Group}
\bibliographystyle{plain}
%% \newtheorem{prop}{Proposition}
\makeatletter
\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@}
\makeatother
\begin{document}
\frontmatter
\myfrontmatter
\pagenumbering{roman}
\maketitle
\addtocontents{toc}{\protect\thispagestyle{empty}}
\input{abstract.tex}
\tableofcontents
\pagenumbering{arabic}
\mainmatter
%
\input{introduction.tex}
\input{cubical.tex}
@ -73,4 +69,5 @@
%% \input{planning.tex}
%% \input{halftime.tex}
\end{appendices}
\printindex
\end{document}

32
doc/packages.tex
View file

@ -1,6 +1,8 @@
\usepackage[utf8]{inputenc}
\usepackage{natbib}
\bibliographystyle{plain}
\usepackage[
hidelinks,
pdfusetitle,
@ -15,8 +17,9 @@
\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym}
\usepackage[toc,page]{appendix}
\usepackage{xspace}
\usepackage[a4paper]{geometry}
\usepackage[a4paper,top=3cm,bottom=3cm]{geometry}
\usepackage{makeidx}
\makeindex
% \setlength{\parskip}{10pt}
% \usepackage{tikz}
@ -85,3 +88,28 @@
\newunicodechar{𝒜}{\textfallback{?}}
\newunicodechar{ℬ}{\textfallback{?}}
%% \newunicodechar{≊}{\textfallback{≊}}
\makeatletter
\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@}
\makeatother
\makeatletter
\newcommand\frontmatter{%
\cleardoublepage
%\@mainmatterfalse
\pagenumbering{roman}}
\newcommand\mainmatter{%
\cleardoublepage
% \@mainmattertrue
\pagenumbering{arabic}}
\newcommand\backmatter{%
\if@openright
\cleardoublepage
\else
\clearpage
\fi
% \@mainmatterfalse
}
\makeatother

7
doc/sources.tex
View file

@ -1,15 +1,15 @@
\chapter{Source code}
\chapter{Source code excerpts}
\label{ch:app-sources}
In the following a few of the definitions mentioned in the report are included.
The following is \emph{not} a verbatim copy of individual modules from the
implementation. Rather, this is a redacted and pre-formatted designed for
presentation purposes. It's provided here as a convenience. The actual sources
presentation purposes. Its provided here as a convenience. The actual sources
are the only authoritative source. Is something is not clear, please refer to
those.
\clearpage
\section{Cubical}
\label{sec:app-cubical}
\begin{figure}[h]
\label{fig:path}
\begin{Verbatim}
postulate
PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
@ -23,6 +23,7 @@ module _ {ℓ} {A : Set ℓ} where
\end{Verbatim}
\caption{Excerpt from the cubical library. Definition of the path-type.}
\end{figure}
\clearpage
%
\begin{figure}[h]
\begin{Verbatim}