Say we prove some theorem constructively (by which I mean, without choice and without LEM). Then it's true inside an arbitrary topos, and in the case of sheaf topoi we can externalize our theorem into some statement about sheaves, which a "regular mathematician" might care about. See, for instance, my question here.
I'm currently working through the details of Hyland's effective topos, which (internally) satisfies the statement "every function $\mathbb{N} \to \mathbb{N}$ is computable". Obviously the mere existence of this topos has philosophical applications (for instance, it tells us that every constructive proof must automatically give computable objects out the other side) but I'm curious if there are any more concrete ways of applying the topos in computability theory (for instance). Precisely:
Is there a way to externalize theorems inside of the effective topos to say something about "classical" computability theory, in a way that's analogous to externalizing theorems inside a sheaf topos to say something about "classical" sheaf theory?
I've tried to work through the construction of the effective topos, using Kripke-Joyal semantics, but unfortunately I don't understand the construction of the effective topos (or indeed, the motivation for the construction) well enough to know what's going on "in the real world".
Thanks in advance! ^_^