On Fri, 24 Jan 2003, Dusko Pavlovic wrote:
Set. Do you think your construction works in any topos?
the coalgebraic structures are defined using just arithmetic. in the first one, there is the "no infinite sequences of 1s" condition, which i am reminded depends on markov's principle; but that is just used in the explanation. i don't think there are other constraints.
If so, what would "Cauchy reals" mean precisely in this general context?
it means fundamental sequence, with the equivalence relation in the "lazy" mode, a la bishop, as described in andrej bauer's message.
I'm sorry, but this won't do. In a topos, equality is equality; you can't treat it "lazily". So a Cauchy real has to be an equivalence class of Cauchy sequences, and there is in general no way of choosing a canonical representative for it. Markov's principle would, I think (I haven't checked the details), suffice to give a canonical representation as a binary expansion with no infinite sequence of 1's, and then Dusko's argument would suffice to show that the Cauchy reals are Cauchy complete. But there are many toposes where Markov's principle fails. I doubt very much whether the Cauchy reals occur as a final coalgebra for anything, in any topos where they fail to coincide with the Dedekind reals, simply because the Dedekind reals are likely to be a coalgebra for the same endofunctor (and they're more "final" than the Cauchy reals). Incidentally, Peter Freyd and I worked out how to do his coalgebra construction constructively, and I showed that its final coalgebra is the Dedekind interval in any topos -- the proof is in the Elephant, at the end of section D4.7. Peter Johnstone