11.3.1 Construction of Cauchy reals

The construction of the Cauchy reals ${ℝ}_{𝖼}$ as a higher inductive type is a bit more subtle than that of the free algebraic structures considered in sec: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 $ϵ$” for any $ϵ:{\mathbb{Q}}_{+}$.This can be represented by a family of binary relations, which we will denote ${\sim }_{ϵ}:{ℝ}_{𝖼}\to {ℝ}_{𝖼}\to \mathrm{𝖯𝗋𝗈𝗉}$.The intended meaning of $x{\sim }_{ϵ}y$ is , but since we do not have notions of subtraction, absolute value, or inequality available yet (we are only just defining ${ℝ}_{𝖼}$, after all), we will have to define these relations ${\sim }_{ϵ}$ at the same time as we define ${ℝ}_{𝖼}$ itself.And since ${\sim }_{ϵ}$ is a type family indexed by two copies of ${ℝ}_{𝖼}$, we cannot do this with an ordinary mutual (higher) inductive definition; instead we have to use a higher inductive-inductive definition.

Recall from sec: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 ${ℝ}_{𝖼}$ and ${\sim }_{ϵ}$ will make the idea transparent.

Remark 11.3.1.

We might also consider a higher inductive-recursive definition, in which ${\mathrm{\sim }}_{ϵ}$ is defined using the recursion principle of ${\mathrm{R}}_{\mathrm{c}}$, simultaneously with the inductive definition of ${\mathrm{R}}_{\mathrm{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 sec:RD-cauchy-complete, we will work with Cauchy approximations (defn: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 ${\mathrm{R}}_{\mathrm{c}}$ and the relation $\mathrm{\sim }\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}\mathrm{\times }{\mathrm{R}}_{\mathrm{c}}\mathrm{\times }{\mathrm{R}}_{\mathrm{c}}\mathrm{\to }\mathrm{U}$ be the following higher inductive-inductive type family.The type ${\mathrm{R}}_{\mathrm{c}}$ of Cauchy realsis generated by the following constructors:

• rational points:for any $q:\mathbb{Q}$ there is a real $\mathrm{𝗋𝖺𝗍}(q)$.

• limit points:for any $x:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$ such that

  $$\forall (\delta ,ϵ:{\mathbb{Q}}_{+}).x_{\delta }{\sim }_{\delta +ϵ}{x}_{ϵ}$$(11.3.2)

  there is a point $\mathrm{𝗅𝗂𝗆}(x):{ℝ}_{𝖼}$. We call $x$ a Cauchy approximation.

• paths:for $u,v:{ℝ}_{𝖼}$ such that

  $$\forall (ϵ:{\mathbb{Q}}_{+}).u{\sim }_{ϵ}v$$(11.3.3)

  then there is a path ${\mathrm{𝖾𝗊}}_{{ℝ}_{𝖼}}(u,v):u{=}_{{ℝ}_{𝖼}}v$.

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

• for any $q,r,ϵ$, if , then $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ}\mathrm{𝗋𝖺𝗍}(r)$,

• for any $q,y,ϵ,\delta$, if $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ-\delta }{y}_{\delta }$, then $\mathrm{𝗋𝖺𝗍}(q){\sim }_{ϵ}\mathrm{𝗅𝗂𝗆}(y)$,

• for any $x,r,ϵ,\delta$, if $x_{\delta }{\sim }_{ϵ-\delta }\mathrm{𝗋𝖺𝗍}(r)$, then $\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ}\mathrm{𝗋𝖺𝗍}(r)$,

• for any $x,y,ϵ,\delta ,\eta$, if $x_{\delta }{\sim }_{ϵ-\delta -\eta }{y}_{\eta }$, then $\mathrm{𝗅𝗂𝗆}(x){\sim }_{ϵ}\mathrm{𝗅𝗂𝗆}(y)$,

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

The first constructor of ${ℝ}_{𝖼}$ 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 $\mathrm{\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 $ϵ$-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 $\mathrm{𝗅𝗂𝗆}(x)$.

We remind ourselves of proof-relevance: a real number obtained from $\mathrm{𝗅𝗂𝗆}$ is represented notjust by a Cauchy approximation $x$, but also a proof $p$ of (11.3.2), so weshould technically have written $\mathrm{𝗅𝗂𝗆}(x,p)$ instead of just $\mathrm{𝗅𝗂𝗆}(x)$.A similar observation also applies to ${\mathrm{𝖾𝗊}}_{{ℝ}_{𝖼}}$ and (11.3.3), but we shall write just${\mathrm{𝖾𝗊}}_{{ℝ}_{𝖼}}:u=v$ instead of ${\mathrm{𝖾𝗊}}_{{ℝ}_{𝖼}}(u,v,p):u=v$. These abuses of notation aremitigated by the fact that we are omitting mere propositions and information that isreadily guessed.Likewise, the last constructor of ${\sim }_{ϵ}$ justifies our leaving the other four nameless.

We are immediately able to populate ${ℝ}_{𝖼}$ 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 itsmodulus of convergence. Then $\mathrm{𝗋𝖺𝗍}\circ x\circ M:{\mathbb{Q}}_{+}\to {ℝ}_{𝖼}$ is a Cauchyapproximation, using the first constructor of $\mathrm{\sim }$ to produce the necessary witness.Thus, $\mathrm{𝗅𝗂𝗆}(\mathrm{𝗋𝖺𝗍}\circ x\circ m)$ is a real number. Various famousreal numbers $\sqrt{2}$, $\pi$, $e$, … are all limits of such Cauchy sequences ofrationals.