Re: Cauchy completeness of Cauchy reals

[Alex Simpson <als@inf.ed.ac.uk>]

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