Relative computability in the effective topos
Wesley Phoa · Mathematical Proceedings of the Cambridge Philosophical Society · 1989
Let ℕ be the natural numbers object in , the effective topos. It was shown in [1] that the maps ℕ → ℕ are (internally or externally) just the total recursive functions. Now a subset A ⊆ ω of natural numbers corresponds to a ¬¬-closed subobject A ↣ ℕ; let kA be the least topology forcing A to be decidable, and let ℕA be the sheafification of ℕ with respect to this topology. Then one would expect the maps ℕ → ℕA to be the total functions recursive in A.