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

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

• The Cauchy real numbers, defined as the quotient type of regular Cauchy sequences of rational numbers, is sequentially complete only assuming that any sequence of its terms has a lift to a sequence of representing regular 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).

Definition

As a sequentially complete Archimedean ordered field

Let $K$ be an Archimedean ordered field. $K$ is sequentially complete if every regular Cauchy sequence in $K$ converges. The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of sequentially 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 regular Cauchy sequences in $K$. $K$ is sequentially 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 rational 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 regular Cauchy sequences converge in the HoTT book real numbers.

See also

• higher inductive-inductive type

• Cauchy real numbers

• generalized Cauchy real numbers

• premetric space

• Escardo-Simpson real numbers

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]