nLab overlap algebra

Idea

Overlap algebras are one possible constructive version of complete Boolean algebras. In the presence of excluded middle, the category of overlap algebras is equivalent to the category of complete Boolean algebras and continuous homomorphisms.

However, in the absence of excluded middle, the powerset of a set is no longer a complete Boolean algebra, but it is an overlap algebra.

Definition

(See Definition 2.1 in OA.)

An overlap algebra is an overt frame $L$ such that if for all $z\in L$ the positivity of $z\wedge x$ implies the positivity of $z\wedge y$, then we have $x\le y$.

Morphisms of overlap algebras are precisely open morphisms of frames.

Thus, in the presence of excluded middle the category of overlap algebras is equivalent to the category of complete Boolean algebras, see Proposition 5.2 in OA.

Properties

In the presence of excluded middle, overlap algebras coincide with complete Boolean algebras. (Proposition 2.2 and Proposition 5.2 in OA.)

References

Francesco Ciraulo?, Michele Contente?, Overlap Algebras: a Constructive Look at Complete Boolean Algebras, arXiv:1904.13320