Alex Simpson <als@inf.ed.ac.uk> writes:

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.

The map e : 2^N --> [0,1] defined by e x = x_0/2 + x_1/4 + x_2/8 + ... is epi in the effective topos, but it is not regular epi. In terms of logic, this means that forall a : [0,1]. (not not (exists x : 2^n. (e x = a))) is valid in the effective topos, but forall a : [0,1]. (exists x : 2^n. (e x = a)) is not valid. Andrej