| Summary: | 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.
|
|---|