When we say that computations are continuous functions we don't mean with respect to any old topology. We are specifically referring to the Scott topology. The topology of Cauchy sequences does not have the same topology as the real line. It has the topology of the Cantor space. Your digit stream producing function is a perfectly continuous function with respect to this topology.

When we quotient Cauchy sequences by an equivalence relation we are imposing an external topological structure on the type, but the representatives don't change. They are still Cauchy sequences, and the same constructive functions are definable, though as you note, these function may not respect the equivalence relation we have imposed. In constructive type theory, we call this quotient structure a setoid (a type paired with an equivalence relation), and functions between setoids that respect the equivalence relations are called respectful functions.

Respectful functions are not necessarily continuous on an externally imposed topology. Consider the following simple example. Consider the subset of ℝ, {$x$ | $x$ < 0 constructive-or 0 ≤ $x$}. We can easily define a constructive function on this domain that is 0 when $x$ < 0 and 1 when 0 ≤ $x$. This function is discontinuous on the induced topology of our domain.

However, in the case of (total) respectful functions from the reals to the natural numbers, it happens to be the case that the only ones we can prove exist are the continuous (and hence constant) ones.

When we say that computations are continuous functions we don't mean with respect to any old topology. We are specifically referring to the Scott topology. The topology of Cauchy sequences does not have the same topology as the real line. It has the topology of the Cantor space. Your digit stream producing function is a perfectly continuous function with respect to this topology.

When we quotient Cauchy sequences by an equivalence relation we are imposing an external topological structure on the type, but the representatives don't change. They are still Cauchy sequences, and the same constructive functions are definable, though as you note, these function may not respect the equivalence relation we have imposed. In constructive type theory, we call this quotient structure a setoid (a type paired with an equivalence relation), and functions between setoids that respect the equivalence relations are called respectful functions.

Respectful functions are not necessarily continuous on an externally imposed topology. Consider the following simple example. Consider the subset of ℝ, {$x$ | $x$ < 0 constructive-or 0 ≤ $x$}. We can easily define a constructive function on this domain that is 0 when $x$ < 0 and 1 when 0 ≤ $x$. This function is discontinuous on the induced topology of our domain.

However, in the case of (total) respectful functions from the reals to the natural numbers, it happens to be the case that the only ones we can construct are the continuous (and hence constant) ones.