11. Real numbers

Any foundation of mathematics worthy of its name must eventually address the construction of real numbers as understood by mathematical analysis, namely as a complete archimedean ordered field. There are two notions of completeness. The one by Cauchy requires that the reals be closed under limits of Cauchy sequences, while the stronger one by Dedekind requires closure under Dedekind cuts. These lead to two ways of constructing reals, which we study in sec:dedekind-reals and sec:cauchy-reals, respectively. In RD-final-field,RC-initial-Cauchy-complete we characterize the two constructions in terms of universal properties: the Dedekind reals are the final archimedean ordered field, and the Cauchy reals the initial Cauchy complete archimedean ordered field.

In traditional constructive mathematics, real numbers always seem to require certain compromises. For example, the Dedekind reals work better with power sets or some other form of impredicativity, while Cauchy reals work well in the presence of countable choice. However, we give a new construction of the Cauchy reals as a higher inductive-inductive type that seems to be a third possibility, which requires neither power sets nor countable choice.

In sec:comp-cauchy-dedek we compare the two constructions of reals. The Cauchy reals are included in the Dedekind reals. They coincide if excluded middle or countable choice holds, but in general the inclusion might be proper.

In sec:compactness-interval we consider three notions of compactness of the closed interval $[0,1]$. We first show that $[0,1]$ is metrically compact in the sense that it is complete and totally bounded, and that uniformly continuous maps on metrically compact spaces behave as expected. In contrast, the Bolzano–Weierstraß property that every sequence has a convergent subsequence implies the limited principle of omniscience, which is an instance of excluded middle. Finally, we discuss Heine-Borel compactness. A naive formulation of the finite subcover property does not work, but a proof relevant notion of inductive covers does. This section is basically standard constructive analysis.

The development of real numbers and analysis in homotopy type theory can be easily made compatible with classical mathematics. By assuming excluded middle and the axiom of choice we get standard classical analysis: the Dedekind and Cauchy reals coincide, foundational questions about the impredicative nature of the Dedekind reals disappear, and the interval is as compact as it could be.

We close the chapter by constructing Conway’s surreals as a higher inductive-inductive type in sec:surreals; the construction is more natural in univalent type theory than in classical set theory.

In addition to the basic theory of cha:basics,cha:logic, as noted above we use “higher inductive-inductive types” for the Cauchy reals and the surreals: these combine the ideas of cha:hits with the notion of inductive-inductive type mentioned in sec:generalizations. We will also frequently use the traditional logical notation described in subsec:prop-trunc, and the fact (proven in sec:piw-pretopos) that our “sets” behave the way we would expect.

Note that the total space of the universal cover of the circle, which in subsec:pi1s1-homotopy-theory played a role similar to “the real numbers” in classical algebraic topology, is not the type of reals we are looking for. That type is contractible, and thus equivalent to the singleton type, so it cannot be equipped with a non-trivial algebraic structure.

Title	11. Real numbers