# Constructive Strong Regularity and the extension property of a
compactification

Giovanni Curi<EMAIL_ADDRESS>
###### 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, as complete regularity of compact regular
locales, may fail to hold. For resolving 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. As an
application, every strongly regular locale $L$ is proved to have a compact
regular compactification. Furthermore, every compactification is shown to
enjoy a natural extension property for an associated class of continuous maps,
and to be the minimal compactification with this property. Finally, an open
problem related to the existence of the compact regular reflection of a locale
is presented.

###### Key words and phrases:

Compactifications, locales, strong regularity, inductive and coinductive
definitions, dependent choice, Constructive Set Theory.

###### 2020 Mathematics Subject Classification:

06D22, 54D35, 03D70, 03F65, 03E25

## Introduction

Among the different motivations for pursuing a point-free development of
general topology [12], a pivotal one is that point-free spaces (locales) often
allow for choice-free proofs of theorems that in their usual topological
formulation require the application of some form of choice principle. This
feature makes locale theory particularly suited for contexts in which no
choice principle is available, as (the internal language of) toposes [13] and
constructive set theories.

This ability of locales however fails in connection with the point-free
version of a well-known standard topological result: the proof that a compact
regular locale is completely regular relies indeed on the use of the principle
of Dependent Choice (DC), as for the corresponding fact for spaces [12]. As
already recalled, there are contexts in which DC is not available;
specifically, there are toposes, that do not validate DC, in which a compact
regular locale fails to be completely regular.

For obtaining choice-free analogues of this and other results involving
complete regularity, Banaschewski and Pultr [7] introduced the notion of
strongly regular locale. With DC, a locale is strongly regular if and only if
it is completely regular. Without DC, every completely regular locale is
strongly regular, and compact regular locales are strongly regular.

To formulate strong regularity, Banaschewski and Pultr use the existence of a
largest interpolative relation contained in a given binary relation $R$,
defined as the union of all interpolative relations contained in $R$.
Unfortunately, this definition is impredicative or circular, as the defined
relation is itself an interpolative relation contained in $R$. For this
construction, the Powerset axiom is implicitly used. While powersets
(powerobjects) are available in toposes and classical set theory, they are
regarded as highly problematic in those settings that, beside using
intuitionistic logical principles (as the internal logic of toposes), also
adopt a constructive notion of set.

The main set-theoretical system of this latter type is Constructive Set
Theory, CST [3]. In this article, using coinductive methods in CST, I
formulate a constructive notion of strong regularity, that in particular will
allow for the choice-free proof that a compact regular locale is strongly
regular, and that makes no use of non-constructive set existence principles.
This appears in Section 3. In Section 4, as an application of this concept, I
show that, as for toposes and ZF, in CST every strongly regular locale $L$ has
a compact regular compactification (this result is largely a reformulation of
topos-valid results I presented in [8], the missing ingredient there being
indeed the formulation of strong regularity developed in this article). The
construction of the compactification then allows to prove that every
compactification can be characterized as the minimal compactification
satisfying an extension property for an associated class of continuous maps
with compact regular co-domains, a fact that does not seem to have been
noticed explicitly before, or adequately emphasized. In point-free terms, this
property is a simple and natural one.

In Section 5 an open problem is presented. In classical set theory and toposes
one can define the compact regular reflection of a compactifiable locale [6,
7]. A natural question is then whether this result is also derivable in CST.
That this is not the case for the compact regular reflection in its full
generality follows by the proof in [10] that the compact _completely_ regular
reflection of a locale $L$ (Stone-Čech compactification of $L$) is independent
from CST, also when extended with (various principles, including) the
principle of dependent choice DC. However, one can construct in CST the
compact completely regular reflection of a locale $L$ for a wide class of
locales, and the locales for which this reflection is definable can be
characterized [8]. So the question naturally arises whether analogous results
may be obtained for the compact regular reflection. This appears to be an
interesting open problem in CST.

This article has been written having in mind a reader familiar with locale
theory, and possibly toposes, but not necessarily with CST. Constructive Set
Theory is a subtheory of classical set theory, so the adopted formalism and
many constructions are the familiar ones of classical mathematics. CST uses
however principles (provable in classical set theory) with which the reader
may not be familiar. For this reason, I included in Section 1 an informal
presentation of the principles of CST to be exploited, focusing on those that
differ the most from the standard classical ones (the formal system for CST is
recalled in Appendix 6). In particular, the needed principles for inductive
and coinductive definitions of sets are recalled; as examples of applications
of these principles the inductive definition of the set of finite subsets of
given set $X$, and the coinductive definition of the largest interpolative
relation $R_{0}$ contained in a relation $R$, are presented.

An ambition of this article is to show how avoiding non-constructive set
existence principles as Powerset and unrestricted Separation, inductive and
coinductive definitions emerge as natural tools, that can be exploited for
obtaining more explicit and informative constructions.

##  1\. Informal Constructive Set Theory

The intended audience of this paper includes readers with some familiarity
with locale theory and intuitionistic logic (topos logic), but not necessarily
with CST. In this section I give an informal presentation of the principles of
constructive set theory to be exploited that may be unfamiliar to such a
reader. The last section contains a formal description of the axiom system(s)
for CST. The reader is referred to [4] for a thorough introduction to the
subject.

In the ordinary mathematical practice, one is rarely faced with the problem of
showing that a certain collection of mathematical objects is a set. This is
due to the fact that classical set theory, as well as the internal set
theories of toposes, have strong set existence principles that trivially imply
that the collections under consideration are indeed sets. For instance, given
a set $X$, in those contexts one considers the discrete topology on $X$ which
is given by the class $\textsf{Pow}(X)$ of subsets of $X$. There is no need of
a proof that such a class is a set, since the Powerset Axiom exactly ensures
that this is the case. The Powerset Axiom, as the unrestricted Separation
axiom (see below), allow for circular non-constructive definitions, that are
rejected in contexts which adopts (intuitionistic logic and) a constructive
concept of set. In such constructive contexts, proving that a certain
construction yields a set, rather than a mere class is, in general, much more
demanding.

Constructive Set Theory, the setting of this article, is a subtheory of
classical set theory, in particular the usual set-theoretical language and
notation is adopted in this context. Several of the CST axioms and schemes, as
the Union or Pairing or Infinity axioms, are familiar ZF axioms (cf. Appendix
6), so we here concentrate on those principles of CST that we shall exploit in
the following, and that might be unfamiliar to the reader. Note that all such
principles are provable in classical set theory.

As in classical set theory, given any formula $\phi$, one has the class
$\\{x:\phi(x)\\}$ of elements satisfying $\phi$. For instance, given any set
or class $X$, one has the class $\textsf{Pow}(X)=\\{x:x\subseteq X\\}$ of
subsets of $X$. As already mentioned, in CST we do not have the Powerset
axiom, so even when $X$ is a set, if it is not empty, one will not be able to
deduce that the class $\textsf{Pow}(X)$ is a set.

Another principle of classical set theory that is not available in its full
form in CST is the Separation axiom:

for every formula $\phi$ and any set $A$, there is a set $X$ such that

$X=\\{x\in A:\phi(x)\\}$.

In CST, this principle is replaced by Restricted Separation:

for every restricted formula $\phi$ and any set $A$, there is a set $X$ such
that

$X=\\{x\in A:\phi(x)\\}$,

where a formula $\phi$ is _restricted_ if the quantifiers that occur in it (if
any) are of the form $\forall x\in B$, $\exists x\in C$, with $B,C$ sets.

Note that the lack of full Separation, implies that one may have in CST a
subclass of a set that need not be a set, precisely subclasses of a set $A$ of
the form $C=\\{x\in A:\phi(x)\\}$ where $\phi$ is not restricted. Thus, the
notation $U\subseteq X$ merely says that $U$ is a possibly proper subclass of
$X$, while $U\in\textsf{Pow}(X)$ expresses the fact that $U$ is a subset of
$X$, as $\textsf{Pow}(X)$ is the class of subsets of $X$.

Another principle to be exploited that might not be familiar to the reader is
the Strong Collection axiom. Strong Collection is a strengthening of the more
familiar ZF axiom of Replacement, stating that if $f:A\to C$ is a function
from a set $A$ to a class $C$, the image of $A$ under $f$ is a set.

Strong Collection states, more generally, that if $A$ is a set and $\phi(x,y)$
is a formula such that $(\forall x\in A)\exists y\phi(x,y)$, then there is a
set $B$ such that

$\displaystyle(\forall x\in A)(\exists y\in B)\phi(x,y)\ \&\ (\forall y\in
B)(\exists x\in A)\phi(x,y).$

Note that from Replacement it follows that if $A$ is a set, $f:A\to C$ a
function, then $f=\\{(x,f(x)):x\in A\\}$ is a set.

A key role in CST, and specifically in this article, is played by inductive
and co-inductive definitions. An _inductive definition_ is any class $\Phi$ of
pairs. A class $A$ is called _$\Phi-$ closed_ if:

$(a,X)\in\Phi$, and $X\subseteq A$ implies $a\in A$.

CST enjoys the _class induction property_ :

for each class of pairs $\Phi$, there is a smallest $\Phi-$closed class
$I(\Phi)$; i.e., there is a class $I(\Phi)$ such that:

$1.$ $I(\Phi)$ is $\Phi-$closed, and

$2.$ if the class $A$ is $\Phi-$closed then $I(\Phi)\subseteq A$.

As an example, we construct inductively the class of _finite subsets_ of a
class $C$. Following Kuratowski, we define $\textsf{Pow}_{fin}(C)$ to be the
class $I(\Phi_{fin})$, with

$\Phi_{fin}=\\{(\emptyset,\emptyset)\\}\cup\\{(U\cup\\{y\\},\\{U\\}):U\in\textsf{Pow}(C),y\in
C\\}.$

A class $X$ is then $\Phi_{fin}-$closed if: $X$ contains the empty set; if $X$
contains a subset $U$ of $C$, it also contains the subset $U\cup\\{y\\}$, for
every $y\in C$.

A class $K$ is a _bound_ for the inductive definition $\Phi$ if, for every
$(x,X)\in\Phi$, there is a set $A\in K$ and an onto mapping $f:A\to X$. An
inductive definition $\Phi$ is defined to be _bounded_ if:

1\. $\\{x\mid(x,X)\in\Phi\\}$ is a set for every $X$;

2\. $\Phi$ is bounded by a set.

The system for CST we adopt satisfies the Bounded Induction Scheme (BIS):

For each bounded class of pairs $\Phi$, the class $I(\Phi)$ is a set. In
particular, if $\Phi$ is a set, $I(\Phi)$ is a set.

As an example, using BIS we may prove that when $S$ is a set,
$\textsf{Pow}_{fin}(S)$ is a set. Indeed, $\Phi_{fin}$ is bounded by the set
$K=\\{\emptyset,\\{\emptyset\\}\\}$, and
$\\{x\mid(x,X)\in\Phi_{fin}\\}=\\{\emptyset\\}\cup\bigcup_{y\in
S}\\{X\cup\\{y\\}\\}$ is a set for every subset $X$ of $S$ (since the union of
set-indexed family of sets is a set, cf. Section 6).

By induction on $\textsf{Pow}_{fin}(X)$, one may also prove that any
$a\in\textsf{Pow}_{fin}(X)$ is the range of a (not necessarily one-one)
function $f:n\to a$, for some $n\in\mathbb{N}$: one considers the class
$\\{u\in\textsf{Pow}_{fin}(X):(\exists n\in\mathbb{N})(\exists
f)f:\textbf{n}\twoheadrightarrow u\\}$, n the set with $n$ elements, and
concludes showing that this class is $\Phi_{fin}-$closed.

Given an inductive definition $\Phi$ on a set $S$, i.e of the form
$\Phi\subseteq S\times\textsf{Pow}(S)$, a class $C\subseteq S$ is said to be
$\Phi-$_inclusive_ if $C\subseteq\Gamma_{\Phi}(C)$, with

$\Gamma_{\Phi}(C)=\\{x\ \mid\ (\exists X)\ (x,X)\in\Phi\ \&\ X\subseteq C\\}.$

CST has _the class co-induction property_ :

the class $C(\Phi)=\bigcup\\{Y\in\textsf{Pow}(S)\ \mid\
Y\subseteq\Gamma_{\Phi}(Y)\\}$ is the largest $\Phi-$inclusive subclass of
$S$, the class co-inductively defined by $\Phi$.

In our system for CST the following principle is available.

Set Coinduction Scheme (SCS): when $S,\Phi$ are sets, $C(\Phi)$ is a set.

As an example, we show that one can construct coinductively the largest
interpolative relation contained in a given binary set-relation on a set. This
construction will be exploited in the definition of strong regularity to be
introduced.

######  Lemma 1.1.

Let $A$ and $R$ be sets, $R$ a binary relation on $A$, $R\subseteq A\times A$.
Then the largest interpolative relation $R_{0}$ contained in $R$ is a set.

###### Proof.

Let $R_{0}=\bigcup\\{Y\in\textsf{Pow}(R):(\forall x,y)[(x,y)\in Y\to(\exists
z\in A)(x,z)\in Y\ \&\ (z,y)\in Y]\\}$ the union of all interpolative set-
relations contained in $R$. A priori, this definition only defines a class. We
now prove that $R_{0}$ can be constructed as the set co-inductively defined by
an inductive definition. Let $\Phi$ be the inductive definition

