Boolean locales are "almost discrete", in the sense that a spatial Boolean locale is just a discrete locale (that is, it corresponds to the frame of open subsets of a discrete space, namely the powerset of a set). This basic fact, however, cannot be proven constructively, that is, over intuitionistic logic, as it requires the full law of excluded middle (LEM). In fact, discrete locales are never Boolean constructively, except for the trivial locale. So, what is an almost discrete locale constructively? Our claim is that Sambin's overlap algebras have good enough features to deserve to be called that. Namely, they include the class of discrete locales, they arise as smallest strongly dense sublocales (of overt locales), and hence they coincide with the Boolean locales if LEM holds.

A σ-frame is a poset with countable joins and finite meets in which binary meets distribute over countable joins. The aim of this paper is to show that σ-frames, actually σ-locales, can be seen as a branch of Formal Topology, that is, intuitionistic and predicative point-free topology. Every σ-frame L is the lattice of Lindelöf elements (those for which each of their covers admits a countable subcover) of a formal topology of a specific kind which, in its turn, is a presentation of the free frame over L. We then give a constructive characterization of the smallest (strongly) dense σ-sublocale of a given σ-locale, thus providing a “σ-version” of a Boolean locale. Our development depends on the axiom of countable choice.

The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent to that of a complete Boolean algebra, has powersets and other natural structures as instances. In this paper we study the category of overlap algebras as an extension of the category of sets and relations, and we establish some basic facts about mono-epi-isomorphisms and (co)limits; here a morphism is a symmetrizable function (with classical logic this is just a function which preserves joins). Then we specialize to the case of morphisms which preserve also finite meets: classically, this is the usual category of complete Boolean algebras. Finally, we connect overlap algebras with locales, and their morphisms with open maps between locales, thus obtaining constructive versions of some results about Boolean locales. Comment: Postproceedings of CCC2018: Continuity, Computability, Constructivity. Faro, Portugal, 24-28 Sep 2018

Abstract 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.