Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic <dusko@kestrel.edu>]

heh, i typed this late, and managed to confuse the basic assumption.
instead of

> let a = (a_i) be a cauchy sequence of rationals between 0 and 1.

let a = (a_i) be a cauchy sequence of *cauchy reals*, i.e. each a_i is a
cauchy sequence of rationals between 0 and 1.

i think the rest goes unchanged: you take a fast converging subsequence
b of a, and then approximate b by irredundant rational prefixes. the
irredundant representation is thus used instead of choice. the
completeness of such representation is the finality of its coalgebraic
structure.

-- dusko