The Countable Reals

Andrej Bauer, James E. Hanson

We construct a topos in which the Dedekind reals are countable. The topos arises from a new kind of realizability, which we call parameterized realizability, based on partial combi…