Morphisms used to transport results from any instance of
ConstructiveReals to any other.
Between any two constructive reals structures R1 and R2,
all morphisms R1 -> R2 are extensionally equal. We will
further show that they exist, and so are isomorphisms.
The difference between two morphisms R1 -> R2 is therefore
the speed of computation.
The canonical isomorphisms we provide here are often very slow,
when a new implementation of constructive reals is added,
it should define its own ad hoc isomorphisms for better speed.
Apart from the speed, those unique isomorphisms also serve as
sanity checks of the interface ConstructiveReals :
it captures a concept with a strong notion of uniqueness.
WARNING: this file is experimental and likely to change in future releases.