Constructive reals and choice principles

A rational Cauchy sequence has arbitrarily small tails. If this is supplied as untruncated dependent data, it includes a function selecting a tail index for every requested precision and a proof that the selection works. If the definition instead uses merely existing indices, extracting a simultaneous modulus is an additional step whose justification depends on the ambient theory. These packages should not be conflated simply because both are described verbally as a Cauchy sequence.

A chosen modulus makes approximation quantitative: ask for a precision, compute the indicated index, and use the accompanying estimate. Different rational sequences can represent the same real, so a quotient or other identification construction is still needed to make representation-independent equality. Equality of real numbers is not automatically a decidable comparison just because rational arithmetic is decidable. Positive separation can often be witnessed by a rational gap, whereas absence of a known separation is not an equality certificate.

A constructive Dedekind real can be given by lower and upper rational cuts satisfying inhabitation, roundedness, disjointness, and a locatedness condition. Locatedness says that whenever one rational is strictly below another, the real lies above the first or below the second, with logical disjunction interpreted according to the chosen foundation. It does not assert an exact comparison with every rational, since equality with a boundary rational may prevent a strict alternative at that same boundary.

In the HoTT book's specified constructions, the canonical map from Cauchy reals into Dedekind reals is an embedding. The book proves that countable choice is sufficient to make it an equivalence, and gives excluded middle as another sufficient assumption. This is a scoped comparison result, not a claim that every constructive foundation must adopt choice or that every presentation of Cauchy reals has identical completeness properties. The distinction between truncated existence and selected rational approximations is central to the proof.

Suppose a sequence consists of equivalence classes of rational Cauchy sequences. A diagonal construction may begin by selecting one representative from every class. Mere membership in a quotient does not in general supply that countable list of representatives. A countable choice assumption can justify such a step in suitable formulations, but an argument should identify where it was used. Assuming an arbitrary sequence already comes with chosen representatives is a stronger input specification than starting with bare quotient elements.

Other constructions organize completion differently. The HoTT book develops a higher inductive Cauchy completion that builds in the needed limit operation without simply repeating a representative-selection proof. Its comparison with Dedekind reals remains a separate theorem. For concrete numerical work, one can often avoid these foundational choices by supplying explicit rational approximations and bounds from the outset. Such a calculation proves the stated approximation guarantee; it does not settle every possible equivalence between competing foundational definitions of the real continuum.