11.3 Cauchy reals

The Cauchy reals are, by intent, the completion of $\mathbb{Q}$ under limits of Cauchy sequences. In the classical construction of the Cauchy reals, we consider the set $𝒞$ of all Cauchy sequences in $\mathbb{Q}$ and then form a suitable quotient $𝒞/\approx$. Then, to show that $𝒞/\approx$ is Cauchy complete, we consider a Cauchy sequence $x:\mathbb{N}\to 𝒞/\approx$, lift it to a sequence of sequences $\overline{x}:\mathbb{N}\to 𝒞$, and construct the limit of $x$ using $\overline{x}$. However, the lifting of $x$ to $\overline{x}$ uses the axiom of countable choice (the instance of (LABEL:eq:ac) where $X=\mathbb{N}$) or the law of excluded middle, which we may wish to avoid. Every construction of reals whose last step is a quotient suffers from this deficiency. There are three common ways out of the conundrum in constructive mathematics:

1. Pretend that the reals are a setoid $(𝒞,\approx )$, i.e., the type of Cauchy sequences $𝒞$ with a coincidence relation attached to it by administrative decree. A sequence of reals then simply is a sequence of Cauchy sequences representing them.

2. Give in to temptation and accept the axiom of countable choice. After all, the axiom is valid in most models of constructive mathematics based on a computational viewpoint, such as realizability models.

3. Declare the Cauchy reals unworthy and construct the Dedekind reals instead. Such a verdict is perfectly valid in certain contexts, such as in sheaf-theoretic models of constructive mathematics. However, as we saw in sec:dedekind-reals, the constructive Dedekind reals have their own problems.

Using higher inductive types, however, there is a fourth solution, which we believe to be preferable to any of the above, and interesting even to a classical mathematician. The idea is that the Cauchy real numbers should be the free complete metric space generated by $\mathbb{Q}$. In general, the construction of a free gadget of any sort requires applying the gadget operations repeatedly many times to the generators. For instance, the elements of the free group on a set $X$ are not just binary products and inverses of elements of $X$, but words obtained by iterating the product and inverse constructions. Thus, we might naturally expect the same to be true for Cauchy completion, with the relevant “operation” being “take the limit of a Cauchy sequence”. (In this case, the iteration would have to take place transfinitely, since even after infinitely many steps there will be new Cauchy sequences to take the limit of.)

The argument referred to above shows that if excluded middle or countable choice hold, then Cauchy completion is very special: when building the completion of a space, it suffices to stop applying the operation after one step. This may be regarded as analogous to the fact that free monoids and free groups can be given explicit descriptions in terms of (reduced) words. However, we saw in sec:free-algebras that higher inductive types allow us to construct free gadgets directly, whether or not there is also an explicit description available. In this section we show that the same is true for the Cauchy reals (a similar technique would construct the Cauchy completion of any metric space; see ex:metric-completion). Specifically, higher inductive types allow us to simultaneously add limits of Cauchy sequences and quotient by the coincidence relation, so that we can avoid the problem of lifting a sequence of reals to a sequence of representatives.

Title	11.3 Cauchy reals