cat/doc/cubical.tex

\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
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.

\subsection{The equality type}
The usual notion of judgmental equality says that given a type $A \tp \MCU$ and
two points of $A$; $a_0, a_1 \tp A$ we can form the type:
%
\begin{align}
  a_0 \equiv a_1 \tp \MCU
\end{align}
%
In Agda this is defined as an inductive data-type with the single constructor:
%
\begin{align}
  \refl \tp a \equiv a
\end{align}
%
For any $a \tp A$.

There also exist a related notion of \emph{heterogeneous} equality where 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:
%
\begin{align}
  a \cong b \tp \MCU
\end{align}
%
This is likewise defined as an inductive data-type with a single constructors:
%
\begin{align}
  \refl \tp a \cong a
\end{align}
%
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:
%
$$
\Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU
$$
%
$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
the real numbers from $0$ to $1$. $P$ is a family of types over the index set
$I$. I will sometimes refer to $P$ as the ``path-space'' of some path $p \tp
\Path\ P\ a\ b$. By this token $P\ 0$ then corresponds to the type at the
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:
%
$$
p \tp I \to P\ i
$$
%
Which must satisfy being judgmentally equal to $a_0$ (respectively $a_1$) at the
endpoints. I.e.:
%
\begin{align*}
  p\ 0 & = a_0 \\
  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:
%
$$
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
interest.

With this definition we can also recover reflexivity. That is, for any $A \tp
\MCU$ and $a \tp A$:
%
\begin{equation}
\begin{aligned}
\refl & \tp \Path (\lambda i \to A)\ a\ a \\
\refl & \defeq \lambda i \to a
\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$.

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:
%
\begin{equation}
\begin{aligned}
%% \begin{split}
& \isContr    && \tp \MCU \to \MCU \\
& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
%% \end{split}
\end{aligned}
\end{equation}
%
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$.

The next step in the hierarchy is the set of mere propositions:
%
\begin{equation}
\begin{aligned}
& \isProp    && \tp \MCU \to \MCU \\
& \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1
\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!!}

I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to
stress that we have $\isProp\ A$.

Then comes the set of homotopical sets:
%
\begin{equation}
\begin{aligned}
& \isSet    && \tp \MCU \to \MCU \\
& \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1)
\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.

The next step in the hierarchy is, as the reader might've guessed, the type:
%
\begin{equation}
\begin{aligned}
& \isGroupoid    && \tp \MCU \to \MCU \\
& \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1)
\end{aligned}
\end{equation}
%
And so it continues. In fact we can generalize this family of types by indexing
them with a natural number. For historical reasons, though, the bottom of the
hierarchy, the contractible types, is said to be a \nomen{-2-type}, propositions
are \nomen{-1-types}, (homotopical) sets are \nomen{0-types} and so on\ldots

Just as with paths, homotopical sets are not at the center of focus for this
thesis. But I mention here some properties that will be relevant for this
exposition:

Proposition: Homotopy levels are cumulative. That is, if $A \tp \MCU$ has
homotopy level $n$ then so does it have $n + 1$.

Let $\left\Vert A \right\Vert = n$ denote that the level of $A$ is $n$.
Proposition: For any homotopic level $n$ this is a mere proposition.
%
\section{A few lemmas}
Rather than getting into the nitty-gritty details of Agda I venture to take a
more ``combinator-based'' approach. That is, I will use theorems about paths
already that have already been formalized. Specifically the results come from
the Agda library \texttt{cubical} (\TODO{Cite}). I have used a handful of
results from this library as well as contributed a few lemmas myself.\footnote{The module \texttt{Cat.Prelude} lists the upstream dependencies. As well my contribution to \texttt{cubical} can be found in the git logs \TODO{Cite}.}

These theorems are all purely related to homotopy theory and cubical Agda and as
such not specific to the formalization of Category Theory. I will present a few
of these theorems here, as they will be used later in chapter
\ref{ch:implementation} throughout.

\subsection{Path induction}
\label{sec:pathJ}
The induction principle for paths intuitively gives us a way to reason about a
type-family indexed by a path by only considering if said path is $\refl$ (the
``base-case''). For \emph{based path induction}, that equality is \emph{based}
at some element $a \tp A$.

Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types:
%
$$
P \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} \MCU
$$
%
And an inhabitant of $P$ at $\refl$:
%
$$
p \tp P\ a\ \refl
$$
%
We have the function:
%
$$
\pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p
$$
%
\subsection{Paths over propositions}
\label{sec:lemPropF}
Another very useful combinator is $\lemPropF$:

To `promote' this to a dependent path we can use another useful combinator;
$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $P \tp A \to
\MCU$. Let $\var{propP} \tp \prod_{x \tp A} \isProp\ (P\ x)$ be the proof that
$P$ is a mere proposition for all elements of $A$. Furthermore say we have a
path between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can built
a heterogeneous path between any two elements of $p_0 \tp P\ a_0$ and $p_1 \tp
P\ a_1$:
%
$$
\lemPropF\ \var{propP}\ p \defeq \Path\ (\lambda\; i \mto P\ (p\ i))\ p_0\ p_1
$$
%
This is quite a mouthful. So let me try to show how this is a very general and
useful result.

Often when proving equalities between elements of some dependent types
$\lemPropF$ can be used to boil this complexity down to showing that the
dependent parts of the type are mere propositions. For instance, saw we have a type:
%
$$
T \defeq \sum_{a \tp A} P\ a
$$
%
For some proposition $P \tp A \to \MCU$. If we want to prove $t_0 \equiv t_1$
for two elements $t_0, t_1 \tp T$ then this will be a pair of paths:
%
%
\begin{align*}
  p \tp & \fst\ t_0 \equiv \fst\ t_1 \\
        & \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
\end{align*}
%
Here $\lemPropF$ directly allow us to prove the latter of these:
%
$$
\lemPropF\ \var{propP}\ p
  \tp \Path\ (\lambda i \to P\ (p\ i))\ \snd\ t_0 \equiv \snd\ t_1
$$
%
\subsection{Functions over propositions}
\label{sec:propPi}
$\prod$-types preserve propositionality when the co-domain is always a
proposition.
%
$$
\mathit{propPi} \tp \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
$$
\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
left type.
%
$$
\mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
$$