一句话：研究重叠代数范畴，将其视为集合与关系范畴的扩展，并建立与完全布尔代数及 locale 的构造性联系。
完全布尔代数在构造数学中虽合法，却无法刻画给定集合的幂集格等自然结构。Sambin 的重叠代数经典上等价于完全布尔代数，却能以幂集等为实例。本文研究重叠代数范畴，将其作为集合与关系范畴的扩展：态射为可对称化函数（经典逻辑下即保持 joins 的函数），并建立单-满-同构与（余）极限等基本事实。随后特化到同时保持有限 meets 的态射，经典情形即完全布尔代数范畴。最后把重叠代数与 locale 及其态射与 locale 间开映射相联系，得到若干 Boolean locale 结果的构造版本。
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
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CirauloC19,
title = {Overlap Algebras: a Constructive Look at Complete Boolean Algebras},
author = {Francesco Ciraulo and Michele Contente},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:13)2020}
}