CoRN.reals.R_morphism