On the collection of points of a formal space (Q2575767)

The paper deals with formal spaces in a range of constructive settings. It is shown that for any formal space \(S\) belonging to some important class of formal spaces (such as locally compact regular formal spaces), the collection Pt\((S)\) of the points of \(S\) is isomorphic to a set. The proof is independent from the constructive foundation adopted, and the proofs that the constructions of the considered classes of points indeed yield sets may be formulated in terms of E. Bishop's naive set and subset theory.