Where can I find the proof of the theorem and what is the computational complexity of the computably isomorphic map? "any two representations of reals which are acceptable are actually computably isomorphic",please see here for reference

where may proof of  this theorem   be found, and what is the the computational complexity of the computably isomorphic maps?
To turn my comment into an answer...

Andrej Bauer in this post makes the parenthetical claim 


  An important theorem states that any two representations of reals which are acceptable are actually computably isomorphic.


He never explicitly defines acceptable or cites the theorem. I assume the OPs question is the following.

What theorem is Andrej Bauer referring to?

Here is a guess.  It seems that earlier in the post, Andrej is implicitly suggesting that an acceptable representation of the reals is one in which the following properties hold:


One can effectively approximate a real by a rational to within a given precision.
Addition, multiplication, and inverse are computable.
The less-then relation, $&lt;$, is semi-decidable.
There is a computable function which takes in a rapid sequence of reals (that is a sequence $(x_n)$ of reals such that $|x_n - x_m| \leq 2^{\min{n,m}}$ and outputs the limit.


Actually (1) and (4) are enough to prove (2) and (3), since to preform those operations: one only needs to approximate the real by a rational, do the operation, and convert back to a real.  (Basic module of continuity will tell you how close the approximated answer is.  Also, one needs to be able to convert from a rational to the corresponding real.  This can be done by using (1) to find reals that are close enough to the rational, and then using (4) to take the limit of these approximations.)

Now, for any two representations satisfying (1) and (4) they are computably isomorphic.  From (1), one can go from the first representation to the rapid Cauchy representation.  (That is, represent a real as a rapid Cauchy sequence of rationals.)  From (4), one can go the other way, taking a rapid Cauchy sequence of rationals and computing the real it converges to (using the second representation).

As for the question about complexity, I think it can't be anything better than just computable, but I realize I don't know for sure, mostly, because I don't know how to formulate the question formally.