Recently arxiv submitted a [new paper][1] claiming an incredible theorem that Dedekind reals are not sequence-avoiding, and furthermore obtaining a topos that makes Dedekind reals countable.

I'm wondering the constructivism Eudoxus reals is sequence-avoiding?


Also, if “all functions $\mathbb{Z} \to \mathbb{Z}$ are computable” holds, what will be the behaviour of Eudoxus reals? Would it become computable?



  [1]: https://arxiv.org/abs/2404.01256