nLab HoTT book real number

Redirected from "HoTT book real numbers".
Contents

Context

Analysis

Constructivism, Realizability, Computability

Contents

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:

Definition

As a sequentially modulated Cauchy complete Archimedean ordered field

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

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

As a Cauchy structure

The set of HoTT book real numbers H\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

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

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

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

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

  • a dependent family of terms

a: H,b: Heq H(a,b):( ϵ: +(a ϵb))(a= Hb)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:,b:,ϵ: +μ ,(a,b,ϵ):(|ab|<ϵ)(inj(a) ϵinj(b))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:,b:C( H),ϵ: +,η: +μ ,C( H)(a,b,ϵ,η):(inj(a) ϵb η)(inj(a) ϵ+ηlim(b))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( H),b:,δ: +,ϵ: +μ C( H),(a,b,δ,ϵ):(a δ ϵinj(b))(lim(a) δ+ϵinj(b))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( H),b:C( H),δ: +,ϵ: +,η: +μ C( H),C( H)(a,b,δ,ϵ,η):(a δ ϵb η)(lim(a) δ+ϵ+ηlim(b))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: H,b: H,ϵ: +π(a,b,ϵ):isProp(a ϵb)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

References

Survey and review:

Last revised on February 2, 2024 at 02:44:44. See the history of this page for a list of all contributions to it.