Constructive metrisability in point-free topology.

Previous work on locales (mainly by Isbell, Pultr, and Banaschewski) has treated metrisability only classically. This paper presents a constructive theory of metrisability based on the notion of elementary diameter. Beside the constructive features, the resulting concept of metric locale (metric formal space) is easier to handle with respect to the existing ones. In particular, metric formal spaces in the sense of this paper may be regarded as providing presentations for Pultr's metric locales. By exploiting the notion of elementary diameter one may formulate quantitatively - in the form of the 'measurably inside' relation - the idea that a given neighbourhood is 'finer than', or is a 'better approximation than', another neighbourhood. This relation is then used to express metrisability. The way-below, well and really inside relations, used in the point-free formulation of local compactness, regularity and complete regularity, respectively, may similarly be regarded as expressions of a concept of 'finer than'. These intuitive similarities can be made formal: in particular, a constructive proof of Urysohn metrization theorem is obtained by constructing a diameter that 'transforms' the really inside relation into the measurably inside relation. This machinery is finally applied to prove that the class of points of a locally compact metrisable locale is a set constructively.