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 . This makes it possible to transfer results between Bishop's constructive theory of metric spaces and constructive locale theory.