Every metric space is separable in function realizability

Andrej Bauer, Andrew Swan

We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with syntheti…