267 lines
12 KiB
TeX
267 lines
12 KiB
TeX
\chapter{Introduction}
|
||
This thesis is a case study in the application of cubical Agda to the
|
||
formalization of category theory. At the center of this is the notion
|
||
of \nomenindex{equality}. There are two pervasive notions of equality
|
||
in type theory: \nomenindex{judgmental equality} and
|
||
\nomenindex{propositional equality}. Judgmental equality is a property
|
||
of the type system. Propositional equality on the other hand is
|
||
usually defined \emph{within} the system. When introducing
|
||
definitions this report will use the symbol $\defeq$. Judgmental
|
||
equalities will be denoted with $=$ and for propositional equalities
|
||
the notation $\equiv$ is used.
|
||
|
||
The rules of judgmental equality are related with $β$- and
|
||
$η$-reduction, which gives a notion of computation in a given type
|
||
theory.
|
||
%
|
||
There are some properties that one usually want judgmental equality to
|
||
satisfy. It must be \nomenindex{sound}, enjoy \nomenindex{canonicity}
|
||
and be a \nomenindex{congruence relation}. Soundness means that things
|
||
judged to be equal are equal with respects to the \nomenindex{model}
|
||
of the theory or the \emph{meta theory}. It must be a congruence
|
||
relation, because otherwise the relation certainly does not adhere to
|
||
our notion of equality. E.g.\ One would be able to conclude things
|
||
like: $x \equiv y \rightarrow f\ x \nequiv f\ y$. Canonicity means
|
||
that any well typed term evaluates to a \emph{canonical} form. For
|
||
example, for a closed term $e \tp \bN$, it will be the case that $e$
|
||
reduces to $n$ applications of $\mathit{suc}$ to $0$ for some $n$;
|
||
i.e.\ $e = \mathit{suc}^n\ 0$. Without canonicity terms in the
|
||
language can get ``stuck'', meaning that they do not reduce to a
|
||
canonical form.
|
||
|
||
For a system to work as a programming languages it is necessary for
|
||
judgmental equality to be \nomenindex{decidable}. Being decidable
|
||
simply means that that an algorithm exists to decide whether two terms
|
||
are equal. For any practical implementation, the decidability must
|
||
also be effectively computable.
|
||
|
||
For propositional equality the decidability requirement is relaxed. It
|
||
is not in general possible to decide the correctness of logical
|
||
propositions (cf.\ Hilbert's \emph{entscheidigungsproblem}).
|
||
|
||
There are two flavors of type-theory. \emph{Intensional-} and
|
||
\emph{extensional-} type theory (ITT and ETT respectively). Identity
|
||
types in extensional type theory are required to be
|
||
\nomen{propositions}{proposition}. That is, a type with at most one
|
||
inhabitant. In extensional type theory the principle of reflection
|
||
%
|
||
$$a ≡ b → a = b$$
|
||
%
|
||
is enough to make type checking undecidable. This report focuses on
|
||
Agda, which at a glance can be thought of as a version of intensional
|
||
type theory. Pattern-matching in regular Agda lets one prove
|
||
\nomenindex{Uniqueness of Identity Proofs} (UIP). UIP states that any
|
||
two identity proofs are propositionally identical.
|
||
|
||
The usual notion of propositional equality in ITT is quite
|
||
restrictive. In the next section a few motivating examples will be
|
||
presented that highlight. There exist techniques to circumvent these
|
||
problems, as we shall see. This thesis will explore an extension to
|
||
Agda that redefines the notion of propositional equality and as such
|
||
is an alternative to these other techniques. The extension is called
|
||
cubical Agda. Cubical Agda drops UIP, as it does not permit
|
||
\nomenindex{functional extensionality} nor \nomenindex{univalence}.
|
||
What makes cubical Agda particularly interesting is that it gives a
|
||
\emph{constructive} interpretation of univalence. What all this means
|
||
will be elaborated in the following sections.
|
||
%
|
||
\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{align*}%
|
||
\var{zeroLeft} & \defeq λ\; (n \tp \bN) \to (0 + n \tp \bN) \\
|
||
\var{zeroRight} & \defeq λ\; (n \tp \bN) \to (n + 0 \tp \bN)
|
||
\end{align*}%
|
||
%
|
||
The term $n + 0$ is \nomenindex{definitionally} equal to $n$, which we
|
||
write as $n + 0 = n$. This is also called \nomenindex{judgmental
|
||
equality}. We call it definitional equality because the
|
||
\emph{equality} arises from the \emph{definition} of $+$, which is:
|
||
%
|
||
\begin{align*}
|
||
+ & \tp \bN \to \bN \to \bN \\
|
||
n + 0 & \defeq n \\
|
||
n + (\suc{m}) & \defeq \suc{(n + m)}
|
||
\end{align*}
|
||
%
|
||
Note that $0 + n$ is \emph{not} definitionally equal to $n$. This is
|
||
because $0 + n$ is in normal form. I.e.\ there is no rule for $+$
|
||
whose left hand side matches this expression. We do, however, have that
|
||
they are \nomen{propositionally}{propositional equality} equal, which
|
||
we write as $n \equiv n + 0$. Propositional equality means that there
|
||
is a proof that exhibits this relation. We can do induction over $n$
|
||
to prove this:
|
||
%
|
||
\begin{align}
|
||
\label{eq:zrn}
|
||
\begin{split}
|
||
\var{zrn}\ & \tp ∀ n → n ≡ \var{zeroRight}\ n \\
|
||
\var{zrn}\ \var{zero} & \defeq \var{refl} \\
|
||
\var{zrn}\ (\var{suc}\ n) & \defeq \var{cong}\ \var{suc}\ (\var{zrn}\ n)
|
||
\end{split}
|
||
\end{align}
|
||
%
|
||
This show that zero is a right neutral element (hence the name
|
||
$\var{zrn}$). Since equality is a transitive relation we have that
|
||
$\forall n \to \var{zeroLeft}\ n \equiv \var{zeroRight}\ n$.
|
||
Unfortunately we don't have $\var{zeroLeft} \equiv \var{zeroRight}$.
|
||
There is no way to construct a proof asserting the obvious equivalence
|
||
of $\var{zeroLeft}$ and $\var{zeroRight}$. Actually showing this is
|
||
outside the scope of this text. It would essentially involve giving a
|
||
model for our type theory that validates all our axioms but where
|
||
$\var{zeroLeft} \equiv \var{zeroRight}$ is not true. We cannot show
|
||
that they are equal even though we can prove them equal for all
|
||
points. This is exactly the notion of equality that we are interested
|
||
in for functions: Functions are considered equal when they are equal
|
||
for all inputs. This is called \nomenindex{pointwise equality} where
|
||
\emph{points} of a function refer to its arguments.
|
||
%
|
||
\subsection{Equality of isomorphic types}
|
||
%
|
||
Let $\top$ denote the unit type -- a type with a single constructor.
|
||
In the propositions as types interpretation of type theory $\top$ is
|
||
the proposition that is always true. The type $A \x \top$ and $A$ has
|
||
an element for each $a \tp A$. So in a sense they have the same shape
|
||
(Greek; \nomenindex{isomorphic}). The second element of the pair does
|
||
not add any ``interesting information''. It can be useful to identify
|
||
such types. In fact it is quite commonplace in mathematics. Say we
|
||
look at a set $\{x \mid \phi\ x \land \psi\ x\}$ and somehow conclude
|
||
that $\psi\ x \equiv \top$ for all $x$. A mathematician would
|
||
immediately conclude $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid
|
||
\phi\ x\}$ without thinking twice. Unfortunately such an
|
||
identification can not be performed in ITT.
|
||
|
||
More specifically what we are interested in is a way of identifying
|
||
\nomenindex{equivalent} types. I will return to the definition of
|
||
equivalence later 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:
|
||
%
|
||
$$\mathit{univalence} \tp (A \simeq B) \simeq (A \equiv B)$$
|
||
%
|
||
In particular this allows us to construct an equality from an equivalence
|
||
%
|
||
$$\mathit{ua} \tp (A \simeq B) \to (A \equiv B)$$
|
||
%
|
||
and vice versa.
|
||
|
||
\section{Formalizing Category Theory}
|
||
%
|
||
The above examples serve to illustrate a limitation of ITT. One case
|
||
where these limitations are particularly prohibitive is in the study
|
||
of Category Theory. At a glance category theory can be described as
|
||
``the mathematical study of (abstract) algebras of functions''
|
||
(\cite{awodey-2006}). By that token functional extensionality is
|
||
particularly useful for formulating Category Theory. In Category
|
||
theory it is also commonplace to identify isomorphic structures.
|
||
Univalence gives us a way to make this notion precise. In fact we can
|
||
formulate this requirement within our formulation of categories by
|
||
requiring the \emph{categories} themselves to be univalent as we shall
|
||
see in section \S\ref{sec:univalence}.
|
||
|
||
\section{Context}
|
||
\label{sec:context}
|
||
%
|
||
The idea of formalizing Category Theory in proof assistants is not new. There
|
||
are a multitude of these available online. Notably:
|
||
%
|
||
\begin{itemize}
|
||
\item
|
||
A formalization in Agda using the setoid approach:
|
||
\url{https://github.com/copumpkin/categories}
|
||
\item
|
||
A formalization in Agda with univalence and functional
|
||
extensionality as postulates:
|
||
\url{https://github.com/pcapriotti/agda-categories}
|
||
\item
|
||
A formalization in Coq in the homotopic setting:
|
||
\url{https://github.com/HoTT/HoTT/tree/master/theories/Categories}
|
||
\item
|
||
A formalization in \emph{CubicalTT} -- a language designed for
|
||
cubical type theory. Formalizes many different things, but only a
|
||
few concepts from category theory:
|
||
\url{https://github.com/mortberg/cubicaltt}
|
||
\end{itemize}
|
||
%
|
||
The contribution of this thesis is to explore how working in a cubical
|
||
setting will make it possible to prove more things, to reuse proofs
|
||
and to compare some aspects of this formalization with the existing
|
||
ones.
|
||
|
||
There are alternative approaches to working in a cubical setting where
|
||
one can still have univalence and functional extensionality. One
|
||
option is to postulate these as axioms. This approach, however, has
|
||
other shortcomings, e.g.\ you lose \nomenindex{canonicity}
|
||
(\cite[p.\ 3]{huber-2016}).
|
||
|
||
Another approach is to use the \emph{setoid interpretation} of type
|
||
theory (\cite{hofmann-1995,huber-2016}). With this approach one works
|
||
with \nomenindex{extensional sets} $(X, \sim)$. That is a type $X \tp
|
||
\MCU$ and an equivalence relation $\sim\ \tp X \to X \to \MCU$ on that
|
||
type. Under the setoid interpretation the equivalence relation serve
|
||
as a sort of ``local'' propositional equality. Since the developer
|
||
gets to pick this relation, it is not a~priori a congruence
|
||
relation. It must be manually verified by the developer. Furthermore,
|
||
functions between different setoids must be shown to be setoid
|
||
homomorphism, that is; they preserve the relation.
|
||
|
||
This approach has other drawbacks: It does not satisfy all
|
||
propositional equalities of type theory a~priori. That is, the
|
||
developer must manually show that e.g.\ the relation is a congruence.
|
||
Equational proofs $a \sim_{X} b$ are in some sense `local' to the
|
||
extensional set $(X , \sim)$. To e.g.\ prove that $x ∼ y → f\ x ∼
|
||
f\ y$ for some function $f \tp A → B$ between two extensional sets $A$
|
||
and $B$ it must be shown that $f$ is a groupoid homomorphism. This
|
||
makes it very cumbersome to work with in practice (\cite[p.
|
||
4]{huber-2016}).
|
||
|
||
\section{Conventions}
|
||
In the remainder of this thesis I will use the term \nomenindex{Type}
|
||
to describe -- well -- types; thereby departing from the notation in
|
||
Agda where the keyword \texttt{Set} refers to types.
|
||
\nomenindex{Set}, on the other hand, shall refer to the homotopical
|
||
notion of a set. I will also leave all universe levels implicit. This
|
||
of course does not mean that a statement such as $\MCU \tp \MCU$ means
|
||
that we have type-in-type but rather that the arguments to the
|
||
universes are implicit.
|
||
|
||
I use the term \nomenindex{arrow} to refer to morphisms in a category,
|
||
whereas the terms \nomenindex{morphism}, \nomenindex{map} or
|
||
\nomenindex{function} shall be reserved for talking about type
|
||
theoretic functions; i.e.\ functions in Agda.
|
||
|
||
As already noted $\defeq$ will be used for introducing definitions $=$
|
||
will be used to for judgmental equality and $\equiv$ will be used for
|
||
propositional equality.
|
||
|
||
All this is summarized in the following table:
|
||
%
|
||
\begin{samepage}
|
||
\begin{center}
|
||
\begin{tabular}{ c c c }
|
||
Name & Agda & Notation \\
|
||
\hline
|
||
|
||
\varindex{Type} & \texttt{Set} & $\Type$ \\
|
||
|
||
\varindex{Set} & \texttt{Σ Set IsSet} & $\Set$ \\
|
||
Function, morphism, map & \texttt{A → B} & $A → B$ \\
|
||
Dependent- ditto & \texttt{(a : A) → B} & $∏_{a \tp A} B$ \\
|
||
|
||
\varindex{Arrow} & \texttt{Arrow A B} & $\Arrow\ A\ B$ \\
|
||
|
||
\varindex{Object} & \texttt{C.Object} & $̱ℂ.Object$ \\
|
||
Definition & \texttt{=} & $̱\defeq$ \\
|
||
Judgmental equality & \null & $̱=$ \\
|
||
Propositional equality & \null & $̱\equiv$
|
||
\end{tabular}
|
||
\end{center}
|
||
\end{samepage}
|