nLab HoTT book real number

Idea

A construction (UFP13, Sec. 11.3) of the type of real numbers in homotopy type theory as a higher inductive-inductive type.

As opposed to the “naive” quotient type of regular Cauchy sequences of rational numbers (i.e. the quotient type of the setoid/Bishop set by which the Cauchy real numbers are traditionally modeled in constructive analysis) this higher inductive-inductive type is sequentially modulated Cauchy complete.

Notice that this crucial property of the real number fails for other constructions:

• The quotient type of regular Cauchy sequences of rational numbers is Cauchy complete only assuming that any sequence of its terms has a lift to a sequence of representing Cauchy sequences, which requires an extra axiom of countable choice (and is the reason why traditional Bishop-constructive analysis does not pass to the quotient but stays with the setoid/Bishop set).

• The modulated Cauchy real numbers are not sequentially modulated Cauchy complete either, in constructive mathematics.

Definition

As a sequentially modulated Cauchy complete Archimedean ordered field

Let $K$ be an Archimedean ordered field. $K$ is sequentially modulated Cauchy complete if every Cauchy sequence in $K$ with a modulus of convergence converges. The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of sequentially modulated Cauchy complete Archimedean fields.

More abstractly, let $\mathrm{ArchiFields}$ be the category of Archimedean ordered fields and Archimedean ordered field homomorphisms, and let $F:\mathrm{ArchiFields} \to \mathrm{ArchiFields}$ be the endofunction which takes an Archimedean ordered field $K$ to the Archimedean ordered field $F(K)$ which is the quotient set of the set of Cauchy sequences in $K$ with a modulus of convergence. $K$ is sequentially modulated Cauchy complete if there is an isomorphism $K \cong F(K)$, and the HoTT book real numbers $\mathbb{R}_H$ is the initial Archimedean ordered field with an isomorphism $\mathbb{R}_H \cong F(\mathbb{R}_H)$.

As a Cauchy structure

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

As a higher inductive-inductive type

As a higher inductive-inductive type:

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

$$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$$

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

$$a:\mathbb{R}_H, b:\mathbb{R}_H \vdash eq_{\mathbb{R}_H}(a, b): \left( \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \right) \to (a =_{\mathbb{R}_H} b)$$

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{R}_H, b:\mathbb{R}_H, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)$$

Properties

The analytic functions, such as the exponential function, the sine function, and the cosine function are well defined in the HoTT book real numbers, since all modulated Cauchy sequences converge in the HoTT book real numbers.

See also

• higher inductive-inductive type

• Cauchy real numbers

• generalized Cauchy real numbers

• premetric space

References

• Univalent Foundations Project, Section 11.3 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

Survey and review:

• Andrej Bauer, The real numbers in homotopy type theory, talk at Computability and Complexity in Analysis, Faro (2016) [pdf, pdf]

• Auke Booij, Analysis in Univalent Type Theory (2020) [etheses:10411, pdf, pdf]