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.