The construction of the reals as the Cauchy completion of the rationals was worked out in full and glorious detail in the Montreal spring of 1973. The point is that taking equiconvergence classes of Cauchy sequences fails to construct the reals in a topos because of the absence generally of countable choice. Take your favourite example of a topos in which this fails, and you are most of the way to having your counter-example. To obtain the constructive version of the Cauchy reals, coinciding with the Dedekind reals in any topos with natural number object, you need to think a little more carefully about you are trying to achieve. The important thing about a Dedekind real is that there exist rationals that are arbitrarily close to it. The problem is that of choosing an instance of a rational at distance < 1/n from the real for each n. If you have countable choice, then choose away, get a Cauchy sequence, and have an isomorphism of Cauchy reals with Dedekind reals. Without countable choice, you still have an inhabited subset of the rationals consisting of all rationals at a distance of < 1/n from the Dedekind cut. This gives you a sequence of such subsets - a Cauchy approximation to the real. The constructive version of the Cauchy reals is the set of equiconvergence classes of Cauchy approximations on the rationals. For the details, later extended to the context of seminormed spaces over the rationals, with the set of rationals as the canonical example, see papers such as Burden/Mulvey in SLN 753 and my paper Banach sheaves in JPAA 17, 69-83 (1980). In the present context, the question is whether you wish to study the deficiencies of toposes in which countable choice fails, in which case Cauchy sequences are for you, or whether you want to develop constructive analysis within a topos, in which case you need to look at Cauchy approximations instead. Ask yourself, when you take a point in the closure of a subset, do you get handed a Cauchy sequence converging to it, or a sequence of possible choices of elements within 1/n of it if only you had countable choice to choose them. If the former, go for Cauchy sequences and count your blessings. If the latter, work with Cauchy approximations, which are every bit as powerful as Cauchy sequences and with respect to which the reals are Cauchy complete. Of course, the approach to Banach spaces through completeness defined in terms of Cauchy approximations acquires collateral justification in terms of the approaches to Banach sheaves taken by Auspitz and Banaschewski, to which reference can be found in the papers above. It is also the approach that allows Gelfand duality to be established constructively between commutative C*-algebras and compact completely regular locales in work with Banaschewski and with Vermeulen. Chris Mulvey.