cat/doc/cubical.tex

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

Most of the source code related with this section is implemented in
\cite{cubical-demo} it can be browsed in hyperlinked and syntax
highlighted HTML online. The links can be found in the beginning of
section \S\ref{ch:implementation}.

\subsection{The equality type}
The usual notion of judgmental equality says that given a type $A \tp
\MCU$ and two points hereof $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 $\refl$ that for any $a \tp A$ gives:
%
\begin{align}
  \refl \tp a \equiv a
\end{align}
%
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 likewise has the single constructor $\refl$ that for any $a \tp
A$ gives:
%
\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}
%
The special type $\I$ is called the index set. The index set can be
thought of simply as the interval on the real numbers from $0$ to $1$
(both inclusive). The family $P$ over $\I$ will be referred to as the
\nomenindex{path space} given some path $p \tp \Path\ P\ a\ b$. By
that token $P\ 0$ corresponds to the type at the left endpoint of $p$.
Likewise $P\ 1$ is the type at the right endpoint. The type is called
$\Path$ because the idea has roots in homotopy theory. The intuition
is that $\Path$ describes\linebreak[1] paths in $\MCU$. I.e.\ paths
between types. For a path $p$ the expression $p\ i$ can be thought of
as a \emph{point} on this path. 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 from the index set to the path space:
%
$$
p \tp \prod_{i \tp \I} P\ i
$$
%
Which must satisfy being judgmentally equal to $a_0$ at the
left endpoint and equal to $a_1$ at the other end. I.e.:
%
\begin{align*}
  p\ 0 & = a_0 \\
  p\ 1 & = a_1
\end{align*}
%
The notion of \nomenindex{homogeneous equalities} is recovered when $P$ does not
depend on its argument. That is for $A \tp \MCU$ and $a_0, a_1 \tp A$ the
homogenous equality between $a_0$ and $a_1$ is the type:
%
$$
a_0 \equiv a_1 \defeq \Path\ (\lambda\;i \to A)\ a_0\ a_1
$$
%
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 a \equiv 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 is constantly $a$ at any index
$i \tp \I$.

It is also surprisingly easy to show functional extensionality.
Functional extensionality is the proposition that 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$ gives:
%
\begin{equation}
\label{eq:funExt}
\funExt \tp \left(\prod_{a \tp A} f\ a \equiv g\ a \right) \to f \equiv g
\end{equation}
%
%% p = λ\; i a → p a i
So given $η \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 $η$ and get the path $η\ a \tp f\ a \equiv g\ a$. And this exactly
satisfies the conditions for $\phi$. In conclustion \ref{eq:funExt} is inhabited
by the term:
%
\begin{equation*}
\funExt\ η \defeq λ\; i\ a → η\ a\ i
\end{equation*}
%
With $\funExt$ in place we can now construct a path between
$\var{zeroLeft}$ and $\var{zeroRight}$ -- the functions defined in the
introduction \S\ref{sec:functional-extensionality}:
%
\begin{align*}
  p & \tp \var{zeroLeft} \equiv \var{zeroRight} \\
  p & \defeq \funExt\ \var{zrn}
\end{align*}
%
Here $\var{zrn}$ is the proof from \ref{eq:zrn}.
%
\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 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 in cubical Agda we have a hierarchy of types with an increasing
amount of homotopic structure. At the bottom of this hierarchy is 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}
%
One can think of $\isProp\ A$ 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*}
%
The term $\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).

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

The next step in the hierarchy is 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 will not give an example of a set at this point. It turns out that
proving e.g.\ $\isProp\ \bN$ directly is not so straightforward (see
\cite[\S3.1.4]{hott-2013}). Hedberg's theorem states that any type
with decidable equality is a set. 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.

As the reader may have guessed the next step in the hierarchy is 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}{homotopy
  levels}, propositions are \nomen{-1-types}{homotopy levels}, (homotopical)
sets are \nomen{0-types}{homotopy levels} 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$.

For any level $n$ it is the case that to be of level $n$ 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 that have already been formalized.
Specifically the results come from the Agda library \texttt{cubical}
(\cite{cubical-demo}). 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 which are available at
  \hrefsymb{https://github.com/Saizan/cubical-demo}{\texttt{https://github.com/Saizan/cubical-demo}}.
}.

These theorems are all purely related to homotopy type theory 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 throughout
chapter \ref{ch:implementation}. They should also give the reader some
intuition about the path type.

\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 \nomen{base case}{path induction}). For \emph{based
  path induction}, that equality is \emph{based} at some element $a
