A note on the axiomatisation of real numbers

Is it possible to give an abstract characterisation of constructive real numbers? This question may be for instance of interest if one wants to specify an abstract data type of real numbers for exact real computations. A condition should be that be that all axioms are valid for Dedekind reals in any topos, or for constructive reals in Bishop mathematics1. We present here a possibl