$\\{((x,z),\\{(x,y),(y,z)\\}):\\{(x,z),(x,y),(y,z)\\}\subseteq R\\}.$

Note that $\Phi$ is a set since $R$ is, so that the largest $\Phi-$inclusive
class $C(\Phi)=\bigcup\\{Z\in\textsf{Pow}(R):Z\ \Phi\textrm{-inclusive}\\}$ is
a set by the SCS. We conclude showing that $R_{0}=C(\Phi)$: let $Y$ be an
interpolative relation contained in $R$. To show that $Y\subseteq C(\Phi)$ one
just need to show that $Y$ is $\Phi-$inclusive: Let $(x,y)\in Y$. Then there
is $z\in A$ such that $(x,z)\in Y\ \&\ (z,y)\in Y$. Since $Y\subseteq R$, we
conclude that $Y$ is $\Phi-$inclusive. To prove the converse, i.e. that
$C(\Phi)\subseteq R_{0}$, since $C(\Phi)$ is a set, it is enough to prove that
$C(\Phi)$ is interpolative. Let $(x,y)\in C(\Phi)$. Then there is
$Z\in\textsf{Pow}(R)$, $Z$ $\Phi-$inclusive, with $(x,y)\in Z$. There is thus
$X$ such that $((x,y),X)\in\Phi\ \&\ X\subseteq Z$. Therefore, an element
$z\in A$ exists such that $(x,z)\in R$, $(z,y)\in R$, and $(x,z)\in Z$,
$(z,y)\in Z$. Since $Z\subseteq C(\Phi)$ we conclude that $C(\Phi)$ is
interpolative. ∎

Contrary to what one might expect, this result will not suffice for a
constructive definition of the concept of strong regularity. Further work will
be needed, in particular involving the application of a principle of CST
called Relation Reflection Scheme, again provable from the ZF axioms.

Relation Reflection Scheme, RRS:

  * For classes $S,R$ with $R\subseteq S\times S$, if $a\in S$ and $\forall x\in S\ \exists y\in S\ R(x,y)$ then there is a set $S_{0}\subseteq S$ such that $a\in S_{0}$ and $\forall x\in S_{0}\ \exists y\in S_{0}\ R(x,y)$.

##  2\. Locales constructively

We assume familiarity with the theory of frames (locales) [12]. In this
section we illustrate how the notions we shall need are formulated in the
present constructive context. Let $X$ be a set. As already noted, the complete
lattice $\Omega(X)$ of open subsets of $X$ endowed with the discrete topology
is the power class of $X$, $\textsf{Pow}(X)$. This example shows that,
constructively, we cannot expect a frame to be carried by a set of elements.
The definition of set-generated frame/locale to be recalled is the version of
the frame/locale concept adopted in constructive set theory.

A pair of classes $(L,\leq)$, with $\leq$ a partial order on $L$, is a _class
locale_ (or class frame) if every finite subset of $L$ has a least upper bound
(meet), every subset has a greatest lower bound (join), and if the following
infinite distributive law is satisfied:

$x\wedge\bigvee U=\bigvee_{y\in U}(x\wedge y)$

for all $x\in L$, $U\in\textsf{Pow}(L)$. A class-locale $L$ is said to be
_set-generated_ by a set $B_{L}\subseteq L$ if, for every $x\in L$,

  * $i.$

the class $D_{x}=\\{b\in B_{L}:b\leq x\\}$ is a set,

  * $ii.$

$x=\bigvee D_{x}$.

$B_{L}$ is called a _basis_ of $L$. In a fully impredicative context as
classical set theory or the internal language of a topos, set-generated class-
locales and ordinary locales come to the same thing.

In the following, a set-generated class-locale $(L,B_{L})$ will simply be
referred to as a _locale_ $L$, sometimes omitting the explicit mention of the
basis $B_{L}$. Note that if $(L,B_{L})$ is set-generated, by Restricted
Separation (Section 1) the restriction of $\leq$ to $B_{L}\times B_{L}$ is a
set: $\leq\cap B_{L}\times B_{L}=\\{(a,b)\in B_{L}\times B_{L}:a\in D_{b}\\}$.
Also, if $B_{L}$ is a basis of $L$, and $B^{\prime}_{L}\subseteq L$ is a set
such that $B_{L}\subseteq B^{\prime}_{L}$, then $B^{\prime}_{L}$ also is a
basis for $L$, as is easy to verify again using Restricted Separation.

A _continuous map_ of locales $f:L\to M$ is a function $f^{-}:B_{M}\to L$
(note the reverse direction) satisfying:

  * 1.

$\bigvee_{a\in B_{M}}f^{-}(a)=1=\bigvee B_{L}$,

  * 2.

$f^{-}(a)\wedge f^{-}(b)=\bigvee\\{f^{-}(c):c\in B_{M},c\leq a,c\leq b\\}$,
for all $a,b\in B_{M}$,

  * 3.

$f^{-}(a)\leq\bigvee_{b\in U}f^{-}(b)$, for all $a\in
B_{M},U\in\textsf{Pow}(B_{M})$ with $a\leq\bigvee U$.

The (in general proper) class of these maps is denoted by
$Hom_{\textrm{Loc}}(L,M)$. Observe that $Hom_{\textrm{Loc}}(L,M)$ is in a one-
to-one correspondence with the collection of frame homomorphisms from $M$ to
$L$, i.e., class functions from $M$ to $L$ preserving the frame structure:
given $f:L\to M$, one extends $f^{-}:B_{M}\to L$ to $M$ by letting for $a\in
M$, $f^{-}[a]=\bigvee\\{f^{-}(b):b\in B_{L},b\leq a\\}$. Trivially, for $b\in
B_{M}$, $f^{-}[b]=f^{-}(b)$. Note in particular that $f^{-}$ preserves meets
and joins that exist in $B_{M}$. Composition $f\circ g:L\to N$ of two
continuous maps $f:M\to N$ and $g:L\to M$ is defined as $(f\circ g)^{-}:N\to
L$, $(f\circ g)^{-}(a)=\bigvee\\{g^{-}(x):x\in B_{M}\ \&\ x\leq
f^{-}(a)\\}=g^{-}[f^{-}(a)]$.

A locale mapping $f:L\to M$ is _dense_ if, for $a\in M$, $f^{-}[a]=0$ implies
$a=0$; $f$ is an embedding (or a sublocale) if $f^{-}[\cdot]$ is onto,
equivalently, if for every $a\in L$ there is $U\in\textsf{Pow}(B_{M})$ such
that $\bigvee_{b\in U}f^{-}(b)=a$.

A locale $L$ is _compact_ iff every covering of $1=\bigvee B_{L}$ by basic
elements (i.e., every $U\in\textsf{Pow}(B_{L})$ such that $1=\bigvee U$) has a
finite subcover. $L$ is _regular_ if, for all $a\in B_{L}$, $a=\bigvee\\{b\in
B_{L}:b\prec a\\}$, where, for $x,y\in L$, $y\prec x\iff 1=x\vee y^{*}$, with
$y^{*}=\bigvee\\{c\in B_{L}:c\wedge y=0\\}$ the _pseudocomplement_ of $y$.

Note that we could not define, as in the classical or topos-theoretic context,
a locale to be regular if $x\leq\bigvee\\{y\in L:y\prec x\\}$, for all $x\in
L$. Indeed, the class $\\{y\in L:y\prec x\\}$ need not be constructively a
set, so that its join need not exist. It is easy however to see that the given
definition is in the classical/topos theoretic context equivalent to the
standard one. Similar considerations apply to the definition of compactness,
and of the separation properties recalled below.

We shall need the following well-known facts.

######  Lemma 2.1.

$i.$ If $f:L\to M$ is a dense embedding, $f^{-}[\cdot]:M\to L$ preserves
pseudocomplements. $ii.$ If $f:L\to M$ is a dense continuous map, $L$ is
compact and $M$ is regular, then $f^{-}[\cdot]:M\to L$ is one-one. $iii.$ If
$h:L\to M$, $f,g:M\to N$ are continuous maps with $h$ dense, $N$ regular, and
$f\circ h=g\circ h$, then $f=g$.

###### Proof.

$i.$ For every $a$ in $M$, one has $f^{-}[a^{*}]=\bigvee\\{f^{-}(x):x\in
B_{M}\ \&\ x\wedge a=0\\}\leq f^{-}[a]^{*}$; for the converse, let $b\in M$ be
such that $f^{-}[b]=f^{-}[a]^{*}$. By density, $f^{-}[b\wedge
a]=f^{-}[b]\wedge f^{-}[a]=0$ implies $b\wedge a=0$, so that $b\leq a^{*}$,
and $f^{-}[b]=f^{-}[a]^{*}\leq f^{-}[a^{*}]$.

$ii.$ We first prove that $f^{-}[\cdot]:M\to L$ is co-dense, i.e. that, for
$a\in M$, $f^{-}[a]=1$ implies $a=1$. Indeed, $a=\bigvee\\{x\in B_{M}:x\prec
a\\}=\bigvee\\{x\in B_{M}:(\forall b\in B_{M})b\in D_{(x^{*}\vee a)}\\}$.
Then, $f^{-}[a]=1=\bigvee\\{f^{-}(x):x\in B_{M}\ \&\ x\prec a\\}$. By
compactness of $L$ there is a finite subset $u$ of $B_{M}$ such that
$f^{-}[\vee u]=1$ and $\vee u\prec a$. Since $f^{-}[\vee u^{*}]\leq f^{-}[\vee
u]^{*}=0$, by density $\vee u^{*}=0$, so that $a=\vee u^{*}\vee a=1$.

Now let $a,b\in M$ be such that $f^{-}[a]=f^{-}[b]$. If $x\in B_{M}$ is such
that $x\prec a$, i.e. $x^{*}\vee a=1_{M}$, then $1_{L}=f^{-}[x^{*}\vee
a]=f^{-}[x^{*}]\vee f^{-}[a]=f^{-}[x^{*}]\vee f^{-}[b]=f^{-}[x^{*}\vee b]$.
Since $f^{-}$ is codense, this gives $x^{*}\vee b=1_{M}$, i.e. $x\prec b$.
Thus, $x\prec a\iff x\prec b$ for all $x\in B_{M}$, and since by regularity
for every $a\in M$, $a=\bigvee\\{x\in B_{M}:x\prec a\\}$, we conclude $a=b$.

$iii.$ We have to show that if $h^{-}[f^{-}(c)]=h^{-}[g^{-}(c)]$ for all $c\in
B_{N}$, then $f^{-}=h^{-}$. By regularity of $N$, for every $c\in B_{N}$,
$c=\bigvee\\{b\in B_{N}:b\prec c\\}$. If $b\prec c$ one has $b^{*}\vee c=1$,
so that $g^{-}[b^{*}\vee c]=g^{-}[b^{*}]\vee g^{-}(c)=1$. Then,

$f^{-}(b)=f^{-}(b)\wedge(g^{-}[b^{*}]\vee g^{-}(c))=(f^{-}(b)\wedge
g^{-}[b^{*}])\vee(f^{-}(b)\wedge g^{-}(c)).$

On the other hand, since $f\circ h=g\circ h$,

$h^{-}[f^{-}(b)\wedge g^{-}[b^{*}]]=h^{-}[f^{-}(b)]\wedge
h^{-}[g^{-}[b^{*}]]=h^{-}[f^{-}(b)]\wedge
h^{-}[f^{-}[b^{*}]]=h^{-}[f^{-}[b\wedge b^{*}]]=0,$

and since $h$ is dense, we get $f^{-}(b)\wedge g^{-}[b^{*}]=0$. Together with
the above, this gives $f^{-}(b)=f^{-}(b)\wedge g^{-}(c)$, whence
$f^{-}(b)\leq[g^{-}(c)]$ for all $b\prec c$. Therefore, $f^{-}(c)\leq
g^{-}(c)$, and symmetrically $g^{-}(c)\leq f^{-}(c)$. ∎

Compared with regularity, a constructive concept of complete regularity
requires some more work. The standard definition of complete regularity for
locales demands that for every $x$ in $L$, $x\leq\bigvee\\{y\in L:y\prec\prec
x\\}$, where $y\prec\prec x$, $y$ really inside (or completely below) $x$, if
there is a scale from $y$ to $x$. A map $s:\mathbb{I}:\to L$ from the rational
unit interval $\mathbb{I}$ to $L$ is called a _scale_ from $y$ to $x$ if
$s(0)=y,s(1)=x$ and, for $p<q$, $s(p)\prec s(q)$.

In this case we have the additional difficulty that, even restricting to basic
elements as we did in redefining regularity, we still not have that $\\{b\in
B:b\prec\prec a\\}$ is a set, because, by contrast with $\prec$, the really
inside relation $\prec\prec$ is not a set when restricted to $B\times B$ (as
the class of scales is not a set). This difficulty is circumvented as follows.

