A constructive and functorial embedding of locally compact metric spaces into locales

The paper establishes, within constructive mathematics, a full and faithful functor M from the category of locally compact metric spaces and continuous functions into the category of formal topologies (or equivalently locales). The functor preserves finite products, and moreover satisfies f ⩽ g if, and only if, M ( f ) ⩽ M ( g ) for continuous f , g : X → R . This makes it possible to transfer results between Bishopʹs constructive theory of metric spaces and constructive locale theory.