On the collection of points of a formal space.

The concept of set available to constructive mathematics is considerably more restrictive than the classical or topos-theoretic ones. Many important constructions yield classes that in the mathematical practice are implicitly proved small by relying on strong comprehension principles. These classes may be hard to be presented as sets constructively, and often they can not. In this paper (every collection of objects that can be regarded as) the class of points of a locally compact regular (=locally compact Hausdorff) formal space is proved to form a set in every foundation adequate to constructive mathematics in the sense of Feferman (in particular therefore in type theory and constructive set theory). The skeleton of a constructive theory of uniform locales/ formal spaces, based on the notion of elementary diameter, is also introduced and used to derive generalizations and a more perspicuous version of the mentioned set-representation.