Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

Let $F$ be an Archimedean ordered field and let

be the positive elements in $F$. $F$ is sequentially Cauchy complete if every Cauchy sequence in $F$ converges:

The set of HoTT book real numbers $\mathbb{R}_H$ is the initial sequentially Cauchy complete? Archimedean ordered field.

The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms.

In homotopy type theory

The HoTT book real numbers $\mathbb{R}_H$ are a homotopy initial Cauchy structure, i.e. a Cauchy structure such that for every other Cauchy structure $S$, the type of Cauchy structure homomorphisms with domain $\mathbb{R}_H$ and codomain $S$ is contractible.

As a higher inductive-inductive type

Let $\mathbb{Q}$ be the rational numbers and let

be the positive rational numbers. The HoTT book real numbers $\mathbb{R}_H$ are inductively generated by the following:

• a function $inj: \mathbb{Q} \to \mathbb{R}_H$

• a function $lim: C(\mathbb{R}_H) \to \mathbb{R}_H$, where $C(\mathbb{R}_H)$ is the type of Cauchy approximations in $\mathbb{R}_H$.

• a dependent family of terms

and the premetric type family $\sim$ is simultaneously inductively generated by the following:

• a dependent family of terms

  $$a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, \mathbb{Q}}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))$$

• a dependent family of terms

  $$a:\mathbb{Q}, b:C(\mathbb{R}_H), \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, C(\mathbb{R}_H)}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))$$

• a dependent family of terms

  $$a:C(\mathbb{R}_H), b:\mathbb{Q}, \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), \mathbb{Q}}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))$$

• a dependent family of terms

  $$a:C(\mathbb{R}_H), b:C(\mathbb{R}_H), \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), C(\mathbb{R}_H)}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))$$

• a dependent family of terms

  $$a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)$$

See also

• Cauchy real numbers
• generalized Cauchy real numbers
• Cauchy real numbers (disambiguation)
• premetric space

References

• Auke B. Booij, Analysis in univalent type theory (pdf)
• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)