A locale $L$ will be defined _completely regular_ if a family
$ri:B\to\textsf{Pow}(B)$ of subsets of $B$ exists such that _i._ for all $a\in
B$, $a=\bigvee ri(a)$, and _ii._ for all $b\in ri(a)$ a scale exists from $b$
to $a$. The idea is that, given a basic element $a$, one does not try to
construct the set of all basic elements $b$ for which a scale exists from $b$
to $a$; to be able to establish that $L$ completely regular, it will suffice
to have a set of such elements that is sufficiently rich to cover $a$.

As said for regularity, it is not difficult to verify that this concept is
classically (or topos-theoretically) equivalent to the standard one, as well
as that this notion allows for the derivation of standard desirable properties
of complete regularity: it is hereditary, invariant under isomorphisms, and
allows to derive Tychonoff embedding theorem [11].

The given constructive definition of complete regularity circumvents the use
of the really inside relation. However, this relation enjoys the important
interpolation property that is in particular useful in the construction of
completely regular compactifications. It is possible to reconstruct a
satisfactory set-analogue of the really inside relation, satisfying the
interpolation property, adding enough scales to the basis as follows.

For $a,b\in B$, let $b\prec\prec_{B}a$ iff a scale of basic elements exists
from $b$ to $a$. Note that this relation is interpolative on $B$. We say that
$L$ has a completely regular basis $B$ if, for all $a\in B$, $a=\bigvee\\{b\in
B:b\prec\prec_{B}a\\}$.

Of course, a locale with a completely regular basis is completely regular. For
the converse the following holds true.

######  Lemma 2.2.

If $(L,B)$ is a completely regular locale, then $L$ has a completely regular
basis.

###### Proof.

By definition of complete regularity, for every pair $a,b$ such that $b\in
ri(a)$ a scale of elements of $L$ exists from $b$ to $a$. We may then apply
Strong Collection (Section 1) to collect a set $V^{\prime}$ of scales so that
for all $a,b\in B$ such that $b\in ri(a)$ there is a scale $s:\mathbb{I}:\to
L$ in $V^{\prime}$ from $b$ to $a$, and conversely for all $s:\mathbb{I}:\to
L$ in $V^{\prime}$ there are $a,b\in B$ such that $s:\mathbb{I}:\to L$ is a
scale from $b$ to $a$. Let $V$ be the set of elements of $L$ that belong to a
scale in $V^{\prime}$, $V=\bigcup_{s\in V^{\prime}}\textrm{Range}(s)$. Since
$V$ is a set, we can construct a new basis $B^{\prime}=B\cup V$ for $L$. To
prove that $B^{\prime}$ is a completely regular base, i.e. that for all $u\in
B^{\prime}$, $u=\bigvee\\{v\in B^{\prime}:u\prec\prec_{B^{\prime}}u\\}$, note
that we have, for all $u\in B^{\prime}$, $u=\bigvee\\{x\in B:(\exists b\in
B)b\in D_{u}\ \&\ x\in ri(b)\\}$. Since for every $c\in ri(b)$ there is in
$B^{\prime}$ a scale from $c$ to $b$, we have $u=\bigvee\\{c\in B:(\exists
b\in B)b\leq u\ \&\ c\prec\prec_{B^{\prime}}b\\}$, and a fortiori
$u=\bigvee\\{v\in B^{\prime}:(\exists b\in B)b\leq u\ \&\
v\prec\prec_{B^{\prime}}b\\}$. But if $v\prec\prec_{B^{\prime}}b$ for $b\leq
u$, then also $v\prec\prec_{B^{\prime}}u$: given the scale $s:\mathbb{I}:\to
L$ from $v$ to $b$, replace $s(1)=b$ with $s(1)=u$ to get a scale from $v$ to
$u$. ∎

An important property of completely regular bases is that any extension of a
completely regular basis is again a completely regular basis.

##  3\. Strong Regularity

As is well-known [12], in a compact regular locale the well-inside relation
interpolates. Then, if the principle of countable dependent choice (DC) is
available, whenever $x\prec y$, a scale from $x$ to $y$ can be
constructed111This holds for systems as ZF or the internal logic of toposes.
In CST, due to the absence of Powerset, a stronger version of the axiom of
Dependent Choice, the axiom of Relativized Dependent Choice, RDC (see e.g. [4]
for this principle) is needed. If the locale is compact and regular, DC
suffices for the construction of a scale, since Lemma 3.3 below ensures that
the element $z$ such that $x\prec z\prec y$ belongs to a set (a base), rather
than a class.. Thus, assuming DC, a compact regular locale is completely
regular. In [7] Banaschewski and Pultr note that this result may fail to hold
in toposes that do not validate DC. For resolving this and related
difficulties, they introduce strongly regular locales.

Banaschewski and Pultr begin by noting that any binary relation $R$ contains a
largest interpolative relation. Indeed, as the union of any set of
interpolative relations is an interpolative relation, defining $R_{0}$ to be
the union of all interpolative relations contained in $R$ will yield the
largest interpolative relation contained in $R$. Taking $R=\prec$ one thus
obtains the largest interpolative relation $\prec_{0}$ contained in the well-
inside relation. A locale $L$ is then defined strongly regular if
$x\leq\bigvee\\{y\in L:y\prec_{0}x\\}$, for all $x\in L$.

Unfortunately, this definition, albeit adequate to the choice-free context of
toposes, is impredicative or circular: $R_{0}$ is indeed itself an
interpolative relation contained in $R$, so that it belongs to the collection
of interpolative relations of which it is the union. Note that Banaschewski
and Pultr definition implicitly requires $\textsf{Pow}(R)$, the class of
subsets of $R$, to be a set. In the present constructive setting, defining
$R_{0}=\bigcup\\{R^{\prime}\in\textsf{Pow}(R):R^{\prime}\
\textrm{interpolative}\\}$ a priori only yields a proper class, since
$\textsf{Pow}(R)$ cannot be proved to be a set in CST when $R$ is not empty
[10].

Exploiting the Set Coinduction Scheme and the Relation Reflection Scheme
(Section 1), in this section I present an alternative method for defining
strong regularity, that is both non-circular and adequate to a choice-free
intuitionistic setting.

On a locale $L$, let the class

$\prec_{0}=\bigcup\\{R\in\textsf{Pow}(\prec):(\forall x,y)[R(x,y)\to(\exists
z\in L)R(x,z)\ \&\ R(z,y)]\\}$

be the union of all interpolative set-relations contained in the well-inside
relation $\prec$ on $L$. Note again that $\prec_{0}$ is a class, so that it
need not belong to $\textsf{Pow}(\prec)$. Similarly to what has been said
before for regularity and complete regularity, one cannot define $L$ to be
strongly regular if $x\leq\bigvee\\{y\in L:y\prec_{0}x\\}$ for all $x\in L$,
since the class $\\{y\in L:y\prec_{0}x\\}$ is not a set in general. Again, we
circumvent the problem by defining $L$ to be _strongly regular_ if a family
$si:B\to\textsf{Pow}(B)$ of subsets of $B$ exists such that

_i._ for all $a\in B$, $a=\bigvee si(a)$, and

_ii._ if $b\in si(a)$, then $b\prec_{0}a$.

Trivially, in the classical and topos-theoretic context, $L$ is strongly
regular according to the Banaschewski and Pultr notion if and only if it is
strongly regular for this definition. Also, one has that a completely regular
locale in the sense of the previous section is strongly regular (just let
$si(a)=ri(a)$ for all $a\in B$). Conversely, assuming the axiom of
(relativized) dependent choice, one proves that a strongly regular locale is
completely regular, with $ri(a)=si(a)$ for all $a\in B$ (cf. note 1).

As for complete regularity, this definition is however not completely
satisfactory. It avoids the circularity in the definition of the largest
interpolative set-relation contained in $\prec$, but the important
interpolation property of this relation is lost. To recover this property we
shall argue as follows. First we construct a larger basis $B^{\prime}$
containing ‘enough interpolants’. Over this new basis, we then construct
coinductively the largest set-relation contained in the well-inside relation.
This construction is the analogue for strong regularity of the construction of
completely regular bases for completely regular locales.

Given a strongly regular locale $(L,B)$, let $S$ be the class

$\\{\\{x_{0},...,x_{n}\\}:n\in\mathbb{N}_{>0}\ \&\ x_{0},...,x_{n}\in L\ \&\
(\forall i<n)x_{i}\prec_{0}x_{i+1}\\}.$

Let $R\subseteq S\times S$ be defined by

$R(\\{x_{0},...,x_{n}\\},\\{y_{0},...,y_{m}\\})$ $\iff$

$x_{0}=y_{0}\ \&\ x_{n}=y_{m}\ \&\
\\{x_{0},...,x_{n}\\}\subseteq\\{y_{0},...,y_{m}\\}\ \&\ $

$\ \&\ (\forall k<n)(\exists k^{\prime}<m)\
x_{k}\prec_{0}y_{k^{\prime}}\prec_{0}x_{k+1}.$

We then have $(\forall l_{1}\in S)(\exists l_{2}\in S)R(l_{1},l_{2})$. Given a
pair $(c,b)\in S$, i.e. such that $c\prec_{0}b$, using the Relation Reflection
Scheme (Section 1) one has a set $S_{0}$ such that $S_{0}\subseteq S$, and

$(c,b)\in S_{0}\ \&\ (\forall l_{1}\in S_{0})(\exists l_{2}\in
S_{0})R(l_{1},l_{2}).$

Thus, for all pairs $(c,b)$ such that $c\in si(b)$ there is such a set
$S_{0}$. Let $SI=\\{(c,b):c\in si(b)\\}$. By Strong Collection (Section 1), a
set $V^{\prime}$ exists such that

$(\forall(c,b)\in SI)(\exists S_{0}\in V^{\prime})(c,b)\in S_{0}\subseteq S\
\&\ (\forall l_{1}\in S)(\exists l_{2}\in S)R(l_{1},l_{2})$

and

$(\forall S_{0}\in V^{\prime})(\exists(c,b)\in SI)(c,b)\in S_{0}\subseteq S\
\&\ (\forall l_{1}\in S)(\exists l_{2}\in S)R(l_{1},l_{2}).$

Let $V=\\{z\in L:(\exists S_{0}\in V^{\prime})(\exists l\in S_{0})z\in l\\}$.
Define $B^{\prime}=B\cup V$. Note that $B^{\prime}$ is a set, and a basis of
$L$.

Let then $\prec^{\prime}$ be the restriction of the well-inside relation to
$B^{\prime}\times B^{\prime}$, $\prec^{\prime}=\\{(y,x)\in B^{\prime}\times
B^{\prime}:1\leq x\vee y^{*}\\}$. The relation $\prec^{\prime}$ is a set: one
has $1\leq x\vee y^{*}\iff(\forall b\in B)b\in D_{(x\vee y^{*})}$. Since
$D_{(x\vee y^{*})}=\\{c\in B:c\leq x\vee y^{*}\\}$ is a set, as $L$ is set-
generated by $B$, by Restricted Separation (Section 1) we can conclude that
$\prec^{\prime}$ is a set. By Lemma 1.1, we can then construct the largest
interpolative set-relation $\prec_{0}^{\prime}$ contained in $\prec^{\prime}$.

######  Lemma 3.1.

Let $u,v,x,y\in B^{\prime}$. If $x\leq u\prec_{0}^{\prime}v\leq y$, then
$x\prec_{0}^{\prime}y$.

###### Proof.

Consider the relation $R=\\{(x,y)\in B^{\prime}\times
B^{\prime}:(\exists(u,v)\in B^{\prime}\times B^{\prime})x\leq
u\prec_{0}^{\prime}v\leq y\\}=\\{(x,y)\in B^{\prime}\times
B^{\prime}:(\exists(u,v)\in B^{\prime}\times B^{\prime})x\in D_{u}\ \&\
(u,v)\in\prec_{0}^{\prime}\ \&\ v\in D_{y}\\}$. By Restricted Separation $R$
is a set. Moreover, $R$ is interpolative and $R\subseteq\prec^{\prime}$. Since
$\prec_{0}^{\prime}$ is the largest relation with these properties,
$R=\prec_{0}^{\prime}$. ∎

We shall say that a locale $L$ has a _strongly regular basis_ $B$ if the
largest interpolative relation $\prec_{0}^{\prime}$ contained in the
restriction of the well-inside relation to $B$ is admissible, i.e. if, for all
$a\in B$, $a=\bigvee\\{b\in B:b\prec_{0}^{\prime}a\\}$. A locale with a
strongly regular basis is strongly regular. Conversely, the following obtains.

######  Proposition 3.2.

If $(L,B)$ is a strongly regular locale, then $L$ has a strongly regular basis
$B^{\prime}$. Moreover, any basis extending $B^{\prime}$ is strongly regular.

###### Proof.

We prove that the basis $B^{\prime}=B\cup V$ we have constructed is a strongly
regular basis for $L$. We have to show that for all $u\in B^{\prime}=B\cup V$,
$u=\bigvee\\{v\in B^{\prime}:v\prec_{0}^{\prime}u\\}$. Let $u\in B^{\prime}$.
Then $u=b\in B$, or $u\in V$.

