Pretopologies and a uniform presentation of sup-lattices, quantales and frames

We introduce the notion of infinitary preorder and use it to obtain a predicative presentation of sup-lattices by generators and relations. The method is uniform in that it extends in a modular way to obtain a presentation of quantales, as “sup-lattices on monoids”, by using the notion of pretopology. Our presentation is then applied to frames, the link with Johnstone’s presentation of frames is spelled out, and his theorem on freely generated frames becomes a special case of our results on quantales. The main motivation of this paper is to contribute to the development of formal topology. That is why all our definitions and proofs can be expressed within an intuitionistic and predicative foundation, like constructive type theory.