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. (c) 2007 Elsevier B.V. All rights reserved.