It appears the answer to the original question is finally available now, a decade later, due to Andrej Bauer and James Hanson, the former of which had already provided a helpful response here ten years ago. Though we do not have such a surjection in the effective topos per se, we can use a modification of the effective topos concept to get a nontrivial topos with a surjection from the naturals to the Dedekind reals. See https://www.youtube.com/watch?v=4CBFUojXoq4.
Sridhar Ramesh
- 5.8k
- 1
- 34
- 45