Re: Cauchy completeness of Cauchy reals

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