Upper levels of the equality type tower
In (Martin-Löf) Type Theory, equality between elements of a type is a type itself. This triggers a chain reaction that leads us to consider elements of an equality type between elements of an equality type between elements... and so on. Traditionally we didn’t have to take this tower of equality types seriously though. For example, it doesn’t seem to make much sense to talk about different ways in which natural numbers are equal — $1 + 1$ and $2$ are ‘just equal’, and we don’t need the equality type $1 + 1 =_{\mathbb N} 2$ to have structures beyond the ability to distinguish inhabitance and uninhabitance. In Homotopy Type Theory (HoTT), the type of natural numbers is called a set or a $0$-type. In general, a type $A : \mathcal U$ is a set exactly when it satisfies the predicate
$$ \mathsf{isSet}\ A \defeq \Pi(x\ y : A)\ \Pi(p\ q : x =_A y)\ p = q $$
which says that any equality proofs about elements of $A$ are equal, so we no longer need to care about what equality proofs we get, and the structure of $x =_A y$ becomes trivial in the sense that it is only about inhabitance/uninhabitance.
In HoTT we can go beyond sets and consider higher-dimensional $n$-types: for example, a type $A$ is a $1$-type exactly when all its equality types $x =_A y$ are $0$-types, so the equality proofs on $A$ may have some non-trivial structure, but the equality proofs between the equality proofs on $A$ are trivial. More generally, we can inductively define a family of predicates characterising $n$-types, which are types whose equality types are all trivial above a certain level. The inductive case of the definition is
$$ \mathsf{is\text-}(n+1)\mathsf{\text-type}\ A \defeq \Pi(x\ y : A)\ \mathsf{is\text-}n\mathsf{\text-type}\ (x =_A y) $$
(We’ll see the base case later.) But here we’re more interested in the lower-dimensional direction. Substituting $-1$ for $n$ in the above definition and matching the resulting type equation with the definition of $\mathsf{isSet}$ (which should be the same as $\mathsf{is\text-}0\mathsf{\text-type}$ but actually the two definitions are slightly different; the (reconcilable) difference is a small puzzle which we will formulate and solve below), we get a definition of $(-1)$-types, which are also called mere propositions:
$$ \mathsf{isProp}\ A \defeq \Pi(x\ y : A)\ x =_A y $$
This coincides with the traditional notion of proposition: traditionally mathematicians only care about whether a proposition is true (inhabited) or not, and wouldn’t want to distinguish the elements inhabiting the proposition when it’s modelled as a type. Can we go further? Alas, the definition of $(-2)$-types — which are also called contractible types — won’t reveal itself if we repeat the process; instead, the definition given in the HoTT book reads
$$ \mathsf{isContr}\ A \defeq \Sigma(x : A)\ \Pi(y : A)\ x =_A y $$
which says that there is an element (called the center) which is equal to any (other) element, so a contractible type is basically one that has exactly one element. The inductive definition of $n$-types then takes contractible types as the base case:
$$ \mathsf{is\text-}(-2)\mathsf{\text-type}\ A \defeq \mathsf{isContr}\ A $$
Two questions naturally arise at this point:
- Why are $(-2)$-types the base case? Or: why aren’t there ‘$(-3)$-types’ and so on?
- Do the definitions $\mathsf{isSet}$ and $\mathsf{isProp}$ really coincide with $\mathsf{is\text-}0\mathsf{\text-type}$ and $\mathsf{is\text-}(-1)\mathsf{\text-type}$? (For example, by definition $\mathsf{is\text-}(-1)\mathsf{\text-type}\ A$ is $$ \Pi(x\ y : A)\ \Sigma(p : x =_A y)\ \Pi(q : x =_A y)\ p = q $$ which says more about the structure of $x =_A y$ than being inhabited and therefore looks more informative than $\mathsf{isProp}\ A$.)
Both questions can be answered by the following lemma saying that the equality types on a mere proposition are contractible:
\begin{equation} \Pi(A : \mathcal U)\ \mathsf{isProp}\ A \to \Pi(x\ y : A)\ \mathsf{isContr}\ (x =_A y) \tag{$*$} \label{lem:roof} \end{equation}
Given the above lemma and the easily provable fact
$$ \Pi(A : \mathcal U)\ \mathsf{isContr}\ A \to \mathsf{isProp}\ A $$
we can readily give answers to the two questions:
- the equality types on a contractible type are also contractible, that is, ‘$(-3)$-types’ are actually just $(-2)$-types, and
- $\mathsf{isSet}$ and $\mathsf{isProp}$ imply $\mathsf{is\text-}0\mathsf{\text-type}$ and $\mathsf{is\text-}(-1)\mathsf{\text-type}$ respectively (and the opposite implications are immediate).
Note that the first answer in general proves an important theorem that $n$-types are also $(n+1)$-types: if we picture the equality types $x =_A y$ on a type $A$ as one level above $A$, then the first answer tells us that we can create a $(-2)$-level above a $(-2)$-type, pushing the latter down and making it a $(-1)$-type (since its equality types are $(-2)$-types), and this pushing works inductively for any $n$-type. Or probably more accurately: every type induces an infinitely tall tower of equality types (with the original type as the ground floor); if all the floors above a certain level have the trivial $(-2)$-structure, then the type at the ground floor is an $n$-type, and we can start counting from any $(-2)$-structured floor downwards to determine $n$.
The proof of the lemma (\ref{lem:roof}) may appear slightly magical to people like me who are not used to working with equality proofs (or paths, which can help to bring out some homotopical intuition). The key is to see that a function of type $\mathsf{isProp}\ A$ doesn’t just map any $x$, $y : A$ to an equality proof in $x =_A y$, but also relates the resulting equality proofs by some equations because all functions preserve equality, meaning that we can automatically get an equality between output equality proofs from an equality between input elements of $A$. More precisely, given $A : \mathcal U$ and $f : \mathsf{isProp}\ A$, for any $x : A$ the partially applied function $f\ x : \Pi(y : A)\ x =_A y$ maps any equality proof $p : z =_A y$ between two possible inputs $z$, $y : A$ to one between the outputs $f\ x\ z : x =_A z$ and $f\ x\ y : x =_A y$. The two outputs don’t have the same type, however, so we need to transport $f\ x\ z : x =_A z$ to $p_*(f\ x\ z) : x =_A y$ before we can say that the two outputs are equal. The transportation $p_* : x =_A z \to x =_A y$ is between equality types, and all it does is concatenate $p$ to its input (by transitivity $(\cdot) : a = b \to b = c \to a = c$), so $p_*(f\ x\ z) = f\ x\ z \cdot p$. What we have constructed so far is
$$ \Pi(x\ z\ y : A)\ \Pi(p : z =_A y)\ f\ x\ z \cdot p = f\ x\ y $$
which relates any $f\ x\ z$ and $f\ x\ y$. Homotopically, we might think of this equality as symbolising the picture where $f\ x\ z$ can be continuously deformed to $f\ x\ y$ along any path $p : z =_A y$. Next we concatenate $(f\ x\ z)^{-1}$ (where $(^{-1}) : a = b \to b = a$ is symmetry of equality or path inversion) to both sides of the equation, cancelling out the $f\ x\ z$ on the left:
$$ \Pi(x\ z\ y : A)\ \Pi(p : z =_A y)\ p = (f\ x\ z)^{-1} \cdot f\ x\ y $$
This changes the orientation of the homotopy, which I find intuitive but am not absolutely certain about; fortunately, though, this step is backed by the path calculation techniques developed in Chapter 2 of the HoTT book (and demonstrates that those techniques are worth learning). Finally we ‘pull’ $z$ to make it coincide with $x$ (that is, we substitute $x$ for $z$) and obtain
$$ \Pi(x\ y : A)\ \Pi(p : x =_A y)\ p = (f\ x\ x)^{-1} \cdot f\ x\ y $$
which is the same as saying that every $x =_A y$ is contractible with $(f\ x\ x)^{-1} \cdot f\ x\ y$ as the center.
Follow-up: 0012 (More path calculations)