In the first case, as $L$ is strongly regular, $b\leq\bigvee si(b)$. We show
that $si(b)\subseteq\\{v\in B^{\prime}:v\prec_{0}^{\prime}u\\}$. If $c\in
si(b)$ there is $S_{0}\in V^{\prime}$ such that

$(*)\ \ \ (c,b)\in S_{0}\ \&\ (\forall l_{1}\in S_{0})(\exists l_{2}\in
S_{0})R(l_{1},l_{2}).$

On $B^{\prime}$ consider the binary relation

$R^{\prime}(u,v)\iff(\exists\\{x_{0},...,x_{n}\\}\in S_{0})(\exists i)(\exists
j>i)x_{i}=u\ \&\ x_{j}=v.$

Note that $R^{\prime}(u,v)$ implies $u\prec^{\prime}v$, and that $R^{\prime}$
interpolates: assume $R^{\prime}(u,v)$, then, by $(*)$, there is $y$ such that
$R^{\prime}(u,y)$ and $R^{\prime}(y,v)$. As a consequence,
$R^{\prime}\subseteq\prec_{0}^{\prime}$, and since in particular
$R^{\prime}(c,b)$, we conclude $si(b)\subseteq\\{v\in
B^{\prime}:v\prec_{0}^{\prime}b\\}$, whence $b=\bigvee\\{v\in
B^{\prime}:v\prec_{0}^{\prime}b\\}$.

If, on the other hand, $u\in V$, then $u=\bigvee\\{b\in B:b\leq u\\}$. For
every $b\in B$ such that $b\leq u$, one has $b\leq\bigvee\\{v\in
B^{\prime}:v\prec_{0}^{\prime}b\\}$. Since then $u\leq\bigvee\\{v\in
B^{\prime}:(\exists b\in B)b\in D_{u}\ \&\ v\prec_{0}^{\prime}b\\}$, we
conclude observing that by the previous lemma $v\prec_{0}^{\prime}b\leq u$
implies $v\prec_{0}^{\prime}u$. ∎

This section ends with a proof that a compact regular locale is strongly
regular. This will be the consequence of the following lemma, to be often
invoked in Section 4. Given a locale $(L,B)$, we can always extend its basis
$B$ to a basis $B^{*}$ that is (a set and) a sub-pseudocomplemented
distributive lattice of $L$, as follows. $B^{*}$ is defined inductively by the
following clauses:

  * if $b\in B$ then $b\in B^{*}$;

  * if $u\in B^{*}$ then $u^{*}\in B^{*}$;

  * if $V$ is a finite subset of $B^{*}$, then $\wedge V,\ \vee V\in B^{*}$,

where $\wedge,\vee,$ and ∗ are the operations in $L$. In other terms, $B^{*}$
is generated by the inductive definition

$\displaystyle\Phi_{B^{*}}$ $\displaystyle=\\{(b,\emptyset):b\in
B\\}\cup\\{(u^{*},\\{u\\}):u\in L\\}\cup$ $\displaystyle\cup\\{(\wedge
V,V):V\in\textsf{Pow}_{fin}(L)\\}\cup\\{(\vee
V,V):V\in\textsf{Pow}_{fin}(L)\\}$

Since this inductive definition is bounded, $B^{*}=I(\Phi_{B^{*}})$ is a set
(Section 1).

The following lemma is proved in [9]. The proof is reformulated here for the
reader’s convenience.

######  Lemma 3.3.

Let $L$ be a compact regular locale, $P$ a set, a sub-lattice and a basis of
$L$. Assume, for $b\in L$, $U\in\textsf{Pow}(P)$, that $b\prec\bigvee U$. Then
$b=0$, or finite subsets $\\{p_{1},...,p_{n}\\}$,
$\\{p^{\prime}_{1},...,p^{\prime}_{n}\\}$, and
$\\{p^{\prime\prime}_{1},...,p^{\prime\prime}_{n}\\}$ of $P$ exist with
$p_{i}\prec p^{\prime}_{i}\prec p^{\prime\prime}_{i}$,
$p^{\prime\prime}_{i}\in U$, and such that

$b\leq\vee p_{i}\prec\vee p^{\prime}_{i}\prec\bigvee U.$

###### Proof.

Since $L$ is regular, and since $P$ is a basis, by $b\prec\bigvee U$, one
obtains $1=b^{*}\vee\bigvee\\{p\in P:(\exists p^{\prime\prime}\in U)(\exists
p^{\prime}\in P)p^{\prime}\prec p^{\prime\prime},\ p\prec p^{\prime}\\}$. By
compactness, thus, $1=\vee s_{0}$, with $s_{0}\in\textsf{Pow}_{fin}(P)$ a
finite subset of $\\{b^{*}\\}\cup\\{p\in P:(\exists p^{\prime\prime}\in
U)(\exists p^{\prime}\in P)p^{\prime}\prec p^{\prime\prime},\ p\prec
p^{\prime}\\}$. By induction on $\textsf{Pow}_{fin}(P)$ (Section 1),
$s_{0}=u_{0}\cup v_{0}$, with $u_{0}\subseteq\\{b^{*}\\},v_{0}\subseteq\\{p\in
P:(\exists p^{\prime\prime}\in U)(\exists p^{\prime}\in P)p^{\prime}\prec
p^{\prime\prime},\ p\prec p^{\prime}\\}$, and both finite. Then $b\leq\vee
v_{0}$. Again by induction, $v_{0}$ is either empty or inhabited. In the first
case $b=0$; in the second, let $v_{0}=\\{p_{1},...,p_{n}\\}$ be an enumeration
of $v_{0}$ (Section 1). Thus, $b\leq\vee\\{p_{1},...,p_{n}\\}$. For all $i\leq
n$, there are $y\in P$ and $z\in U$ such that $p_{i}\prec y\prec z$. Using
induction on the length $n$ of the enumeration of $v_{0}$ (see also [4, Lemma
8.2.8], provable choice for finite sets), one constructs the required subsets
$\\{p^{\prime}_{1},...,p^{\prime}_{n}\\}$,
$\\{p^{\prime\prime}_{1},...,p^{\prime\prime}_{n}\\}$. ∎

In particular, if for $a,b\in P$ one has $b\prec a$, then there are $p,q\in P$
with $b\leq p\prec q\prec a$. Therefore, $P$ is a strongly regular basis for
$L$.

##  4\. Compact regular compactifications

In contexts as toposes or constructive set theory, in which the principle of
Dependent Choice is not assumed, compact regular compactifications do not
coincide with compact completely regular compactifications. In this section we
deal with compactifications of the first type. Part of the material in this
section, formulated for the topos-theoretic context, is presented in [9]. It
is here reproduced in a version adequate to constructive set theory.

A compact regular compactification of a locale $L$, in the following simply a
compactification, is a dense embedding $k:L\to M$, with compact regular co-
domain. Exploiting the coinductive formulation of strong regularity derived in
the previous section, we shall show how, given a compactifiable locale $L$,
and any set-indexed family of locale mappings
${\cal{F}}\equiv\\{f_{i}\\}_{i\in I}$, $f_{i}:L\to L_{i}$, with compact and
regular co-domain, a compactification $\gamma L$ of $L$ can be constructed
with the property that each function in ${\cal{F}}$ has a unique extension to
$\gamma L$.

The construction of the compactification to be presented will then alow us to
show that any compactification can be characterized in terms of its ability of
extending continuous functions with compact regular codomain, an aspect of
compactifications that does not seem to have been emphasized before. The
relation of these results with the compact regular reflection of $L$ (the
‘weak’ Stone-Čech compactification) is discussed in the next section.

As a compact regular locale is strongly regular, and since, as is easy to
verify, strong regularity is hereditary (if $(L,B_{s})$ is a strongly regular
locale with strongly regular basis $B_{s}$, and $f:L^{\prime}\to L$ is an
embedding, $B^{\prime}_{s}=\\{f^{-}(b):b\in B_{s}\\}$ is a strongly regular
basis for $L^{\prime}$), a compactifiable locale must be strongly regular. We
now show that the converse also holds constructively.

In [5] Banaschewski showed that relations of strong inclusion on a frame $L$
may be used for defining the compactifications of that frame. The whole frame
structure is not needed for carrying out Banaschewski’s construction. In
particular, strong inclusions can be considered more generally over pcd-
lattices [9]. This fact is particularly relevant in a constructive context as
the present one, since, while in such a context a (non-trivial) frame is
carried by a proper class, a pcd-lattice may well be carried by a set. Recall
in particular from the previous section that every set $B$ generating a frame
can be extended to a pcd-lattice $P=B^{*}$ that is a set; recall also that, as
noted earlier, the partial order restricted to any set of generators also is a
set.

In the following, by _pcd-lattice_ we mean a partial order $(P,\leq)$ with
$P,\leq$ sets, satisfying the standard axioms of a pseudo-complemented
distributive lattice. A strong inclusion on a pcd-lattice $P$ is a binary set-
relation $\lhd$ on $P$ satisfying:

1\. $0\lhd 0$, $1\lhd 1$;

2\. if $x\leq a\lhd b\leq y$ then $x\lhd y$;

3\. if $x\lhd a$, $x\lhd b$ then $x\lhd a\wedge b$;

4\. if $x\lhd a$, $y\lhd a$ then $x\vee y\lhd a$;

5\. if $a\lhd b$ then $b^{*}\lhd a^{*}$;

6\. $\lhd\subseteq\prec$;

7\. if $x\lhd y$ then $x\lhd z\lhd y$, for some $z\in P$.

Note that from 6. it follows $\lhd\subseteq\leq$. On every pcd-lattice $P$ the
well inside relation $\prec$ (is a set and) satisfies conditions $1$ to $6$,
while $\prec_{0}^{\prime}$ is a strong inclusion: that $\prec_{0}^{\prime}$ is
a set is due to Proposition 1.1; that it is a strong inclusion is proven as in
[7]: 1\. consider $R=\\{(0,0),(1,1)\\}$. $R$ is interpolative and contained in
$\prec$. Since $\prec_{0}^{\prime}$ is the largest such relation,
$\\{(0,0),(1,1)\\}\subseteq\prec_{0}^{\prime}$. 2\. Let $R=\\{(x,y)\in P\times
P:(\exists a\in P)(\exists b\in P)x\leq a\prec_{0}^{\prime}b\leq y\\}$. $R$ is
a set, interpolative and contained in $\prec$, so
$R\subseteq\prec_{0}^{\prime}$. Properties from 3 to 5 are proven similarly.
6. and 7. hold by definition.

If $P$ is a sub-pcd-lattice of a frame $L$, and $L$ is set-generated by $P$, a
strong inclusion $\lhd$ on $P$ is said to be compatible with $L$ if
$a=\bigvee_{L}\\{x\in P:x\lhd a\\}$, for all $a\in P$. The following lemma
provides a method for constructing strong inclusions on $P$.

######  Lemma 4.1.

Let $P$ be a pcd-lattice, and $R$ be an interpolating binary set-relation on
$P$ with $R\subseteq\prec$. The relation $\lhd_{R}$ defined inductively on $P$
as the least relation containing $R$ and closed under conditions 1-5 is a
strong inclusion on $P$.

###### Proof.

Let $\lhd_{R}=I(\Phi_{R})$, with

$\displaystyle\Phi_{R}$ $\displaystyle=\\{((x,y),\emptyset):(x,y)\in R\\}\cup$
$\displaystyle\cup\\{((0,0),\emptyset)\\}\cup\\{((1,1),\emptyset)\\}\cup$
$\displaystyle\cup\\{((x,y),\\{(a,b)\\}):x,y,a,b\in P,\ x\leq a,\ b\leq
y\\}\cup$ $\displaystyle\cup\\{((x,a\wedge b),\\{(x,a),(x,b)\\}):x,a,b\in
P\\}\cup$ $\displaystyle\cup\\{((x\vee y,a),\\{(x,a),(y,a)\\}):x,y,a\in
P\\}\cup$ $\displaystyle\cup\\{((b^{*},a^{*}),\\{(a,b)\\}):a,b\in P\\}.$

This inductive definition is a set, and so is bounded. Thus,
$\lhd_{R}=I(\Phi_{R})$ is a set. Obviously, $\lhd_{R}$ satisfies conditions
from 1 to 5. Indeed, assume for instance $x\leq a\lhd_{R}b\leq y$ as in
condition 2. Then, since $\lhd_{R}$ is $\Phi_{R}$-closed, also $x\lhd_{R}y$.

The proof of $6$ and $7$ is by induction. So, to prove 6, one shows that
$\prec$ is $\Phi_{R}$-closed. Since $\lhd_{R}$ is the least $\Phi_{R}$-closed
class, we conclude $\lhd_{R}\subseteq\prec$: the base cases ($(x,y)\in R$ and
1) are trivial (as $R\subseteq\prec$ by hypothesis); easy calculations show
that $\prec$ is closed for the other conditions in $\Phi_{R}$.

