NOTE: If you come across this please know that it is a WIP. There is stuff in here that is wrong because I was still learning it.
Part I: Foundations
Introduction
If some framework for reasoning about mathematical objects posits that it exists as a foundation of mathematics, what good would it be if something as critical as the real numbers couldn’t be reasoned about, much less even constructed, in that framework? When Homotopy Type Theory states that it is such a framework, we must measure such a postulation against the same requirements for any other foundations of mathematics. For HoTT to be “foundational” we’re going to need to be able to reason about the real numbers through it.
The goal of this document is to first build up an intuition for the requisite pieces of understanding the reals in HoTT. We begin by giving a whirlwind introduction to Homotopy Type Theory and the mathematical toolbox it provides us. Next, we’ll explore the mathematical structure we need to construct the real numbers, namely Cauchy Sequences. And finally, I’ll elucidate how we can use the tools provided to us by HoTT to construct, and then reason about the reals.
Homotopy Type Theory
Homotopy Type Theory is many things, and its existence has many elegant applications, but for the purpose at hand, I’m going to cover just the parts which we need to begin to think about the real numbers. To begin, why Homotopy Type Theory?
2.1 Homotopies
In topology, a homotopy is a mathematical object which bends one function into another. More formally:
Given two functions which map between spaces \(X\) and \(Y\):
\[ f,\ g : X \rightarrow Y \]
A homotopy \(H\) is a functionWhere \([0, 1]\) denotes the real interval, the continuous
and transfinite sequence of the real numbers between \(0\) and
\(1\).
:
\[ H : [0, 1] \times X \rightarrow Y \]
Such that
\[ H(0, X) = f \]
And
\[ H(1, X) = g \]
The intuition here is that, in a sense, our homotopy \(H\) is a functions between functions.
We can take this notion a step further too, and use a homotopy as an equivalence between two topological spaces:
Given two functions:
\[ \begin{align*} &f : X \rightarrow Y \\ &g : Y \rightarrow X \end{align*} \]
We can use our homotopy to say, “if the composition of \(f\) and \(g\) is homotopic to the function \(Id_x\), then the spaces \(X\) and \(Y\) are homotopy equivalent.”
\[ \begin{align*} H(0, X) &= Id_x \\ H(1, X) &= g \circ f \end{align*} \]
In topology, it is reasonable to say that a homotopy equivalence is an isomorphism. That is, an identity preserving map between our two spaces \(X\) and \(Y\).
There are two take-aways that I want to make sure we don’t abscond from this section without taking them with us.
- A homotopy can, more generally, be thought of as a function between functions.
- A homotopy can be seen as an isomorphism in the mathematical field of topology, because it is identity preserving.
Now, this notion of functions, their inverses, and functions between functions can be generalized in category theory in an object called a groupoid.
Groupoids
In the land of category theory, a groupoid is an object in which the usual axioms hold—namely composition, the associativity of composition, an identity morphism, &c. However, in a groupoid, all morphisms also have an inverse:
\[ \xymatrix{ A \ar[r]_f & B \ar@{.>}@/_1pc/[l]_{f^{-1}} \ar[d]_g \\ & C \ar@{.>}@/_1pc/[u]_{g^{-1}} } \]
In the same way we think of homotopy equivalence as an isomorphism in topology, we can also think of these morphisms and their inverses as isomorphisms. Given the diagram above, the composition:
\[ f^{-1} \circ f \simeq Id_A \]
is identity preserving. Through this lens, we can start to think as a groupoid as a category whose morphisms are equivalences.
\(\infty\)-Groupoids
Like our homotopy was a function between functions, an \(\infty\)-groupoid is governed by the precept that not only can we have morphisms between objects, but also we can have morphisms between morphisms, and morphisms between morphisms between morphisms, ad infinitum. However, another way to think of this, given what we’ve stated before about the composition of a morphism and its inverse as an isomorphism, this would correspond to stating isomorphisms of isomorphisms.
For example:
If we have the following diagram:
\[ \xymatrix{ A \ar@/^/[r]^f \ar@/_/[r]_g & B \ar@{.>}@/_2pc/[l]_{f^{-1}} \ar@{.>}@/^2pc/[l]^{g^{-1}} } \]
Another way we could state this is like so:
\[ \begin{align*} p &: A \simeq B \\ p &= f^{-1} \circ f \\ \\ \end{align*} \]
and
\[ \begin{align*} q &: A \simeq B \\ q &= g^{-1} \circ g \end{align*} \]
Now, with our higher groupoid structure, we can say things like:
\[ p \simeq q \]
The Univalence Axiom
Secondarily to this notion of morphisms of morphisms, concomitant to HoTT’s conception came the idea of univalence. The univalence axiom states the following:
\[ (A \simeq B) = (A = B) \]
Before we can cover the implications of such an axiom, we need first to cover a few prerequisites.
Intensional vs Extensional Type Theories
In an intensional type theory, the notion of equality is definitional, not one that can be expressed as a proposition. This concept of intensionality is how Per Martin-Löf originally conceived of type theory. In an intensional type theory, for two objects to be equivalent, they must, by definition, be the same thing. While Martin-Löf stated that intensional equality was an equality of meaning, i.e. synonymy, its implications are such that two objects must be syntactically equivalent.
However, in an extensional type theory, equivalences can be expressed as simply another type—a proposition of equality.
This would allow one to, say, state that in our type of topological spaces, a homotopy equivalence is an equivalence for this type, and to prove two spaces’ equivalence, we merely need to define an inhabitant of that type.
This idea of being able to define our own equivalences can plausibly be seen as a weakening of equality, as we’re now providing a way in which to arbitrarily state equivalences for our types. But wait!
Univalence as an Extensional to Intensional Bridge
Lets look again at the definition of the Univalence Axiom:
\[ (A \simeq B) = (A = B) \]
What this axiom is stating is this: If two objects are isomorphic, then they are equivalent.
This axiom elides the need for an explicitly extensional type theory, as those propositional isomorphisms we’ve defined for our types like the type of topological spaces, are in fact, universally, equivalences. Univalence universalizes domain specific isomorphisms stating that they are all equivalent to an equality. The implication of this axiom is then, a type theory which has propositional equalities can again be seen as intensional as the definitional-style of equality is possible by axiomatizing isomorphisms from specific types to be universal equalities.
Higher Inductive Types
A higher inductive type is the generalization of the idea that, along with a type’s definition and the definition of its constructors, we may also define its equivalences. Something like this:
\[ \begin{align*} \mathbb{N} &: Type \\ zero &: \mathbb{N} \\ succ &: \mathbb{N} \rightarrow \mathbb{N} \\ \equiv_{\mathbb{N}}\ &: \{n : \mathbb{N}\} \rightarrow n \rightarrow n \rightarrow Type \\ \end{align*} \]
This has a lot of overlap with what we’ve discussed thus far, i.e. extensional equality, & c., but when we talk about Higher Inductive Types, rather than merely considering the equality, we want to think about what happens when we use one of these equalities.
H-Levels
In HoTT, as we’ve discussed previously, we are given the ability to define functions between functions, and equality is simply a function. That ladder of equalities has a name: H-Levels. When we’re working with a type which requires no higher equalities, we say that type is a quotient type. In the following section, we’ll use quotient types to try and build an intuition for what the application of one of these equalities results in.
Quotient Types
We’ll use quotient types’ categorical semantics to demonstrate the application of one of these equalities.
To begin, lets say we have some category \(D\), in which we have the following diagram:
\[ \xymatrix{ A_1 \ar[r] \ar[d] & A_2 \ar[d] \\ B_1 \ar[r] \ar[d] & B_2 \ar[d] \\ C_1 \ar[r] & C_2 \\ } \]
And an equivalence, \(E\), applicable to objects in \(D\). We can then define a functor \(F : D \rightarrow D/E\) which applies that equivalence and maps a category to its skeleton:
\[ \xymatrix{ A \ar[d] \\ B \ar[d] \\ C } \]
What we’ve done here is divide our category into its equivalence classes, precipitated by \(E\).
At this point, we covered homotopies as our foundational structure, and then studied that structure and learned about many interesting things which shake out of homotopies when we think hard enough about them. These mathematical tools that we’ve explicated thus far compose the logical, categorical, and type theoretical desiderata for thinking about the real numbers in Homotopy Type Theory. We’ll use these tools to construct the mathematical objects discussed in the following section, which, when put together give us a construction of the real numbers.
However, before we can do that, we first need to have an intuition for this metod of construction.
Part II: Constructing the Real Numbers
We’ve said that we intend construct the real numbers. What I mean when I say construct, is that we will build them, like a house from its materials, from other types which, when used together, can realize the real numbers. The following sections will cover those materials and how we fasten them together in order to produce the reals.
Cauchy
As presented in the book, there exists two ways in which to construct the real numbers, heretofore denoted \(\mathbb{R}\). One of those ways is through Dedekind cuts which we will not elucidate in this document. The other is the Cauchy real numbers, or \(\mathbb{R}_c\). This section will focus on this construction.
Cauchy Sequences
A Cauchy Sequence is a sequence of points, or elements of a set, which converge on some value. For example, if we were to choose from the set of the rationals the sequence \(\{3, 3.14, 3.141, 3.1415, 3.14159, …\}\), we could say that, over time, it converges on famous number which we know to be irrational: \(\pi\). This number to which our sequence converges is called its limit.
Stated more formally, a Cauchy sequence is a sequence:
\[ \mathcal{C} := \{x_1, x_2, x_3, …, x_n \} \]
Such that
\[ \forall i.\ \exists \epsilon.\ |x_i - x_{i+1}| < \epsilon \]
Our use of \(\pi\) was no accident. It turns out, Cauchy’s sequences can be used to construct real numbers like it! This is accomplished by beginning with the rationals, or \(\mathbb{Q}\), and then completing them, or filling in the gaps between them, by employing sequences of \(\mathbb{Q}\) which converge on some real number—a number which can be enumerated by —up to some \(\epsilon\) precision.
Formalizing \(\mathbb{R}\)
If through Cauchy sequences we con construct \(\mathbb{R}\), then we can simply formalize their notion in HoTT. The first way we’d likely go about this is through quotient types as described above:
\[ \mathbb{R}_c := \mathbb{Q}_c / \approx \]
Where \(\approx\) is defined through our Cauchy sequence definition:
\[ \approx_{\epsilon} : \mathbb{R} \rightarrow \mathbb{R} \rightarrow \text{Prop} \]
I.e. the relationship \(\approx\) holds for two \(r \in \mathbb{R}\)’s up to some \(\epsilon\) precision.
The implication of this is of course that any \(r \in \mathbb{R}\) can be defined as the Cauchy sequences which approximate it. Unfortunately, this approach requires the axiom of (countable) choice. AoC provides an axiomatic way in which to arbitrarily “choose” some set out of a set of set, which is exactly what we’d have to do to with our set of sequences. While they approximate the same real, even up to the same precision, we must still select one in particular in order to deploy it as our construction of that real number it approximates. We’d like to instead be able to construct \(\mathbb{R}\) without employing such an axiom.
The Cauchy Reals in HoTT
In order to avoid the AoC, the onus of selection is instead pushed off to the caller, so to speak. This is through a constructor which produces a Cauchy approximation.
\[ \text{CApprx} : \Sigma_{x : \mathbb{Q}_+ \rightarrow A}\ \forall \epsilon\ \delta .\ x_{\epsilon} \approx_{\epsilon + \delta} x_{\delta} \]
And given an \(a : \text{CApprox}\) we take its limit: \(lim : \text{CApprx} \rightarrow \mathbb{R}\) to produce our real number.