11.3.1 Construction of Cauchy reals

The construction of the Cauchy reals $\mathbb{R}_{\mathsf{c}}$ as a higher inductive type is a bit more subtle than that of the free algebraic structures considered in \autorefsec:free-algebras. We intend to include a “take the limit” constructor whose input is a Cauchy sequence of reals, but the notion of “Cauchy sequence of reals” depends on having some way to measure the “distance” between real numbers. In general, of course, the distance between two real numbers will be another real number, leading to a potentially problematic circularity.

However, what we actually need for the notion of Cauchy sequence of reals is not the general notion of “distance”, but a way to say that “the distance between two real numbers is less than $\epsilon$” for any $\epsilon:\mathbb{Q}_{+}$. This can be represented by a family of binary relations, which we will denote $\mathord{\sim_{\epsilon}}:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}\to% \mathsf{Prop}$. The intended meaning of $x\sim_{\epsilon}y$ is $|x-y|<\epsilon$, but since we do not have notions of subtraction, absolute value, or inequality available yet (we are only just defining $\mathbb{R}_{\mathsf{c}}$, after all), we will have to define these relations $\sim_{\epsilon}$ at the same time as we define $\mathbb{R}_{\mathsf{c}}$ itself. And since $\sim_{\epsilon}$ is a type family indexed by two copies of $\mathbb{R}_{\mathsf{c}}$, we cannot do this with an ordinary mutual (higher) inductive definition; instead we have to use a higher inductive-inductive definition.

Recall from \autorefsec:generalizations that the ordinary notion of inductive-inductive definition allows us to define a type and a type family indexed by it by simultaneous induction. Of course, the “higher” version of this allows both the type and the family to have path constructors as well as point constructors. We will not attempt to formulate any general theory of higher inductive-inductive definitions, but hopefully the description we will give of $\mathbb{R}_{\mathsf{c}}$ and $\sim_{\epsilon}$ will make the idea transparent.

Remark 11.3.1.

We might also consider a higher inductive-recursive definition, in which $\sim_{\epsilon}$ is defined using the recursion principle of $\mathbb{R}_{\mathsf{c}}$, simultaneously with the inductive definition of $\mathbb{R}_{\mathsf{c}}$. We choose the inductive-inductive route instead for two reasons. Firstly, higher inductive-recursive definitions seem to be more difficult to justify in homotopical semantics. Secondly, and more importantly, the inductive-inductive definition yields a more powerful induction principle, which we will need in order to develop even the basic theory of Cauchy reals.

Finally, as we did for the discussion of Cauchy completeness of the Dedekind reals in \autorefsec:RD-cauchy-complete, we will work with Cauchy approximations (\autorefdefn:cauchy-approximation) instead of Cauchy sequences. Of course, our Cauchy approximations will now consist of Cauchy reals, rather than Dedekind reals or rational numbers.

Definition 11.3.2.

Let $\mathbb{R}_{\mathsf{c}}$ and the relation $\mathord{\sim}:\mathbb{Q}_{+}\times\mathbb{R}_{\mathsf{c}}\times\mathbb{R}_{% \mathsf{c}}\to\mathcal{U}$ be the following higher inductive-inductive type family. The type $\mathbb{R}_{\mathsf{c}}$ of Cauchy reals is generated by the following constructors:

• rational points: for any $q:\mathbb{Q}$ there is a real $\mathsf{rat}(q)$.

• limit points: for any $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}$ such that

 $\forall(\delta,\epsilon:\mathbb{Q}_{+}).\,x_{\delta}\sim_{\delta+\epsilon}x_{\epsilon}$ (11.3.2)

there is a point $\mathsf{lim}(x):\mathbb{R}_{\mathsf{c}}$. We call $x$ a Cauchy approximation.

• paths: for $u,v:\mathbb{R}_{\mathsf{c}}$ such that

 $\forall(\epsilon:\mathbb{Q}_{+}).\,u\sim_{\epsilon}v$ (11.3.3)

