We present and study the category of formal topologies and some of its variants. Two main results are proven. The first is that, for any inductively generated formal cover, there exists a formal topology whose cover extends in the minimal way the given one. This result is obtained by enhancing the method for the inductive generation of the cover relation by adding a coinductive generation of the positivity predicate. Categorically, this result can be rephrased by saying that inductively generated formal (...) topologies are coreflective into inductively generated formal covers. The second result is that unary formal covers are exponentiable in the category of inductively generated formal covers and hence, thanks to the coreflection, unary formal topologies are exponentiable in the category of inductively generated formal topologies. From a localic point of view the exponentiability of unary formal topologies means that algebraic dcpos are exponentiable in the category of open locales. But, the coreflection theorem states that open locales are coreflective in locales and hence, as a consequence of well-known impredicative results on exponentiable locales, it allows to prove that locally compact open locales are exponentiable in the category of open locales. (shrink)

If a locale is presented by a “flat site”, it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale . Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies. A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion (...) is then related to the double powerlocale. (shrink)

Abstract.Formal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in [CSSV]. However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to (...) this framework the method used to generate inductively formal topologies with a unary positivity predicate; the main problem that one has to face in such a new setting is that, as a consequence of the lack of a complete formalization, both the cover relation and the positivity predicate can have proper axioms. (shrink)

Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...) a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined. (shrink)