Point-free characterisation of Bishop compact metric spaces

Abstract

We give a point-free characterisation of Bishop compact metric spaces in terms of formal topology. We show that the notion of overt compact enumerably completely regular formal topology is a point-free counterpart of that of Bishop compact metric space. Specifically, a formal topology is isomorphic to an overt compact enumerably completely regular formal topology if and only if it is isomorphic to the image of a compact metric space under the localic completion of metric spaces into formal topologies. The result is obtained in Bishop constructive mathematics with the axiom of Dependent Choice.