Proof of 7: we prove that the set $K=\\{(x,y)\in\lhd_{R}:(\exists z\in
P)(x,z)\in\lhd_{R}\ \&\ (z,y)\in\lhd_{R}\\}$ is $\Phi_{R}$-closed, so that it
must contain $\lhd_{R}$. The base cases are immediate. Now assume $x\leq
a,b\leq y$ for $x,y,a,b\in P$, and let $(a,b)\in K$. Then, by the proof that
condition 2 on strong inclusions holds, $(x,y)\in\lhd_{R}$ and
$x\lhd_{R}z\lhd_{R}y$, for some $z\in P$, so $(x,y)\in K$, as wished. The
closure for the other conditions in $\Phi_{R}$ is proved similarly, as a
further example we show that if $(x,a),(x,b)\in K$ then also $(x,a\wedge b)\in
K$: from $(x,a),(x,b)\in K$ we have
$x\lhd_{R}c_{1}\lhd_{R}a,x\lhd_{R}c_{2}\lhd_{R}b$ for some $c_{1},c_{2}\in P$.
Then, by 3 and 2 (and 6), $x\lhd_{R}c_{1}\wedge c_{2}\lhd_{R}a\wedge b$. ∎

Note that, for $R=\emptyset$, one gets the least strong inclusion on $P$:
$x\lhd_{\emptyset}y$ iff $x=0$ or $y=1$. Recall that an ideal in a join-
semilattice is a set $I$ such that

$i.$ $a\in I,b\leq a$ implies $b\in I$,

$ii.$ $u\subseteq I$ finite implies $\vee u\in I$.

A _round ideal_ of a pcd-lattice $P$ with a strong inclusion $\lhd$ is an
ideal $I$ such that for all $b\in I$ there is $a\in I$ with $b\lhd a$.

Ordered by inclusion, the class ${\cal R}(P)$ (or ${\cal R}(P,\lhd)$ when
confusion may arise) of such ideals is a class-frame, in fact a subframe of
the frame of ideals of $P$. Indeed, the meet of a finite set $F$ of round
ideals $\wedge F=\cap F$ is round, as is the join $\bigvee\cal U=\\{x\in
P:(\exists u\in\textsf{Pow}_{fin}(P))(\forall y\in u)(\exists I\in\cal U)(y\in
I)\ \&\ x\leq\vee u\\}$, for $\cal U\subseteq{\cal R}(P)$ a set of round
ideals.

Observe also that for all $a\in P$, $\Downarrow a\equiv\\{b\in P:b\lhd a\\}$
is a round ideal, and that the set $B_{d}=\\{\Downarrow a:a\in P\\}$ is a
basis of ${\cal R}(P)$. With this basis, $({\cal R}(P),B_{d})$ is a set-
generated frame.

In [5] Banaschewski proved that given a compatible strong inclusion on a frame
$L$, the locale map $h:L\to{\cal R}(L)$, with $h^{-}(I)=\bigvee I$, is a
compactification of $L$. The round ideal construction cannot be performed over
a non-trivial frame constructively (since a frame is carried by a proper
class, see also Section 5). Fortunately, the whole frame structure is not
needed for obtaining a compact regular locale.

######  Lemma 4.2.

Given a pcd-lattice $P$ and a strong inclusion $\lhd$ on $P$, $({\cal
R}(P),B_{d})$ is a compact regular locale.

###### Proof.

Compactness is trivial. Regularity: with minor adjustments, the proof in [5,
Lemma 2] is valid in CST if one replaces $L$ with $P$. We reproduce it here
for the reader’s convenience. Note first that, if $x\lhd a$, then $\Downarrow
x\prec\Downarrow a$ in ${\cal R}(P)$: indeed if $x\lhd a$ there are $b,c$ such
that $x\lhd c\lhd b\lhd a$. By 5., also $a^{*}\lhd b^{*}\lhd c^{*}\lhd x^{*}$.
Moreover, as $b\vee c^{*}=1$ (1 the greatest element in $P$), $P=\Downarrow
a\vee\Downarrow(x^{*})\leq\Downarrow a\vee(\Downarrow x)^{*}=P$ (the latter
since trivially $\Downarrow(x^{*})\cap\Downarrow(x)=0$). By 7. and 4. we have
$\Downarrow a=\bigvee\\{\Downarrow x:x\lhd a\\}$, so that, in conclusion,
$\Downarrow a=\bigvee\\{\Downarrow x\in B_{d}:\Downarrow x\prec\Downarrow
a\\}$, proving the regularity of ${\cal R}(P)$. ∎

Given a compact regular frame $L$, set-generated by a basis $B$, the frame
${\cal R}(B^{*})$, obtained considering on $B^{*}$ the well inside relation as
strong inclusion (recall Lemma 3.3), is isomorphic to $L$ via $j^{-}:B_{d}\to
L$, $j^{-}(\Downarrow b)=\bigvee\Downarrow b$: we leave to the reader to prove
that $j$ is a locale mapping; then, $j^{-}(\Downarrow b)=b$ by strong
regularity, so that $j^{-}$ is onto. We want to show that $j^{-}$ is _one-one_
, i.e. that for all $I,J\in{\cal R}(B^{*})$, if $\bigvee I=\bigvee J$ then
$I=J$. This follows by the observation that if $L$ is compact, then a strongly
regular ideal $I$ on $B^{*}$ is such that $x\in I\iff 1_{L}=x^{*}\vee\bigvee
I$ (cf [6, Lemma 5]).

Thus, by the above lemma, compact regular frames are precisely the frames of
round ideals over some pcd-lattice endowed with a strong inclusion.

Let $\lhd$ be a strong inclusion on a sub-pcd-lattice $P$ of a locale $L$.
Given a locale map $f:L\to L^{\prime}$ we say that $\lhd$ is _finer than
$f^{-}\times f^{-}[\prec]$_ if $y\prec x$ on $L^{\prime}$ implies
$f^{-}[y]\leq p\lhd p^{\prime}\leq f^{-}[x]$, for some $p,p^{\prime}\in P$.
Denote by $\cal C$ the class of mappings $f:L\to L^{\prime}$ with compact and
regular codomain such that $\lhd$ is finer than $f^{-}\times f^{-}[\prec]$.

######  Theorem 4.3.

Let $L$ be a locale, $P$ any sub-pcd-lattice of $L$, and $\lhd$ a compatible
strong inclusion on $P$. Then, the locale mapping $\mu:L\to{\cal R}(P)$,
defined by $\mu^{-}(I)=\bigvee I$, satisfies the following property: for every
$f:L\to L^{\prime}$ in $\cal C$ a unique locale mapping $g:{\cal R}(P)\to
L^{\prime}$ exists such that $g\circ\mu=f$:

