I’ve had some recent thoughts revolving around real numbers and rational numbers. Consider the real numbers from a constructivist’s point of view (as I often do) as a function taking a positive rational ε and returning a rational number within ε of the real number the function is representing.
Constructive functions on the reals, that return a real, must always be continuous. To me this seems like an extremely nice property of constructivism, and seems to indicate why we are so interested in continuous functions on the real numbers.
What is a little strange is that the behaviour of continuous functions are completely characterised by how they behave on the rationals. There are more functions from the rationals to the reals than continuous functions from the reals to the reals in the sense that every continuous function can be restricted to the rationals (and this restriction is an injection), but not every function on the rationals can be extended to a continuous function on the reals.
In general we would expect more functions from the reals to the reals than functions from the rationals to the reals. What is interesting is that when we try to do this constructively, every real function is continuous and we end up with fewer functions from the reals to the reals.
Although there are fewer functions, the structure is very nice, and that nice structure was probably our goal to begin with. It is just strange that the way of achieving this structure was not to take our functions from rationals to reals, and try to find a predicate to pull out the ones that are continuous, rather we do the opposite and expand the domain of our functions.
Maybe the trick is that not every function from the reals as defined is correct. Because there is more than one way of representing a real number by an approximating function, you have to prove that the real function respects this equivalence relation of the real numbers. This restriction might have the same effect as placing a continuity restriction on functions from the rationals.