nLab HoTT book real number

Contents

Context

Analysis

Constructivism, Realizability, Computability

Contents

Idea

A notion of real numbers that is sequentially modulated Cauchy complete, because the modulated Cauchy real numbers are not sequentially modulated Cauchy complete in constructive mathematics

Definition

As a sequentially Cauchy complete Archimedean ordered pointed halving group

Note: everything in this particular section was copied from the Sandbox of the HoTT wiki and is likely to be original research.

The HoTT book real numbers is the (homotopy)-initial sequentially Cauchy complete Archimedean ordered pointed halving group. There should be a corresponding definition as a higher inductive-inductive type, but that still has to be worked out.

We define a sequentially Cauchy complete Archimedean ordered pointed halving group below as follows:

Pointed abelian groups

A pointed abelian group is a set AA with an element 1:A1:A called one and a binary operation ()():A×AA(-)-(-):A \times A \to A called subtraction such that

  • for all elements a:Aa:A, aa=11a - a = 1 - 1

  • for all elements a:Aa:A, (11)((11)a)=a(1 - 1) - ((1 - 1) - a) = a

  • for all elements a:Aa:A and b:Ab:A, a((11)b)=b((11)a)a - ((1 - 1) - b) = b - ((1 - 1) - a)

  • for all elements a:Aa:A, b:Ab:A, and c:Ac:A, a(bc)=(a((11)c))ba - (b - c) = (a - ((1 - 1) - c)) - b

00 is defined as 111 - 1, a-a is defined as 0a0 - a, and a+ba + b is defined as a(b)a - (-b). It is left to the reader as an exercise to prove from the given axioms and definitions that (A,0,+,,1)(A,0,+,-,1) is an abelian group with an extra point 11.

Pointed halving groups

A pointed halving group is a pointed abelian group G with a function ()/2:GG(-)/2:G \to G called halving or dividing by two such that for all elements g:Gg:G, g/2=gg/2g/2 = g - g/2.

Strictly ordered pointed halving groups

A pointed halving group RR is a strictly ordered pointed abelian group if it comes with a type family <\lt such that

  • for all elements a:Ra:R and b:Rb:R, a<ba \lt b is a proposition
  • for all elements a:Ra:R, a<aa \lt a is false
  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, if a<ca \lt c, then a<ba \lt b or b<cb \lt c
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b is false and b<ab \lt a is false, then a=ba = b
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b, then b<ab \lt a is false.
  • 11<11 - 1 \lt 1
  • for all elements a:Ra:R and b:Rb:R, if 11<a1 - 1 \lt a and 11<b1 - 1 \lt b, then (11)<a((11)b)(1 - 1) \lt a - ((1 - 1) - b)

The homotopy initial strictly ordered pointed halving group is the dyadic rational numbers 𝔻\mathbb{D}.

Archimedean ordered pointed halving groups

A strictly ordered pointed halving group AA is an Archimedean ordered pointed halving group if for all elements a:Aa:A and b:Ab:A, if a<ba \lt b, then there merely exists a dyadic rational number d:𝔻d:\mathbb{D} such that a<h(d)a \lt h(d) and h(d)<bh(d) \lt b.

Sequentially Cauchy complete Archimedean ordered pointed halving groups

Let

𝔻 + a:𝔻0<a\mathbb{D}_{+} \coloneqq \sum_{a:\mathbb{D}} 0 \lt a

be the positive dyadic rational numbers.

A sequence in AA is a function x:Ax:\mathbb{N} \to A.

A sequence x:Ax:\mathbb{N} \to A is a Cauchy sequence if for all positive dyadic rational numbers ϵ:𝔻 +\epsilon:\mathbb{D}_{+}, there merely exists a natural number N:N:\mathbb{N} such that for all natural numbers i:i:\mathbb{N} and j:j:\mathbb{N} such that NiN \leq i and NjN \leq j, x ix j<ϵx_i - x_j \lt \epsilon or x jx i<ϵx_j - x_i \lt \epsilon.

An element l:Al:A is said to be a limit of the sequence x:Ax:\mathbb{N} \to A if for all positive dyadic rational numbers ϵ:𝔻 +\epsilon:\mathbb{D}_{+}, there merely exists a natural number N:N:\mathbb{N} such that for all natural numbers i:i:\mathbb{N} such that NiN \leq i, x il<ϵx_i - l \lt \epsilon or lx i<ϵl - x_i \lt \epsilon

AA is sequentially Cauchy complete if every Cauchy sequence in AA merely has a limit.

As a sequentially modulated Cauchy complete Archimedean field

Let FF be an Archimedean field. FF is sequentially modulated Cauchy complete if every Cauchy sequence in FF 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.

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

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:,b:,ϵ: +π(a,b,ϵ):isProp(a ϵb)a:\mathbb{Q}, b:\mathbb{Q}, \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

Last revised on July 2, 2022 at 11:05:40. See the history of this page for a list of all contributions to it.