11.3.1 Construction of Cauchy reals

The construction of the Cauchy reals ℝ𝖼 as a higher inductive type is a bit more subtle than that of the free algebraic structuresPlanetmathPlanetmath considered in \autorefsec:free-algebras. We intend to include a β€œtake the limit” constructor whose input is a Cauchy sequenceMathworldPlanetmathPlanetmath of reals, but the notion of β€œCauchy sequence of reals” depends on having some way to measure the β€œdistance” between real numbers. In general, of course, the distance between two real numbers will be another real number, leading to a potentially problematic circularity.

However, what we actually need for the notion of Cauchy sequence of reals is not the general notion of β€œdistance”, but a way to say that β€œthe distance between two real numbers is less than ϡ” for any Ο΅:β„š+. This can be represented by a family of binary relationsMathworldPlanetmath, which we will denote ∼ϡ:β„π–Όβ†’β„π–Όβ†’π–―π—‹π—ˆπ—‰. The intended meaning of x∼ϡy is |x-y|<Ο΅, but since we do not have notions of subtraction, absolute valueMathworldPlanetmathPlanetmathPlanetmathPlanetmath, or inequality available yet (we are only just defining ℝ𝖼, after all), we will have to define these relations ∼ϡ at the same time as we define ℝ𝖼 itself. And since ∼ϡ is a type family indexed by two copies of ℝ𝖼, we cannot do this with an ordinary mutual (higher) inductive definition; instead we have to use a higher inductive-inductive definition.

Recall from \autorefsec:generalizationsPlanetmathPlanetmath that the ordinary notion of inductive-inductive definition allows us to define a type and a type family indexed by it by simultaneous inductionMathworldPlanetmath. Of course, the β€œhigher” version of this allows both the type and the family to have path constructors as well as point constructors. We will not attempt to formulate any general theory of higher inductive-inductive definitions, but hopefully the description we will give of ℝ𝖼 and ∼ϡ will make the idea transparent.

Remark 11.3.1.

We might also consider a higher inductive-recursive definition, in which ∼ϡ is defined using the recursion principle of Rc, simultaneously with the inductive definition of Rc. We choose the inductive-inductive route instead for two reasons. Firstly, higher inductive-recursive definitions seem to be more difficult to justify in homotopical semantics. Secondly, and more importantly, the inductive-inductive definition yields a more powerful induction principle, which we will need in order to develop even the basic theory of Cauchy reals.

Finally, as we did for the discussion of Cauchy completeness of the Dedekind reals in \autorefsec:RD-cauchy-complete, we will work with Cauchy approximations (\autorefdefn:cauchy-approximation) instead of Cauchy sequences. Of course, our Cauchy approximations will now consist of Cauchy reals, rather than Dedekind reals or rational numbers.

Definition 11.3.2.

Let Rc and the relation ∼:Q+Γ—RcΓ—Rcβ†’U be the following higher inductive-inductive type family. The type Rc of Cauchy reals is generated by the following constructors:

  • β€’

    rational points: for any q:β„š there is a real 𝗋𝖺𝗍⁒(q).

  • β€’

    limit pointsPlanetmathPlanetmath: for any x:β„š+→ℝ𝖼 such that

    βˆ€(Ξ΄,Ο΅:β„š+).xδ∼δ+Ο΅xΟ΅ (11.3.2)

    there is a point 𝗅𝗂𝗆⁒(x):ℝ𝖼. We call x a Cauchy approximation.

  • β€’

    paths: for u,v:ℝ𝖼 such that

    βˆ€(Ο΅:β„š+).u∼ϡv (11.3.3)

    then there is a path π–Ύπ—Šβ„π–Όβ’(u,v):u=ℝ𝖼v.

Simultaneously, the type family ∼:Rcβ†’Rcβ†’Q+β†’U is generated by the following constructors. Here q and r denote rational numbers; Ξ΄, Ο΅, and Ξ· denote positive rationals; u and v denote Cauchy reals; and x and y denote Cauchy approximations:

  • β€’

    for any q,r,Ο΅, if -Ο΅<q-r<Ο΅, then 𝗋𝖺𝗍⁒(q)βˆΌΟ΅π—‹π–Ίπ—β’(r),

  • β€’

    for any q,y,Ο΅,Ξ΄, if 𝗋𝖺𝗍⁒(q)∼ϡ-Ξ΄yΞ΄, then 𝗋𝖺𝗍⁒(q)βˆΌΟ΅π—…π—‚π—†β’(y),

  • β€’

    for any x,r,Ο΅,Ξ΄, if xδ∼ϡ-δ𝗋𝖺𝗍⁒(r), then 𝗅𝗂𝗆⁒(x)βˆΌΟ΅π—‹π–Ίπ—β’(r),

  • β€’

    for any x,y,Ο΅,Ξ΄,Ξ·, if xδ∼ϡ-Ξ΄-Ξ·yΞ·, then 𝗅𝗂𝗆⁒(x)βˆΌΟ΅π—…π—‚π—†β’(y),

  • β€’

    for any u,v,ϡ, if ξ,΢:u∼ϡv, then ξ=΢ (propositional truncation).

The first constructor of ℝ𝖼 says that any rational number can be regarded as a real number. The second says that from any Cauchy approximation to a real number, we can obtain a new real number called its β€œlimit”. And the third expresses the idea that if two Cauchy approximations coincide, then their limits are equal.

The first four constructors of ∼ specify when two rational numbers are close, when a rational is close to a limit, and when two limits are close. In the case of two rational numbers, this is just the usual notion of Ο΅-closeness for rational numbers, whereas the other cases can be derived by noting that each approximant xΞ΄ is supposed to be within Ξ΄ of the limit 𝗅𝗂𝗆⁒(x).

We remind ourselves of proof-relevance: a real number obtained from 𝗅𝗂𝗆 is represented not just by a Cauchy approximation x, but also a proof p ofΒ (11.3.2), so we should technically have written 𝗅𝗂𝗆⁒(x,p) instead of just 𝗅𝗂𝗆⁒(x). A similar observation also applies to π–Ύπ—Šβ„π–Ό andΒ (11.3.3), but we shall write just π–Ύπ—Šβ„π–Ό:u=v instead of π–Ύπ—Šβ„π–Όβ’(u,v,p):u=v. These abuses of notation are mitigated by the fact that we are omitting mere propositions and information that is readily guessed. Likewise, the last constructor of ∼ϡ justifies our leaving the other four nameless.

We are immediately able to populate ℝ𝖼 with many real numbers. For suppose x:β„•β†’β„š is a traditional Cauchy sequence of rational numbers, and let M:β„š+β†’β„• be its modulus of convergence. Then π—‹π–Ίπ—βˆ˜x∘M:β„š+→ℝ𝖼 is a Cauchy approximation, using the first constructor of ∼ to produce the necessary witnessMathworldPlanetmath. Thus, 𝗅𝗂𝗆⁒(π—‹π–Ίπ—βˆ˜x∘m) is a real number. Various famous real numbers 2, Ο€, e, … are all limits of such Cauchy sequences of rationals.

Title 11.3.1 Construction of Cauchy reals