Constructive metrisability in point-free topology. (Q1427775)

The author introduces the notion of elementary diameter to provide a constructive notion of metrisability (in the context of locale theory). First, he investigates a predicative formulation and properties of complete regularity. The main notion of metric formal topologies is based on a constructive and predicative notion of metrisability and a point-free axiomatisation of the theory of metrics in spaces. Rather than the properties of a diameter in the general sense, the author describes a diameter of basic or atomic elements. The main result is a point-free version of the Urysohn metrization theorem with a constructive choice-free proof. As an application, the author shows that the points of locally compact metrisable formal topologies can be identified with ``shrinking'' and ``approximating'' sequences of basic neighbourhoods.