Is it consistent intuitionistically (in the sense of topos theory) for there to be a surjection from the natural numbers to the Dedekind real numbers? [I've managed to convince myself this happens in the effective topos, but not so convincingly as I'd like; I suspect others will be able to answer more confidently off the top of their heads...]