A specification is said to be categorical or monomorphic, if it has exactly one model up to isomorphism. Neither the specification BasicReal nor the specifications of the reals in ZFC or HOL are categorical. Due to the theorem of Löwenheim and Skolem, a categorical axiomatization is impossible6. However, it is possible to prove the internal categoricity of the specification of the reals in ZFC (meaning that within each model of ZFC plus two axiomatizations of the reals, the two reals are isomorphic). A similar result should hold for the reals in HOL (but we are not entirely sure). BasicReal is definitely too weak for such a result, since there is not even an internalized notion of functions on reals.