Cauchy completeness of Cauchy reals

[Martin Escardo <m.escardo@cs.bham.ac.uk>]

Andrej Bauer writes:
 > find a topos in which Cauchy reals
 > are not Cauchy complete (i.e., not every Cauchy sequence of reals has
 > a limit). For extra credit, make it so that the Cauchy completion of
 > Cauchy reals is strictly smaller than the Dedekind reals.

One small clarification: Regarding the extra credit, there doesn't
seem to be a reasonable "absolute" way of defining the completion in
question. E.g.  the various, constructively different, notions of
metric completion already assume the existence of some given complete
reals. However, one can always embed the Cauchy reals into the
Dedekind reals, which are always Cauchy complete, and then look at the
smallest "subset" containing this which is closed under limits of
Cauchy sequences (where Cauchy sequences are defined as in Andrej's
message). We sometimes call this, somewhat verbosely, "the Cauchy
completion of the Cauchy reals within the Dedekind reals".  But notice
that this is the same as what one gets starting from the rationals
within the Dedekind reals and then closing under limits and hence
could be called the "Cauchy completion of the rationals within the
Dedekind reals".

NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
Simpson and I characterized "the Cauchy completion of the rationals
within the Dedekind reals" as a free algebra (to be precise, we
started from the algebras as a primitive notion and later found this
construction of the free one). But this has already been discussed in
postings in the past few years.

Martin Escardo