then there is a path $\mathsf{eq}_{\mathbb{R}_{\mathsf{c}}}(u,v):u=_{\mathbb{R}_{\mathsf{c}}}v$.

Simultaneously, the type family $\mathord{\sim}:\mathbb{R}_{\mathsf{c}}\to\mathbb{R}_{\mathsf{c}}\to\mathbb{Q}_% {+}\to\mathcal{U}$ is generated by the following constructors. Here $q$ and $r$ denote rational numbers; $\delta$, $\epsilon$, and $\eta$ denote positive rationals; $u$ and $v$ denote Cauchy reals; and $x$ and $y$ denote Cauchy approximations:

• for any $q,r,\epsilon$, if $-\epsilon, then $\mathsf{rat}(q)\sim_{\epsilon}\mathsf{rat}(r)$,

• for any $q,y,\epsilon,\delta$, if $\mathsf{rat}(q)\sim_{\epsilon-\delta}y_{\delta}$, then $\mathsf{rat}(q)\sim_{\epsilon}\mathsf{lim}(y)$,

• for any $x,r,\epsilon,\delta$, if $x_{\delta}\sim_{\epsilon-\delta}\mathsf{rat}(r)$, then $\mathsf{lim}(x)\sim_{\epsilon}\mathsf{rat}(r)$,

• for any $x,y,\epsilon,\delta,\eta$, if $x_{\delta}\sim_{\epsilon-\delta-\eta}y_{\eta}$, then $\mathsf{lim}(x)\sim_{\epsilon}\mathsf{lim}(y)$,

• for any $u,v,\epsilon$, if $\xi,\zeta:u\sim_{\epsilon}v$, then $\xi=\zeta$ (propositional truncation).

The first constructor of $\mathbb{R}_{\mathsf{c}}$ says that any rational number can be regarded as a real number. The second says that from any Cauchy approximation to a real number, we can obtain a new real number called its “limit”. And the third expresses the idea that if two Cauchy approximations coincide, then their limits are equal.

The first four constructors of $\mathord{\sim}$ specify when two rational numbers are close, when a rational is close to a limit, and when two limits are close. In the case of two rational numbers, this is just the usual notion of $\epsilon$-closeness for rational numbers, whereas the other cases can be derived by noting that each approximant $x_{\delta}$ is supposed to be within $\delta$ of the limit $\mathsf{lim}(x)$.

We remind ourselves of proof-relevance: a real number obtained from $\mathsf{lim}$ is represented not just by a Cauchy approximation $x$, but also a proof $p$ of (11.3.2), so we should technically have written $\mathsf{lim}(x,p)$ instead of just $\mathsf{lim}(x)$. A similar observation also applies to $\mathsf{eq}_{\mathbb{R}_{\mathsf{c}}}$ and (11.3.3), but we shall write just $\mathsf{eq}_{\mathbb{R}_{\mathsf{c}}}:u=v$ instead of $\mathsf{eq}_{\mathbb{R}_{\mathsf{c}}}(u,v,p):u=v$. These abuses of notation are mitigated by the fact that we are omitting mere propositions and information that is readily guessed. Likewise, the last constructor of $\mathord{\sim_{\epsilon}}$ justifies our leaving the other four nameless.

We are immediately able to populate $\mathbb{R}_{\mathsf{c}}$ with many real numbers. For suppose $x:\mathbb{N}\to\mathbb{Q}$ is a traditional Cauchy sequence of rational numbers, and let $M:\mathbb{Q}_{+}\to\mathbb{N}$ be its modulus of convergence. Then $\mathsf{rat}\circ x\circ M:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{c}}$ is a Cauchy approximation, using the first constructor of $\mathord{\sim}$ to produce the necessary witness. Thus, $\mathsf{lim}(\mathsf{rat}\circ x\circ m)$ is a real number. Various famous real numbers $\sqrt{2}$, $\pi$, $e$, … are all limits of such Cauchy sequences of rationals.

Title 11.3.1 Construction of Cauchy reals
\metatable