**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.