cat/doc/cubical.tex

\chapter{Cubical Agda}
\section{Propositional equality}
Judgmental equality in Agda is a feature of the type-system. It's 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 $+$.

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
\S\ref{sec:app-cubical}.

\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
for any $a \tp A$:
%
\begin{align}
  \refl \tp a \equiv a
\end{align}
%
For any $a \tp A$.

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:
%
\begin{align}
  a \cong b \tp \MCU
\end{align}
%
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
\end{align}
%
In Cubical Agda these two notions are paralleled with homogeneous- and
heterogeneous paths respectively.
%
\subsection{The path 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
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 \prod_{i \tp I} 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'' is recovered when $P$ does not 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 \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
\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}
%
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$.

It's 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 (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\ 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$''. 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:
%
\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. And
indeed both $\top$ and $\bot$ are propositions:
%
\begin{align*}
λ \var{tt}\ \var{tt} → refl & \tp \isProp\ ⊤ \\
λ\varnothing\ \varnothing   & \tp \isProp\ ⊥
\end{align*}
%
I've used $\varnothing$ 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$.

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}
%
I won't give an example of a set at this point. It turns out that proving e.g.
$\isProp\ \bN$ is not so straight-forward (see \S3.1.4 in \ref{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:
%
\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:
%
\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. But we'll see an application
of it in \ref{eq:pathJ-example}.

\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)
$$