\tp A$.

\pagebreak[3]
\begin{samepage}
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.\linebreak[3] Given
a family of types:
%
$$
D \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} \MCU
$$
%
And an inhabitant of $D$ at $\refl$:
%
$$
d \tp D\ a\ \refl
$$
%
We have the function:
%
\begin{equation}
\pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ b\ p
\end{equation}
\end{samepage}%

A simple application of $\pathJ$ is for proving that $\var{sym}$ is an
involution. Namely for any set $A \tp \MCU$, points $a, b \tp A$ and a path
between them $p \tp a \equiv b$:
%
\begin{equation}
\label{eq:sym-invol}
\var{sym}\ (\var{sym}\ p) ≡ p
\end{equation}
%
The proof will be by induction on $p$ and will be based at $a$. That
is $D$ will be the family:
%
\begin{align*}
D         & \tp \prod_{b' \tp A} \prod_{p \tp a ≡ b'} \MCU \\
D\ b'\ p' & \defeq \var{sym}\ (\var{sym}\ p') ≡ p'
\end{align*}
%
The base case will then be:
%
\begin{align*}
d & \tp \var{sym}\ (\var{sym}\ \refl) ≡ \refl \\
d & \defeq \refl
\end{align*}
%
The reason $\refl$ proves this is that $\var{sym}\ \refl = \refl$ holds
definitionally. In summary \ref{eq:sym-invol} is inhabited by the term:
%
\begin{align*}
  \pathJ\ D\ d\ b\ p
  \tp
  \var{sym}\ (\var{sym}\ p) ≡ p
\end{align*}
%
Another application of $\pathJ$ is for proving associativity of $\trans$. That
is, given a type $A \tp \MCU$, elements of $A$, $a, b, c, d \tp A$ and paths
between them $p \tp a \equiv b$, $q \tp b \equiv c$ and $r \tp c \equiv d$ we
have the following:
%
\begin{equation}
  \label{eq:cum-trans}
  \trans\ p\ (\trans\ q\ r) ≡ \trans\ (\trans\ p\ q)\ r
\end{equation}
%
In this case the induction will be based at $c$ (the left-endpoint of $r$) and
over the family:
%
\begin{align*}
  T       & \tp \prod_{d' \tp A} \prod_{r' \tp c ≡ d'} \MCU \\
  T\ d'\ r' & \defeq \trans\ p\ (\trans\ q\ r') ≡ \trans\ (\trans\ p\ q)\ r'
\end{align*}
%
So the base case is proven with $t$ which is defined as:
%
\begin{align*}
  \trans\ p\ (\trans\ q\ \refl) & ≡
  \trans\ p\ q \\
   & ≡
  \trans\ (\trans\ p\ q)\ \refl
\end{align*}
%
Here we have used the proposition $\trans\ p\ \refl \equiv p$ without proof. In
conclusion \ref{eq:cum-trans} is inhabited by the term:
%
\begin{align*}
\pathJ\ T\ t\ d\ r
\end{align*}
%
We shall see another application of path induction in \ref{eq:pathJ-example}.

\subsection{Paths over propositions}
\label{sec:lemPropF}
Another very useful combinator is $\lemPropF$: Given a type $A \tp
\MCU$ and a type family on $A$; $D \tp A \to \MCU$. Let $\var{propD}
\tp \prod_{x \tp A} \isProp\ (D\ x)$ be the proof that $D$ 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 $d_0 \tp
D\ a_0$ and $d_1 \tp D\ a_1$.
%
$$
\lemPropF\ \var{propD}\ p \tp \Path\ (\lambda\; i \mto D\ (p\ i))\ d_0\ d_1
$$
%
Note that $d_0$ and $d_1$, though points of the same family, have
different types. 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
say we have a type:
%
$$
T \defeq \sum_{a \tp A} D\ a
$$
%
For some proposition $D \tp A \to \MCU$. That is we have $\var{propD}
\tp \prod_{a \tp A} \isProp\ (D\ a)$. 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 D\ (p\ i))\ (\snd\ t_0)\ (\snd\ t_1)
\end{align*}
%
Here $\lemPropF$ directly allow us to prove the latter of these given
that we have already provided $p$.
%
$$
\lemPropF\ \var{propD}\ p
  \tp \Path\ (\lambda\; i \to D\ (p\ i))\ (\snd\ t_0)\ (\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 its first component is
a proposition, and its second component is a proposition for all
points of 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)
$$