Peter Johnstone writes:
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,
In fact not. Markov's principle holds in the effective topos, and there, unless I'm much mistaken, it is not even true that the map from binary representations to Cauchy (= Dedekind) reals in [0,1] is epi, let alone split epi. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209