Andrej Bauer: Countable reals – part II

Abstract: In the second part I will define uniform realizability, which is a variant of realizability that faithfully captures Turing machines which compute uniformly with respect to a set of oracles. We will then verify that the resulting topos indeed contains an epimorphism from the natural numbers to the Dedekind reals. If time permits, we will investigate the new topos a little further.