# Overlap Algebras: a Constructive Look at Complete Boolean Algebras

## TL;DR

This paper introduces overlap algebras as a constructive alternative to complete Boolean algebras, capturing natural structures like powersets and relating to locales, with foundational categorical properties explored.

## Contribution

It develops the theory of overlap algebras, extending the category of sets and relations, and connects them to locale theory in a constructive setting.

## Key findings

- Overlap algebras generalize complete Boolean algebras constructively.
- The category of overlap algebras has well-understood mono-epi-isomorphisms and (co)limits.
- Constructive connections between overlap algebras and locales are established.

## Abstract

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.