On the collection of points of a formal space

The collection of points of a locally compact regular formal space is shown to be isomorphic to a set in the context of Martin-Löf type theory. By introducing the notion of uniform formal space, this result is refined and generalized in the subcategory of open formal spaces.