$\textstyle{L\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu}$$\scriptstyle{f}$$\textstyle{{\cal
R}(P)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{L^{\prime}}$

If $\lhd$ is compatible, $\mu:L\to{\cal R}(P)$ is a compactification of $L$.

###### Proof.

Standard arguments show that $\mu^{-}$ satisfies the conditions on continuous
maps. To prove the extension property, if $f:L\to L^{\prime}$ is in $\cal C$,
let $B^{\prime}$ be a sub-pcd-lattice and basis of $L^{\prime}$ ($B^{\prime}$
always exists, cf. Section 3). For $a\in B^{\prime}$, set

$g^{-}(a)=\\{c\in P:(\exists b\in B^{\prime})b\prec a,\ c\leq f^{-}(b)\\}.$

First we prove that $g^{-}(a)\in{\cal R}(P)$. By Restricted Separation,
$g^{-}(a)$ is a set, and trivially an ideal. Let $c\in g^{-}(a)$. Then $c\leq
f^{-}(b),$ for $b\prec a$. By the interpolation property of $\prec$ on
$B^{\prime}$ (Lemma 3.3), there is $d\in B^{\prime}$ such that $b\prec d\prec
a$. By hypothesis, there are $p,p^{\prime}\in P$ such that $f^{-}(b)\leq p\lhd
p^{\prime}\leq f^{-}(d)$. Then $c\lhd p^{\prime}\leq f^{-}(d)$; since $d\prec
a$, one concludes $p^{\prime}\in g^{-}(a)$. This gives $g^{-}(a)\in{\cal
R}(P)$.

Now assume $a\in B^{\prime}$, $U\in\textsf{Pow}(B^{\prime})$ and $a\leq\bigvee
U$. Then $g^{-}(a)\leq\bigvee_{q\in U}g^{-}(q)$: let $c\in g^{-}(a)$, i.e.
assume there is $b\in B^{\prime}$ such that $c\leq f^{-}(b),\ b\prec a$. By
Lemma 3.3, either $b=0$, whence $c=0$, or there are finite subsets
$\\{q_{1},...,q_{n}\\}$, $\\{q^{\prime}_{1},...,q^{\prime}_{n}\\}$ and
$\\{q^{\prime\prime}_{1},...,q^{\prime\prime}_{n}\\}$ of $B^{\prime}$, with
$q^{\prime}_{i}\prec q^{\prime\prime}_{i}\prec q_{i}$, $q_{i}\in U$, and such
that $b\leq\vee q_{i}^{\prime}\prec\vee q^{\prime\prime}_{i}\prec\bigvee U.$
By hypothesis, $p_{i},p_{i}^{\prime}$ exist such that
$f^{-}(q^{\prime}_{i})\leq p_{i}\lhd p_{i}^{\prime}\leq
f^{-}(q_{i}^{\prime\prime})$. Thus, since $q_{i}^{\prime\prime}\prec q_{i}$,
$p_{i}^{\prime}\in g^{-}(q_{i})$. Since $c\leq f^{-}(b)\leq f^{-}(\vee
q^{\prime}_{i})\leq\vee p_{i}^{\prime}$, one has $c\in\bigvee_{q\in
U}g^{-}(q)$. Therefore $g^{-}(a)\leq\bigvee_{q\in U}g^{-}(q)$.

By the properties of $\prec$, and the fact that $f^{-}$ defines a continuous
map, it immediately follows that $g^{-}$ also satisfies conditions 1, 2 on
continuous maps (since $B^{\prime}$ is a pcd-lattice, to verify condition 2 it
is enough to show that $g^{-}(a)\wedge g^{-}(b)=g^{-}(a\wedge b)$, as
$g^{-}(a\wedge b)=\bigvee\\{g^{-}(c):c\in B_{M},c\leq a,c\leq b\\}$, for all
$a,b\in B^{\prime}$). So $g:{\cal R}(P)\to L^{\prime}$ is a continuous map.

To show that $f^{-}(a)=\mu^{-}(g^{-}(a))$, for all $a\in B^{\prime}$, that is,
to prove $\bigvee g^{-}(a)=f^{-}(a)$, let $c\in g^{-}(a)$, i.e. assume there
is $b\in B^{\prime}$ such that $c\leq f^{-}(b),\ b\prec a$. This implies
$c\leq f^{-}(a)$, so that $\bigvee g^{-}(a)\leq f^{-}(a)$. Conversely, since
$a=\bigvee\\{b\in B^{\prime}:b\prec a\\}$, $f^{-}(a)=f^{-}(\bigvee\\{b\in
B^{\prime}:b\prec a\\})=\bigvee_{b\prec a,b\in B^{\prime}}f^{-}(b)$. Let
$b\prec a$; by Lemma 3.3, there is $d\in B^{\prime}$ such that $b\prec d\prec
a$. By hypothesis, there are $p,p^{\prime}\in P$ such that $f^{-}(b)\leq p\lhd
p^{\prime}\leq f^{-}(d)$. Since $d\prec a$, one gets $p^{\prime}\in g^{-}(a)$.
Thus $f^{-}(b)\leq\bigvee g^{-}(a)$ for all $b\prec a$, so that
$f^{-}(a)\leq\bigvee g^{-}(a)$. Finally, uniqueness of $g$ follows by Lemma
2.1, $iii$.

If $\lhd$ is compatible, since $\mu$ is trivially dense and recalling Lemma
4.2, to prove that $\mu$ is a compactification we only have to show that
$\mu^{-}$ is onto: by compatibility of $\lhd$, $L$ is set-generated by $P$,
and given $a\in P$, the set $\\{b\in P:b\lhd a\\}$ is a round ideal of $P$
whose join is $a$. ∎

Now let ${\cal{F}}\equiv\\{f_{i}\\}_{i\in I}$ be a (possibly empty) family of
locale mappings, $f_{i}:L\to L_{i}$, with $L_{i}$ compact and regular, and let
$S$ be a subset of $L$. Set $S_{\cal{F}}=S\cup\\{f_{i}^{-}(b):i\in I,b\in
B_{i}\\}$, where $B_{i}$ is a set of generators and sub-pcd-lattice of
$L_{i}$. With $S_{\mathcal{F}}^{*}$ we shall abbreviate
$(S_{\mathcal{F}})^{*}$.

######  Lemma 4.4.

The relation $\lhd_{\cal{F}}\subseteq S^{*}_{\cal{F}}\times S^{*}_{\cal{F}}$
defined inductively as the least relation containing the set
$\\{(f_{i}^{-}(b),f^{-}_{i}(a)):i\in I,a,b\in B_{i},b\prec a\\}$, and closed
under conditions from 1 to 5 on strong inclusions, is a strong inclusion on
$S^{*}_{\cal{F}}$.

###### Proof.

The set of pairs $(f_{i}^{-}(b),$ $f^{-}_{i}(a))$ is a relation satisfying the
hypotheses of Lemma 4.1 (as $f_{i}^{-}$ preserves $\prec$, and since, by Lemma
3.3, $\prec$ interpolates on $B_{i}$). ∎

Starting from $S=\emptyset$, one obtains the least strong inclusion
$\lhd_{\cal{F}}$ containing the indicated set, on the least (sub)structure on
which it may be considered, i.e. $\emptyset^{*}_{\cal{F}}$.

######  Proposition 4.5.

Let $L$ be a locale, $S$ any subset of $L$, ${\cal{F}}$ a family of locale
mappings as above. Let $\lhd$ be a strong inclusion on $S_{\cal{F}}^{*}$
containing $\lhd_{\cal{F}}$. Then the locale mapping $\mu:L\to{\cal
R}(S_{\cal{F}}^{*},\lhd)$, $\mu^{-}(I)=\bigvee I$, is such that each $f_{i}$
factors uniquely through $\mu$: for all $i$ a unique $g_{i}:{\cal
R}(S^{*}_{\cal{F}},\lhd)\to L_{i}$ exists such that $g_{i}\circ\mu=f_{i}$.

###### Proof.

By Lemma 3.3, if $b\prec a$ on $L_{i}$, one has $b\leq b^{\prime}\prec
a^{\prime}\leq a$, for $a^{\prime},b^{\prime}\in B_{i}$. Then, by construction
of $S_{\cal{F}}^{*}$ and $\lhd_{\cal{F}}$, each $f_{i}$ is such that $\lhd$ is
finer than $f_{i}^{-}\times f_{i}^{-}[\prec]$, and hence, by Theorem 4.3, each
$f_{i}$ factors uniquely through $\mu$. ∎

The compactification to be described next was defined in [9] using topos-
valid, but impredicative, comprehension principles. There I claimed that co-
inductive definitions would probably have allowed for a predicative
construction222At the time of writing [9], [4, Theorem 13.2.3], on the
existence of the largest set coinductively defined by a given set-sized
inductive definition, had not been (proved or) published yet.. The following
shows that this is indeed the case.

In general, the strong inclusion $\lhd_{\cal{F}}$ one obtains by Lemma 4.4
need not be compatible, so that $\mu:L\to{\cal
R}(B_{\cal{F}}^{*},\lhd_{\cal{F}})$ need not be a compactification. For
obtaining a compatible strong inclusion, we shall have to enlarge
$\lhd_{\cal{F}}$.

######  Theorem 4.6.

Let $L$ be a strongly regular locale, and let
${\cal{F}}\equiv\\{f_{i}\\}_{i\in I}$ be a (possibly empty) family of locale
mappings $f_{i}:L\to L_{i}$, with $L_{i}$ compact and regular for all $i\in
I$. Let $B$ be a strongly regular basis for $L$, and $B_{i}$ any basis for
$L_{i}$. Define $B_{\cal{F}}=B\cup\bigcup_{i\in I}\\{f_{i}^{-}(b_{i}):b_{i}\in
B^{*}_{i}\\}$. On $B_{\cal{F}}^{*}$ let $\lhd_{\prec}$ be the largest
interpolative relation contained in $\prec\cap B_{\cal{F}}^{*}\times
B_{\cal{F}}^{*}$. Then the following hold:

  1. $i.$

$\lhd_{\prec}$ is a set and a strong inclusion on $B_{\cal{F}}^{*}$ compatible
with $L$;

  2. $ii.$

$\mu:L\to\gamma L={\cal R}(B_{\cal{F}}^{*},\lhd_{\prec})$ is a
compactification of $L$ such that for all $f_{i}$ there is a unique
$g_{i}:\gamma L\to L_{i}$ such that $g_{i}\circ\mu=f_{i}$:

$\textstyle{L\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu}$$\scriptstyle{f_{i}}$$\textstyle{\gamma
L\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{i}}$$\textstyle{L_{i}}$

###### Proof.

That $\lhd_{\prec}$ is a set follows by proposition 1.1, and that it is a
strong inclusion is proved after the definition of strong inclusion.

We show that $\mu:L\to\gamma L$ is a compactification of $L$ by proving that
$\lhd_{\prec}$ is compatible. Since $B$ is a basis, for all $a\in
B_{\cal{F}}^{*}$, $a=\bigvee_{L}\\{b\in B:b\leq a\\}$. On the other hand, for
all $b\in B$, $b=\bigvee_{L}\\{c\in B:c\prec_{0}^{\prime}b\\}$, because $B$ is
a strongly regular basis of $L$. One has $c\prec_{0}^{\prime}b$ implies
$c\lhd_{\prec}b$, since, by $B\subseteq B_{\cal{F}}^{*}$,
$\prec_{0}^{\prime}\subseteq\prec\cap(B\times
B)\subseteq\prec\cap(B_{\cal{F}}^{*}\times B_{\cal{F}}^{*})$, and
$\prec_{0}^{\prime}$ is interpolative by definition. Then,
$b=\bigvee_{L}\\{c\in B:c\lhd_{\prec}b\\}$, whence $a=\bigvee_{L}\\{b\in
B_{\cal{F}}^{*}:b\lhd_{\prec}a\\}$. This proves that $\lhd_{\prec}$ is
compatible, so that $\mu$ is a compactification.

Since $\lhd_{\cal{F}}$ is interpolative and contained in
$\prec\cap(B_{\cal{F}}^{*}\times B_{\cal{F}}^{*})$, one has that
$\lhd_{\prec}$ contains $\lhd_{\cal{F}}$. Thus, by Proposition 4.5, $ii$
follows. ∎

We showed that a compatible strong inclusion on a sub-pcd-lattice $P$ of a
locale $L$ determines a compactification of $L$. The converse also holds. To
prove this we shall need the following lemma.

######  Lemma 4.7.

Let ${\cal{F}}=\\{f\\}$, $f:L\to M$ with $M$ compact and regular, and let
$B_{M}$ be a base and sub-pcd-lattice of $M$. If $f^{-}[\cdot]:M\to L$ is
$*-$preserving, then for all $x,y\in S^{*}_{f}$, $x\lhd_{f}y\iff x\leq
f^{-}(b),f^{-}(a)\leq y$ for some $a,b\in B_{M}$, with $b\prec a$.

###### Proof.

On $P=S^{*}_{f}$, $\lhd_{f}$ is defined inductively as in Lemma 4.1, as the
least relation containing the set $R=\\{(f^{-}(b),f^{-}(a)):a,b\in
B_{M},b\prec a\\}$, and closed under conditions from 1 to 5 on strong
inclusions. I.e., $\lhd_{f}=I(\Phi_{R})$, with $\Phi_{R}$ as in Lemma 4.1. We
prove the claim by induction. Let $T\subseteq P\times P$, $T=\\{(x,y)\in
P\times P:(\exists a\in B_{M})(\exists b\in B_{M})b\prec a\ \&\ x\leq
f^{-}(b)\ \&\ f^{-}(a)\leq y\\}$. We prove that $T$ is $\Phi_{R}-$closed, so
that, since $\lhd_{f}$ is the least $\Phi_{R}-$closed class, we may conclude
$\lhd_{f}\subseteq T$. Given $(f^{-}(b),f^{-}(a))$ with $a,b\in B_{M},b\prec
a$, we have to prove that $(\exists c\in B_{M})(\exists d\in B_{M})d\prec c\
\&\ f^{-}(b)\leq f^{-}(d)\ \&\ f^{-}(c)\leq f^{-}(a)$. One simply takes
$d=b,c=a$. The remaining cases are as simple, we only prove two of them:
assume $x\leq f^{-}(b^{\prime}),f^{-}(a^{\prime})\leq a$ with $b^{\prime}\prec
a^{\prime}$, and $y\leq f^{-}(b^{\prime\prime}),f^{-}(a^{\prime\prime})\leq a$
with $b^{\prime\prime}\prec a^{\prime\prime}$. Then, $x\vee y\leq
f^{-}(b^{\prime})\vee f^{-}(b^{\prime\prime})=f^{-}(b^{\prime}\vee
b^{\prime\prime}),f^{-}(a^{\prime}\vee a^{\prime\prime})=f^{-}(a^{\prime})\vee
f^{-}(a^{\prime\prime})\leq a$, with $b^{\prime}\vee b^{\prime\prime}\prec
a^{\prime}\vee a^{\prime\prime}$, so that $(x\vee y,a)\in T$. If instead
$a\leq f^{-}(b^{\prime}),f^{-}(a^{\prime})\leq b$, with $b^{\prime}\prec
a^{\prime}$, then $b^{*}\leq f^{-}(a^{\prime})^{*}=f^{-}(a^{\prime*})$ and
$f^{-}(b^{\prime})^{*}=f^{-}(b^{\prime*})\leq a^{*}$, with $a^{\prime*}\prec
b^{\prime*}$, since $f^{-}$ is $*-$preserving. ∎

######  Theorem 4.8.

Let $k:L\to kL$ be a compactification of a locale $L$. Then a sub-pcd-lattice
$P_{k}$ of $L$ and a compatible strong inclusion $\lhd_{k}$ on $P_{k}$ exist
such that ${\cal R}(P_{k},\lhd_{k})$ is isomorphic with $kL$.

###### Proof.

Let $P_{k}=\emptyset^{*}_{\\{k\\}}$, and $\lhd_{k}$ be the strong inclusion
given by Lemma 4.4, where ${\cal{F}}=\\{k\\}$, i.e. the least relation on
$\emptyset^{*}_{\\{k\\}}$ containing the set $\\{(k^{-}(b),k^{-}(a)):a,b\in
B_{kL},b\prec a\\}$, and closed under conditions from 1 to 5 on strong
inclusions ($B_{kL}$ sub-pcd-lattice and basis of $kL$). Compatibility of
$\lhd_{k}$: for all $a\in P_{k}$, $a=\bigvee_{b\in U}k^{-}(b)$ for some
$U\in\textsf{Pow}(B_{kL})$, as $k^{-}$ is onto. For $b\in U$, one has
$b=\bigvee_{c\in B_{kL}}\\{c:c\prec b\\}$. Thus, $a=\bigvee_{b\in
U}\bigvee_{c\in B_{kL}}\\{k^{-}(c):c\prec b\\}$. Since
$k^{-}(c)\lhd_{k}k^{-}(b)\leq a$, one concludes that $\lhd_{k}$ is compatible.

It remains to prove that $kL$ is isomorphic with ${\cal R}(P_{k},\lhd_{k})$.
By Theorem 4.3, the mapping $\mu:L\to{\cal R}(P_{k})$, defined by
$\mu^{-}(I)=\bigvee I$, is a compactification of $L$ that satisfies: for every
$f:L\to L^{\prime}$ in $\cal C_{k}$ a unique mapping $g:{\cal R}(P_{k})\to
L^{\prime}$ exists such that $g\circ\mu=f$, with $\cal C_{k}$ the class of
mappings $f:L\to L^{\prime}$ with compact and regular codomain such that
$\lhd_{k}$ is finer than $f^{-}\times f^{-}[\prec]$. Now, compactification $k$
is in $\cal C_{k}$. Indeed, if $y\prec x$ in $kL$, by Lemma 3.3 there are
$q,q^{\prime}\in B_{kL}$ with $y\leq q\prec q^{\prime}\prec x$. Therefore,
$k^{-}[y]\leq k^{-}(q)\prec k^{-}(q^{\prime})\prec k^{-}[x]$, with
$k^{-}(q),k^{-}(q^{\prime})\in P_{k}$. We then have a unique $g:{\cal
R}(P_{k})\to kL$ such that $g\circ\mu=k$, defined by, for $a\in B_{kL}$,

$g^{-}(a)=\\{c\in P_{k}:(\exists b\in B_{kL})b\prec a,\ c\leq k^{-}(b)\\}.$

We prove that $g$ provides the required isomorphism. Since $k$ is dense, $g$
is dense too (as $k=g\circ\mu$). By Lemma 2.1, then $g^{-}[\cdot]$ in one-one.
To conclude thus we have to prove that $g^{-}$ is onto: if $I\in{\cal
R}(P_{k},\lhd_{k})$ there is $U\in\textsf{Pow}(B_{kL})$ with $\bigvee_{b\in
U}g^{-}(b)=I$. It is enough to show that for $a\in P_{k}$ there is
$U\in\textsf{Pow}(B_{kL})$ with $\bigvee_{b\in U}g^{-}(b)=\Downarrow a$. Let
$U=\\{a^{\prime}\in B_{kL}:k^{-}(a^{\prime})\leq a\\}$. If $d\in\Downarrow a$,
then $d\lhd_{k}a$, so that by the previous Lemma, $d\leq
k^{-}(b^{\prime}),k^{-}(a^{\prime})\leq a$ for some $a^{\prime},b^{\prime}\in
B_{kL}$, $b^{\prime}\prec a^{\prime}$ ($k^{-}$ is $*-$preserving by Lemma 2.1,
$i.$). Thus, $\Downarrow a\subseteq\bigcup_{a^{\prime}\in
U}g^{-}(a^{\prime})=\bigcup_{a^{\prime}\in U}\\{c\in P_{k}:(\exists
b^{\prime}\in B_{kL})b^{\prime}\prec a^{\prime},\ c\leq k^{-}(b^{\prime})\\}$,
that gives $\Downarrow a\leq\bigvee_{a^{\prime}\in U}g^{-}(a^{\prime})$. On
the other hand, for all $a^{\prime}\in U$, $g^{-}(a^{\prime})\leq\Downarrow a$
again by the previous Lemma. This proves that $g^{-}$ is onto, as wished. ∎

Note that the class $\cal C_{k}$, of continuous maps $f:L\to L^{\prime}$ with
compact and regular codomain such that $\lhd_{k}$ is finer than $f^{-}\times
f^{-}[\prec]$ (recall that $\lhd_{k}$ is finer than $f^{-}\times f^{-}[\prec]$
if $y\prec x$ on $L^{\prime}$ implies $f^{-}[y]\leq p\lhd_{k}p^{\prime}\leq
f^{-}[x]$, for some $p,p^{\prime}\in P_{k}$), is completely determined by the
compactification $k:L\to kL$, i.e., it does not depend on the choice of the
base $B_{kL}$ of $kL$ for the construction of $(P_{k},\lhd_{k})$. Indeed,
assume $B^{\prime}_{kL}$ is a different sub-pcd-lattice and basis of $kL$, and
let $P_{k}^{\prime}=\emptyset^{*}_{\\{k\\}}$ and $\lhd^{\prime}_{k}$ be the
sub-pcd-lattice of $L$ and strong inclusion constructed from
$B^{\prime}_{kL}$. We prove that if $\lhd^{\prime}_{k}$ is finer than
$f^{-}\times f^{-}[\prec]$, then also $\lhd_{k}$ is finer than $f^{-}\times
f^{-}[\prec]$: let $y\prec x$ on $L^{\prime}$, so that $f^{-}[y]\leq
p\lhd^{\prime}_{k}p^{\prime}\leq f^{-}[x]$ for $p,p^{\prime}\in
P_{k}^{\prime}$. By Lemma 4.7, if $p\lhd^{\prime}_{k}p^{\prime}$ then
$a^{\prime},b^{\prime}\in B^{\prime}_{kL}$ exist with $b^{\prime}\prec
a^{\prime}$, $p\leq k^{-}(b^{\prime})$, $k^{-}(a^{\prime})\leq p^{\prime}$, as
$k^{-}$ is $*-$preserving. Since $kL$ is compact, by Lemma 3.3, $a,b$ exist in
$B_{kL}$ such that $b^{\prime}\prec b\prec a\prec a^{\prime}$. Therefore,
$p\leq k^{-}(b)=q$, $q^{\prime}=k^{-}(a)\leq p^{\prime}$, whence
$q\lhd_{k}q^{\prime}$, and $f^{-}[y]\leq q\lhd_{k}q^{\prime}\leq f^{-}[x]$.

Banaschewski [5] proves (in our notation) that every compactification $k:L\to
kL$ is associated with a compatible strong inclusion $\lhd_{k}$ on $L$
determining an isomorphic compactification ${\cal R}(L,\lhd_{k})$, by
defining, for $x,y\in L$, $x\lhd_{k}y\iff\bigvee\\{u\in
kL:k^{-}(u)=x\\}\prec\bigvee\\{v\in kL:k^{-}(v)=y\\}$. As already expounded,
Banaschewski’s construction is not viable in the present constructive setting.
Theorem 4.8 provides then a constructive version of Banaschewski’s result.

The construction of ${\cal R}(P_{k},\lhd_{k})$ in the previous theorem, aside
from its constructive character, allows us to characterize a compactification
in terms of its ability to extend continuous mapping with compact and regular
codomain. Recall indeed that the compactifications of a locale $L$ are ordered
as follows: if $k:L\to kL$ and $k^{\prime}:L\to k^{\prime}L$ are
compactifications of $L$, $k\leq k^{\prime}$ if and only if $k=h\circ
k^{\prime}$, for a continuous $h:k^{\prime}L\to kL$:

$k\leq k^{\prime}\hskip 28.45274pt\iff$

The following is the announced characterization.

######  Corollary 4.9.

Let $k:L\to kL$ be a compactification of a strongly regular locale $L$, and
$\cal C_{k}$ the associated class of continuous maps $f:L\to L^{\prime}$ with
compact and regular codomain such that $\lhd_{k}$ is finer than $f^{-}\times
f^{-}[\prec]$. Then, for every $f\in\cal C_{k}$ a unique continuous $g:kL\to
L^{\prime}$ exists such that $g\circ k=f$, and $k:L\to kL$ is the minimal
compactification with this property.

###### Proof.

The first part of this corollary follows directly by Theorems 4.3 and 4.8. For
the second, assume $k^{\prime}:L\to k^{\prime}L$ has the same property with
respect to the class $\cal C_{k}$. Then, since $k:L\to kL$ is in $\cal C_{k}$,
there is a (unique) $g:k^{\prime}L\to kL$ with $g\circ k^{\prime}=k$, so that
$k\leq k^{\prime}$. ∎

Observe that, given a strong inclusion $\lhd$ on a sub-pcd-lattice $P$ of a
locale $L$, the composite $\overline{\lhd}\equiv\leq\circ\lhd\circ\leq$ on $L$
yields a class relation satisfying the axioms of a strong inclusion, the least
one on $L$ extending $\lhd$. One then has that $\lhd$ on $P$ is finer than
$f^{-}\times f^{-}[\prec]$ iff $f^{-}\times
f^{-}[\prec]\subseteq\overline{\lhd}$. So the extension property in the
previous corollary may be expressed as follows: every continuous $f:L\to
L^{\prime}$ with compact and regular codomain such that $f^{-}\times
f^{-}[\prec]\subseteq\overline{\lhd}_{k}$ has a unique continuous extension
$g:kL\to L^{\prime}$ to $kL$. In [9] we showed that Alexandroff
compactification $\alpha L$ of a locally compact regular locale $(L,B)$ can be
defined by constructing inductively the least strong inclusion $\lhd_{<<}$ on
$B^{*}$ that contains the restriction of the familiar way-below relation to
$B^{*}\times B^{*}$. Once the concepts of local compactness and way-below
relation are treated as indicated in [10], the given proof can be formulated
in CST. So by the above Corollary, Alexandroff compactification $\alpha L$ can
be characterized as the minimal compactification that allows for the extension
of all those continuous mappings from $L$ to a compact and regular codomain
whose inverse images ‘send the well-inside relation into the least strong
inclusion containing the way-below relation’.

Finally, we observe that for compactifications $k_{1}:L\to k_{1}L,k_{2}:L\to
k_{2}L$ one has

$k_{1}\leq k_{2}\iff\cal C_{k_{1}}\subseteq\cal C_{k_{2}}$

Indeed, assume $k_{1}\leq k_{2}$, i.e. assume there is $h:k_{2}L\to k_{1}L$
such that $k_{1}=h\circ k_{2}$. Let $f:L\to L^{\prime}$ in $\cal C_{k_{1}}$,
so that, if $y\prec x$ in $L^{\prime}$, there are $p,p^{\prime}\in P_{k_{1}}$
with $f^{-}[y]\leq p\lhd_{1}p^{\prime}\leq f^{-}[x]$. To conclude that
$f\in\cal C_{k_{2}}$, we want $q,q^{\prime}\in P_{k_{2}}$ such that
$f^{-}[y]\leq q\lhd_{2}q^{\prime}\leq f^{-}[x]$. By $p\lhd_{1}p^{\prime}$,
recalling Lemma 4.7, we have $a,b\in B_{k_{1}L},b\prec a$ with $p\leq
k_{1}^{-}(b)=k_{2}^{-}[h^{-}(b)],\ k_{2}^{-}[h^{-}(a)]=k_{1}^{-}(a)\leq
p^{\prime}$ ($B_{k_{i}L}$ sub-pcd-lattices and bases for $k_{i}L$). Since
$k_{2}L$ is compact and regular, and since $h^{-}(b)\prec h^{-}(a)$, by Lemma
3.3 we have $a^{\prime},b^{\prime}\in B_{k_{2}L}$ with $h^{-}(b)\prec
b^{\prime}\prec a^{\prime}\prec h^{-}(a)$, so that $f^{-}[y]\leq p\leq
k_{1}^{-}(b)=k_{2}^{-}[h^{-}(b)]\leq
k_{2}^{-}(b^{\prime})\lhd_{1}k_{2}^{-}(a^{\prime})\leq k_{1}^{-}(a)\leq
p^{\prime}\leq f^{-}[x]$. Thus we conclude with
$q=k_{2}^{-}(b^{\prime}),q^{\prime}=k_{2}^{-}(a^{\prime})\in P_{k_{2}}$.
Conversely, if $\cal C_{k_{1}}\subseteq\cal C_{k_{2}}$, we conclude by
Corollary 4.9 that $k_{1}\leq k_{2}$ observing that $k_{1}\in C_{k_{1}}$.

Therefore, if the sublattice $P_{k}$ of $L$ and strong inclusion $\lhd_{k}$
are ‘sufficiently large’ to be such that$\lhd_{k}$ is finer than every
continuous function with compact regular co-domain, so that $\cal C_{k}$
coincides with the class of all such functions, $k:L\to kL$ is the largest
compactification of $L$, i.e. the compact regular reflection of $L$ (‘weak’
Stone-Čech compactification). In this sense, the ability of a compactification
$k$ to extend the continuous functions in $\cal C_{k}$ can be regarded as an
approximation of the characterizing property of Stone-Čech compactification
(when it exists, cf. next section).

##  5\. An interesting open question: the constructive compact regular
reflection of a locale

One might be tempted to think that, choosing in Theorem 4.6 as ${\cal{F}}$ the
family of all mappings $f:L\to L^{\prime}$, with $L^{\prime}$ compact regular,
one would get the ‘weak’ Stone-Čech compactification of $L$ (i.e. its compact
regular reflection, ‘weak’ as opposed to the compact completely regular
reflection). Unfortunately, this is not the case, since those mappings are too
many to be set-indexed (even in classical set theory).

In [7], Banaschewski and Pultr define the compact regular reflection of a
strongly regular locale $L$ considering the strongly regular ideals of $L$
with respect to the largest strong inclusion contained in the well-inside
relation on $L$. Previously, Banaschewski and Mulvey [6] used the completely
regular ideals on $L$ (i.e. the strongly regular ideals with respect to the
really inside relation as strong inclusion) to define the compact completely
regular reflection of $L$ (‘strong’ Stone-Čech compactification).

None of these reflections can be defined constructively in the present sense
in full generality. This is not just because the specific constructions cannot
be carried out in CST (a non-trivial frame is a proper class [10], and the
ideals of this class do not yield a frame). It is proved in [10] that the
compact _completely_ regular reflection is independent from CST also when
extended with (various principles including) the principle of dependent
choice. With DC the compact regular and compact completely regular reflection
coincide, so that if we could define the compact regular reflection of every
locale $L$ in CST, we could also define the compact completely regular
reflection of every locale $L$ in CST+DC (see the Appendix for the formal
version of these statements).

In [8] it is however proved that one may define constructively the compact
completely regular reflection $\beta L$ of $L$, for every locale $L$ such that
the class of continuous mappings $Hom_{Loc}(L,[0,1])$ from $L$ to the localic
real unit interval is a set (while this is always the case in classical set
theory or in a topos, proving that $Hom_{Loc}(L,[0,1])$ is a set is in general
non-trivial, and not the case for every locale in CST). This condition in fact
characterizes the locales $L$ of which the compact completely regular
reflection can be constructed.

The construction of $\beta L$ in [8] can be summarized as follows: if
$Hom_{Loc}(L,[0,1])$ is a set, one can expand a base $B$ of $L$ to a base
$B_{\cal{F}}$ containing counterimages of basic elements of the localic real
unit interval. Since $Hom_{Loc}(L,[0,1])$ is a set, $B_{\cal{F}}$ is a set,
too. Then, on the pcd-lattice $B_{\cal{F}}^{*}$ one takes the completely
regular ideals. The resulting frame ${\cal R}(B_{\cal{F}}^{*})$ is compact and
completely regular, and allows for the extension of each mapping in
$Hom_{Loc}(L,[0,1])$ to ${\cal R}(B_{\cal{F}}^{*})$.

One then proves that (Čech’s theorem implies Stone’s theorem, i.e. that) a
compactification of $L$ that allows for the extension of each mapping in
$Hom_{Loc}(L,[0,1])$ in fact allows for the extension of each continuous
mapping in $Hom_{Loc}(L,L^{\prime})$, for every $L^{\prime}$ compact and
completely regular. This latter result in turn is proved exploiting Tychonoff
embedding theorem for exhibiting the completely regular locale $L^{\prime}$ as
a sublocale of a set-indexed product of the localic unit interval.

A similar procedure does not seem to work for the compact regular reflection
of a strongly regular locale. Indeed, when $Hom_{Loc}(L,[0,1])$ is a set for
$L$ a strongly regular locale, by Theorem 4.6 we are able to construct a
compact regular compactification that allows for the extension of all mappings
in ${\cal{F}}=Hom_{Loc}(L,[0,1])$, but we cannot use Tychonoff embedding
theorem for embedding a compact regular (not necessarily completely regular
without DC) $L$ in a set-indexed product of $[0,1]$, for showing that the
obtained compactification is in fact the compact regular reflection of $L$.

In [6] Banaschewski and Mulvey also provided a definition of the compact
regular reflection of a locale, but remarked that a concrete description of
the compact regular reflection of a strongly regular locale using strongly
regular ideals would have been desirable. As said such a description, when not
appealing to strongly non constructive set existence principles, cannot be
derived in full generality, but the question whether a restricted version of
it similar to that obtained for the compact completely regular reflection in
[8] can be constructed is open.

Open Problem: Can the compact regular reflection of a locale $L$ be defined in
CST in non-trivial cases? Can the locales of which the compact regular
reflection exists in CST be characterized?

A related open problem is the following. In [9] we proved that, when
$Hom_{Loc}(L,$ $[0,1])$ is a set, the sub-pcd-lattice $B_{\cal{F}}^{*}$ of $L$
used for constructing the compact regular reflection is sufficiently large for
fully replacing $L$ in the construction of every compactification, in the
sense that every compactification of a frame $L$ can be obtained as the frame
of round ideals over $B_{\cal{F}}^{*}$, for a certain inductively defined
strong inclusion on $B_{\cal{F}}^{*}$. A similar result for compact regular
compactifications would be desirable.

##  6\. Appendix: Constructive Set Theory. Inductive and co-inductive
definitions

In this appendix the formal system for the constructive set theory we have
been working in is described to make the paper self-contained. The reader may
consult [1, 3, 4] for a thorough introduction to the subject. A core formal
system for constructive set theory is the choice-free _Constructive Zermelo-
Fraenkel Set Theory_ (CZF). This system is often extended by principles
(described below) ensuring that certain inductively and co-inductively defined
classes are sets. Note that CZF, extended or not by those principles, is a
subtheory of classical set theory. As already pointed out, in contrast to ZF,
CZF does not have the impredicative unrestricted Separation scheme and the
Powerset axiom.

The language of CZF is the same as that of Zermelo-Fraenkel Set Theory, ZF,
with $\in$ as the only non-logical symbol. Beside the rules and axioms of a
standard calculus for intuitionistic predicate logic with equality (e.g.,
[15]), CZF has the following axioms and axiom schemes:

  1. (1)

Extensionality: $\forall a\forall b(\forall y(y\in a\leftrightarrow y\in
b)\rightarrow a=b)$.

  2. (2)

Pair: $\forall a\forall b\exists x\forall y(y\in x\leftrightarrow y=a\vee
y=b).$

  3. (3)

Union: $\forall a\exists x\forall y(y\in x\leftrightarrow(\exists z\in a)(y\in
z))$.

  4. (4)

Restricted Separation scheme:

$\forall a\exists x\forall y(y\in x\leftrightarrow y\in a\&\phi(y)),$

for $\phi$ a restricted formula. A formula $\phi$ is _restricted_ if the
quantifiers that occur in it are of the form $\forall x\in b$, $\exists x\in
c$.

  5. (5)

Subset Collection scheme:

$\displaystyle\forall a\forall b\exists c\forall u((\forall x\in a)(\exists
y\in b)\phi(x,y,u)\;\rightarrow$ $\displaystyle(\exists d\in c)((\forall x\in
a)(\exists y\in d)\phi(x,y,u)\&(\forall y\in d)(\exists x\in a)\phi(x,y,u))).$

  6. (6)

Strong Collection scheme:

$\displaystyle\forall a((\forall x\in a)\exists y\phi(x,y)\;\rightarrow$
$\displaystyle\exists b((\forall x\in a)(\exists y\in b)\phi(x,y)\&(\forall
y\in b)(\exists x\in a)\phi(x,y))).$

  7. (7)

Infinity: $\exists a(\exists x\in a\&(\forall x\in a)(\exists y\in a)x\in y)$.

  8. (8)

Set Induction scheme: $\forall a((\forall x\in
a)\phi(x)\rightarrow\phi(a))\rightarrow\forall a\phi(a)$.

We shall denote by ${\mathrm{CZF}}^{-}$ the system obtained from
${\mathrm{CZF}}$ by leaving out the Subset Collection scheme. Subset
Collection is perhaps the most unusual of the CZF axioms and schemes; for this
article it suffices to note that using it one proves that the class $b^{a}$ of
functions from a set $a$ to a set $b$ is a set, i.e., the Exponentiation
Axiom. We did not make use of Subset Collection or Exponentiation in this
paper. Note that the theory obtained from ${\mathrm{CZF}}$ by adding the Law
of Excluded Middle has the same theorems as ZF.

As in classical set theory, one takes advantage in this context of class
notation and terminology [3, 4]. For example, given any set or class $X$, one
has the class $\mathrm{V}=\\{x\mid x=x\\}$ of all sets.

As shown in this paper, a major role in constructive set theory is played by
inductive definitions. Inductively defined classes and sets are natural
objects in a constructive context [1]; further, they partially compensate the
lack of the impredicative powerset construction.

An _inductive definition_ is any class $\Phi$ of pairs. A class $A$ is
_$\Phi-$ closed_ if:

$(a,X)\in\Phi$, and $X\subseteq A$ implies $a\in A$.

The following theorem is called _the class inductive definition theorem_ [3].
It says that (any extension of) the system ${\mathrm{CZF}}^{-}$ has the class
induction property CIP recalled in Section 1.

######  Theorem 6.1 (${\mathrm{CZF}}^{-}$).

Given any class $\Phi$ of ordered pairs, there exists a least $\Phi-$closed
class $I(\Phi)$, the class inductively defined by $\Phi$.

Even when $\Phi$ is a set, $I(\Phi)$ need not be a set in CZF. For this
reason, CZF is often extended with the _Regular Extension Axiom_ , REA.

REA: every set is a subset of a regular set.

A set $c$ is _regular_ if it is transitive, inhabited, and for any $u\in c$
and any set $R\subseteq u\times c$, if $(\forall x\in u)(\exists y)\langle
x,y\rangle\in R$, then there is a set $v\in c$ such that

(1) $\displaystyle(\forall x\in u)(\exists y\in v)((x,y)\in R)$
$\displaystyle\&$ $\displaystyle(\forall y\in v)(\exists x\in u)((x,y)\in R).$

$c$ is said to be weakly regular if in the above definition of regularity the
second conjunct in (1) is omitted. The weak regular extension axiom, wREA, is
the statement that every set is the subset of a weakly regular set.

A class $K$ is a _bound_ for $\Phi$ if, for every $(x,X)\in\Phi$, there is a
set $k\in K$ and an onto mapping $f:k\to X$. The inductive definition $\Phi$
is defined to be _bounded_ if:

1\. $\\{x\mid(x,X)\in\Phi\\}$ is a set for every set $X$;

2\. $\Phi$ is bounded by a set.

The following theorem states that in the system $\mathrm{CZF+wREA}$ the
Bounded Induction Scheme (BIS) is derivable.

######  Theorem 6.2 ($\mathrm{CZF+wREA}$).

If $\Phi$ is bounded, in particular if $\Phi$ is a set, then $I(\Phi)$ is a
set.

Given an inductive definition $\Phi$ on a class $S$, $\Phi\subseteq
S\times\textsf{Pow}(S)$, a class $C\subseteq S$ is said to be $\Phi-$inclusive
if $C\subseteq\Gamma_{\Phi}(C)$, with $\Gamma_{\Phi}$ the operator on
subclasses associated with $\Phi$: $\Gamma_{\Phi}(C)=\\{x\ \mid\ (\exists X)\
(x,X)\in\Phi\ \&\ X\subseteq C\\}$. Aczel showed that the class
$J=\bigcup\\{Y\in\textsf{Pow}(S)\ \mid\ Y\subseteq\Gamma_{\Phi}(Y)\\}$ is the
largest $\Phi-$inclusive subclass of $S$, the class co-inductively defined by
$\Phi$, denoted by $C(\Phi)$. This result is proven in the system CZF- \+ RRS,
where the Relation Reflection Scheme RRS is the following axiom scheme.

Relation Reflection Scheme, RRS:

  * For classes $S,R$ with $R\subseteq S\times S$, if $a\in S$ and $\forall x\in S\ \exists y\in S\ R(x,y)$ then there is a set $S_{0}\subseteq S$ such that $a\in S_{0}$ and $\forall x\in S_{0}\ \exists y\in S_{0}\ R(x,y)$.

This scheme can be regarded as a weakening of the Relativized Dependent
Choices Axiom, RDC. By contrast with RDC, RRS is valid in all topological
models (all cHa-valued models). Note also that RRS is a theorem of ZF (see [2]
for a proof of these facts).

The following strengthening of RRS and REA is used to show that $J$ is a set
when $S,\Phi$ are sets. A regular set $A$ is _strongly regular_ if it is
closed under the union operation, i.e., if $\forall x\in A\ \cup x\in A$. Let
$A$ be a strongly regular set. $A$ is defined to be _RRS-strongly regular_ if
also, for all sets $A^{\prime}\subseteq A$ and $R\subseteq A^{\prime}\times
A^{\prime}$, if $a_{0}\in A^{\prime}$ and $\forall x\in A^{\prime}\ \exists
y\in A^{\prime}\ xRy$ then there is $A_{0}\in A$ such that $a_{0}\in
A_{0}\subseteq A^{\prime}$ and $\forall x\in A_{0}\ \exists y\in A_{0}\ xRy$.

RRS-$\bigcup$REA: Every set is the subset of a RRS-strongly regular set.

The following theorem is proved in [4].

######  Theorem 6.3 (CZF+ RRS-$\bigcup$REA).

If $S$ and $\Phi$ are sets, the largest $\Phi-$inclusive subclass of $S$, i.e.
the class $C(\Phi)\equiv J=\bigcup\\{Y\in\textsf{Pow}(S)\ \mid\
Y\subseteq\Gamma_{\Phi}(Y)\\}$ co-inductively defined by $\Phi$, is a set.

We conclude this Appendix describing formally the independence - mentioned in
Section 5 \- of the weak Stone-Čech compactification of locales in its full
form, from the formal system for CST adopted in this article. In [10], the
compact completely regular reflection of a Boolean locale is proved to be
independent from the formal system CZF, and from every extension of CZF that
is consistent with the Generalized Uniformity Principle (GUP), as e.g.
CZF+REA+RDC. As pointed out to me by M. Rathjen, using realizability [14], one
shows that one such system is also CZF+$\bigcup$REA+ RDC. This system extends
the choice-free system CZF+RRS-$\bigcup$REA, described above, and adopted in
this article as formal system for CST. So, if the compact regular reflection
of a Boolean locale were derivable in CZF+RRS-$\bigcup$REA, it would also be
derivable in CZF+$\bigcup$REA+RDC, but in the presence of DC (and a fortiori
of RDC), the compact regular and compact completely regular reflection of a
locale coincide.

## References

  * [1] P. Aczel, _The type theoretic interpretation of constructive set theory: inductive definitions_. In: Logic, Methodology, and Philosophy of Science VII, R. B. Marcus et al. eds. North Holland, 1986, 17-49.
  * [2] P. Aczel, “The relation reflection scheme”. _Math. Log. Q._ 54 (2008), no. 1, 5 11.
  * [3] P. Aczel, M. Rathjen, “Notes on Constructive Set Theory”, Mittag-Leffler Technical Report No.40, 2000/2001.
  * [4] P. Aczel, M. Rathjen _Constructive Set Theory_ , Book Draft, 2010. [Available from http://www1.maths.leeds.ac.uk/ rathjen/preprints.html].
  * [5] B. Banaschewski, “Compactification of frames”. _Math. Nachr._ 6 (1990), 105-116.
  * [6] B. Banaschewski, C.J. Mulvey “Stone-Čech compactification of locales I”. Houston J. Math. 6 (1980), 301-312.
  * [7] B. Banaschewski, A. Pultr, “A constructive view of complete regularity”. _Kyungpook Math. J._ 43 (2) (2003), 257-262.
  * [8] G. Curi, “Exact approximations to Stone-Čech compactification”. Ann. Pure Appl. Logic, 146, 2-3 (2007), 103-123.
  * [9] G. Curi, “Remarks on the Stone-Čech and Alexandroff compactifications of locales”. _J. Pure Appl. Algebra_ 212, 5, (2008), 1134-1144.
  * [10] G. Curi, “On the existence of Stone-Čech compactification”, _JSL_ , 75, 4 (2010), 1137-1146.
  * [11] G. Curi, _Topological inductive definitions_. Kurt Gödel Research Prize Fellowships 2010. Ann. Pure Appl. Logic, 163, 11 (2012), 1471-1483.
  * [12] P. T. Johnstone, Stone Spaces, Cambridge University Press, 1982.
  * [13] P. T. Johnstone, Sketches of an elephant. A topos theory compendium. Oxford Logic Guides 44; Oxford Science Publications, Clarendon Press, Oxford, 2002.
  * [14] M. Rathjen, “Constructive Set Theory and Brouwerian Principles”, _Journal of Universal Computer Science_ , vol. 11, no. 12 (2005), 2008-2033.
  * [15] A. Troelstra, D. van Dalen, Constructivism in mathematics, an introduction. Volume I. Studies in logic and the foundation of mathematics, vol. 121, North-Holland.