\chapter{Cubical Agda} \section{Propositional equality} Judgmental equality in Agda is a feature of the type system. Its 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} % 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 \nomenindex{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 \nomenindex{homogeneous equalities} is recovered when $P$ does not depend on its argument. That is for $A \tp \MCU$, $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 \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 is also surpisingly easy to show functional extensionality with which we can construct a path between $f$ and $g$ -- the functions defined in the introduction (section \S\ref{sec:functional-extensionality}). 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 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 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} % 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).\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 will not give an example of a set at this point. It turns out that proving e.g. $\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{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. 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$. 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 \nomen{base case}{path induction}). 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: % $$ 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\ a\ p \end{equation} % 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 on path induction 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 \tp \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 its first component is a proposition, and its 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) $$