Constructive strong regularity and the extension property of a compactification

TL;DR

This paper develops a fully constructive approach to strong regularity in locales, enabling the construction of compact regular compactifications and characterizing locale compactifications through extension properties.

Contribution

It introduces a constructive formulation of strong regularity for locales, replacing non-constructive principles with coinductive definitions and the Relation Reflection Scheme.

Findings

Every strongly regular locale has a compact regular compactification.

Characterization of locale compactifications via extension of continuous functions.

Open problem on the existence of the compact regular reflection of a locale.

Abstract

In contexts in which the principle of dependent choice may not be available, as toposes or Constructive Set Theory, standard locale theoretic results related to complete regularity may fail to hold. To resolve this difficulty, B. Banaschewski and A. Pultr introduced strongly regular locales. Unfortunately, Banaschewski and Pultr's notion relies on non-constructive set existence principles that hinder its use in Constructive Set Theory. In this article, a fully constructive formulation of strong regularity for locales is introduced by replacing non-constructive set existence with coinductive set definitions, and exploiting the Relation Reflection Scheme. As an application, every strongly regular locale $L$ is proved to have a compact regular compactification. The construction of this compactification is then used to derive the main result of this article: a characterization of locale compactifications (and thus, classically, of the compactifications of a space) in terms of their ability of extending continuous functions with compact regular codomains. Finally, an open problem related to the existence of the compact regular reflection of a locale is presented.