We construct a Galois connection between closure and interior operators on a given set. All arguments are intuitionistically valid. Our construction is an intuitionistic version of the classical correspondence between closure and interior operators via complement.

A positive topology is a set equipped with two particular relations between elements and subsets of that set: a convergent cover relation and a positivity relation. A set equipped with a convergent cover relation is a predicative counterpart of a locale, where the given set plays the role of a set of generators, typically a base, and the cover encodes the relations between generators. A positivity relation enriches the structure of a locale; among other things, it is a tool to (...) study some particular subobjects, namely the overt weakly closed sublocales. We relate the category of locales to that of positive topologies and we show that the former is a reflective subcategory of the latter. We then generalize such a result to the category of suplattices, which we present by means of cover relations. Finally, we show that the category of positive topologies also generalizes that of formal topologies, that is, overt locales. (shrink)

Giovanni Sambin has recently introduced the notion of an overlap algebra in order to give a constructive counterpart to a complete Boolean algebra. We propose a new notion of regular open subset within the framework of intuitionistic, predicative topology and we use it to give a representation theorem for overlap algebras. In particular we show that there exists a duality between the category of set-based overlap algebras and a particular category of topologies in which all open subsets are regular.

We study some connections between two kinds of emph{overlap} relations: that of point-free geometries in the sense of Grzegorczyk, Whitehead and Clarke, and that recently introduced by Sambin within his constructive approach to topology. The main thesis of this paper is that the overlap relation in the latter sense is a necessary tool for a constructive and intuitionistic development of point-free geometry.

This paper provides a constructive topological semantics for non-deducibility of a first order intuitionistic formula. Formal topology theory, in particular the recently introduced notion of a binary positivity predicate, and co-induction are two needful tools.

We characterize the category of Sambin’s positive topologies as the result of the Grothendieck construction applied to a doctrine over the category Loc of locales. We then construct an adjunction between the category of positive topologies and that of topological spaces Top, and show that the well-known adjunction between Top and Loc factors through the constructed adjunction.

We characterize the category of Sambin’s positive topologies as the result of the Grothendieck construction applied to a doctrine over the category Loc of locales. We then construct an adjunction between the category of positive topologies and that of topological spaces Top, and show that the well-known adjunction between Top and Loc factors through the constructed adjunction.