@MartinEscardo I'm a bit surprised you're so surprised by this, but maybe I'm biased since Paulo was my supervisor. I don't doubt this result is extremely cool if I could understand it, but instinctively I already felt that topology is related to constructivity (thanks to both topos theory and synthetic topology), whereas my mind is still blown by the cases where dialectica type methods were used to sharpen analytic bounds in ergodic theory and Ramsey theory and things like that