Constructive version of Boolean algebra

TL;DR

This paper develops a constructive framework for Boolean algebras using overlap algebras, providing new characterizations and generalizations that align with constructive mathematics principles.

Contribution

It introduces a constructive approach to Boolean algebras via overlap algebras, including new properties, descriptions, and generalizations of morphisms.

Findings

Overlap morphisms correspond classically to join-preserving maps

Atomic overlap algebras are characterized in formal topology

Power-collections form free overlap algebras from sets

Abstract

The notion of overlap algebra introduced by G. Sambin provides a constructive version of complete Boolean algebra. Here we first show some properties concerning overlap algebras: we prove that the notion of overlap morphism corresponds classically to that of map preserving arbitrary joins; we provide a description of atomic set-based overlap algebras in the language of formal topology, thus giving a predicative characterization of discrete locales; we show that the power-collection of a set is the free overlap algebra join-generated from the set. Then, we generalize the concept of overlap algebra and overlap morphism in various ways to provide constructive versions of the category of Boolean algebras with maps preserving arbitrary existing joins.