Constructive strong regularity and the extension property of a compactification

[giovan...@email.it]

Constructive strong regularity and the extension property of a compactification 

APAL, to appear

https://arxiv.org/abs/2105.07457

The system for constructive set theory adopted in this article allows for general inductive and coinductive definitions of sets. 

It seems remarkable to me that this system provides exactly what is needed for a constructive and choice-free theory of regular compactifications. 

The intended audience includes readers familiar with locale theory and intuitionistic reasoning, but not necessarily with constructive set theory. 

The adopted principles of constructive set theory that may be unfamiliar to the non-specialist, in particular inductive and coinductive definitions, are presented informally. 

An open problem related to the constructive existence of the compact regular reflection of a locale ('weak' Stone-Cech compactification) is also discussed. 

Giovanni Curi