271 lines
12 KiB
TeX
271 lines
12 KiB
TeX
\chapter{Introduction}
|
||
This thesis is a case-study in the application of cubical Agda in the
|
||
context of category theory. At the center of this is the notion of
|
||
\nomenindex{equality}. In type-theory there are two pervasive notions
|
||
of equality: \nomenindex{judgmental equality} and
|
||
\nomenindex{propositional equality}. Judgmental equality is a property
|
||
of the type system. Judgmental 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. 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$; $e =
|
||
\mathit{suc}^n\ 0$. Without canonicity terms in the language can get
|
||
``stuck'' meaning that they do not reduce to a canonical form.
|
||
|
||
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
|
||
highlight this. 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 this does not permit
|
||
\nomenindex{functional extensionality} and
|
||
\nomenindex{univalence}. What makes this extension 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 \lambda\; (n \tp \bN) \to (0 + n \tp \bN) \\
|
||
\var{zeroRight} & \defeq \lambda\; (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. Essentially it would 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. For functions this is exactly the notion of equality that we
|
||
are interested in: Functions are considered equal when they are equal
|
||
for all inputs. This is called \nomenindex{pointwise equality}, where
|
||
the \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 and
|
||
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 \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 and to reuse proofs and to try and
|
||
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. So this must be verified manually 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 paper 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.
|
||
|
||
And 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}
|