#### Supplement to Constructive Mathematics

## Approaches to Constructive Topology

One of the basic results of classical point set topology is the
Heine-Borel theorem (HBT): if a set of open intervals covers the
closed unit interval [0,1], then already finitely many of them cover
the interval; in other words, [0,1] is *open-cover
compact*. Within INT the theorem is still valid by an appeal to
the full fan theorem (Dummett [2000]). Moerdijk [1984] has shown that
HBT is strictly weaker than the full fan theorem, but we do not know
of any natural fan theorem to which the Heine-Borel theorem is
equivalent relative to BISH. HBT is one example of how fan theorems
facilitate the development of topology within INT; see also Troelstra
[1978] and Waaldijk [1996]. However the effectivity of HBT can be called
into question, as within RUSS the existence of \(\varepsilon\)-singular
covers (see Section 3.2 above) provides a strong recursive
counterexample to the theorem.

In his practice of analysis, Bishop [1967] took a radical approach by limiting his attention to metric spaces, in which compactness can be defined as completeness plus total boundedness. Moreover, he took the continuity of a function from a compact metric space into a metric space to mean uniform continuity, by definition. This allowed him to regain most of the useful theorems about, for example, suprema and positive measures, without referring to HBT. It is possible to generalise his theory to uniform spaces, but for some applications this is clearly not sufficient: for instance, quotient spaces of uniform spaces need not be uniform spaces, a fact that bars direct applicability to fields such as algebraic topology.

However, almost in passing, Bishop [1967] mentions two possible approaches to the constructive development of topology: neighbourhood spaces and function spaces. Little appears to have been done in the former topic, but Petrakis [2016, 2016a] has made considerable progress in the latter. The two are linked in an interesting article of Ishihara [2013].

The neighborhood structure on a topological space tells us only when points are close, but in general gives little information about the more global structure of the space. In order to go significantly beyond metric and uniform spaces, we need to consider topological spaces endowed with some not-necessarily-uniform structure over and above the neighbourhood one. One such endowment is the function space structure mentioned in the preceding paragraph. We now describe two alternative approaches: apartness spaces, where the fundamental axioms capture the idea of subspaces being apart from one another; and point-free topology, where the notion of open sets and their mutual cover relations are taken as basics.

### Apartness spaces

A classical theory of proximity spaces, based on the primitive notion of two sets being near each other, has been around for over 100 years and has been developed substantially over the last 60 or so; see Riesz [1908], Naimpally & Warrack [1970], and Naimpally [2009]. It soon becomes clear, however, that the notion—a negative one, logically speaking—of nearness does not have much computational strength, and that, in some constructive form, its classical obverse—apartness—is what one needs for a constructively fruitful theory. We sketch such a theory based on a few axioms specifying the fundamental properties of the notion of apartness (a) between a point and a set, and (b) between two sets.

Let \(X\) be an inhabited set equipped with an inequality relation \(\ne\) : that is, a binary relation on \(X\) that satisfies these two properties for all \(x, y \in X\) :

\[\begin{align*} x \ne y &\Rightarrow \neg(y \ne x), \\ x \ne y &\Rightarrow y \ne x. \end{align*}\]Note that, in general, this inequality relation will be distinct from the special case of the denial inequality, in which the first implication in the preceding display is replaced by a bi-implication. This distinction gives rise to two types of complement for subsets \(S\) of \(X\):

- the
*logical complement*, \(\neg S \equiv \{x \in X : \neg(x \in S)\}\); - the
*complement*, \({\sim}S \equiv \{x \in X : \forall s \in S (x \ne s)\}\).

We also equip \(X\) with a binary relation \(\bowtie\) between points and subsets of \(X\). This brings into play a third type of complement:

- the
*apartness complement*, \({-}S \equiv \{x \in X : x \bowtie S\}\).

It will follow from the axioms for \(\bowtie\) that \({-}S \subset{\sim}S \subset \neg S\).

If \(\bowtie\) satisfies the following axioms (in which, for
simplicity, we omit the quantifiers), then it is called a
(*point-set*) *pre-apartness* on \(X\), and \(X\), taken
with \(\bowtie\), becomes a (*point-set*) *pre-apartness
space*:

If, in addition to A1–A4, the pre-apartness satisfies

\[ \tag{A5} x \bowtie A \Rightarrow \forall y \in X (x \ne y \vee y \bowtie A), \]
then we call it an *apartness*, and the space X a (point-set)
apartness space. The value of the additional axiom A5 is that it
provides us with alternatives that hold automatically in CLASS and
that facilitate many constructive proofs. Nevertheless, it makes good
sense to work without A5 where it is not needed.

The canonical example of an apartness space is an inhabited metric space \((X,\varrho)\), taken with the metric inequality defined by

\[ x \ne y \Leftrightarrow \varrho(x, y) \gt 0 \]and with

\[ x \bowtie S \Leftrightarrow \exists r \gt 0\,\forall s \in S\, (\varrho(x, s) \ge r). \]The real line \(\mathbf{R}\) with its standard metric is such an apartness space. However, if we take the real line with the denial inequality, rather than metric one, then axiom A5 holds if and only if we adopt Markov’s principle; so in the absence of the latter, the resulting space is only a pre-apartness one.

For the rest of this section only, we adopt the convention that a topological space \(X\) comes with an inequality relation \(\ne\). The topology \(\tau\) then induces a topological pre-apartness \(\bowtie_{\tau}\) on \(X\), defined by

\[ x \bowtie_{\tau} S \Leftrightarrow x \in({\sim}S)^{\circ}, \]where, as usual, \(^{\circ}\) denotes interior. If
\(X\) has the *topological A5 property*,

then the corresponding pre-apartness is an apartness. Note that on a metric apartness space the apartness corresponding to the metric topology coincides with the metric apartness.

Every pre-apartness
\(\bowtie\) on an inhabited set induces a natural apartness topology
\(\tau_{\bowtie}\), in which the *nearly open sets* are the
unions of families of apartness complements. In turn,
\(\tau_{\bowtie}\) induces on \(X\) a pre-apartness, which turns out
to be the original one. If the pre-apartness \(\bowtie\) is induced by
a topology \(\tau\) on \(X\), then every nearly open subset of \(X\)
is \(\tau\)-open. When the converse holds, so that the apartness
topology and the original one coincide, we say that the topological
space \(X\) is *topologically consistent*. Topological
consistency always holds classically, but need not hold
constructively. One condition on \(X\) that ensures its topological
consistency is that of *topological local decomposability*:

If we start with a pre-apartness \(\bowtie\) on a set \(X\), then we
can define a counterpart of this last condition—*local
decomposability*:

It turns out that a topological space \((X, \tau)\) is topologically locally decomposable if and only if it is topologically consistent and \((X, \bowtie_{\tau})\) is locally decomposable.

One obvious way to introduce continuity of a mapping \(f : (X,
\bowtie_X) \rightarrow(Y, \bowtie_Y)\) between pre-apartness spaces is
to work with the corresponding apartness topologies. Thus we say that
\(f\) is *topologically continuous* if for each nearly open
subset \(V\) of \(Y, f^{-1}(V)\) is nearly open in \(X\). But there is
a notion of continuity that is more in the morphic spirit of category
theory: we say that \(f\) is *apartness continuous* if for all
\(x \in X\) and \(S \subset X\),

If \(X\) and \(Y\) are metric spaces, then the apartness continuity of \(f\) is equivalent to continuity in the usual \(\varepsilon\)-\(\delta\) sense.

The really hard work, with significant rewards, in the theory of apartness comes when we lift our attention to pre-apartness between subsets of an inhabited set \(X\). For this, we require the (set-set) pre-apartness \(\bowtie\) to satisfy the following axioms:

\[\begin{align} \tag{B1} &X \bowtie \varnothing \\ \tag{B2} &{-}A \subset{\sim}A \\ \tag{B3} &(A_1 \cup A_2) \Leftrightarrow(B_1 \cup B_2) \not\Leftrightarrow \forall i, j \in \{1, 2\} (A_i \bowtie B_j) \\ \tag{B4} &{-}A \subset{\sim}B \Rightarrow {-}A \subset {-}B. \end{align}\](The rather complicated form of axiom B3 enables us to work without assuming the symmetry of \(\bowtie\).)

As the reader will have surmised, in axioms B2 and B4, \({-}A\) is the apartness complement of \(A\) relative to the point-set relation defined by

\[ x \bowtie A \Leftrightarrow \{x\} \bowtie A, \]
which is a point-set pre-apartness said to be *associated
with*, or *induced by*, the set-set relation \(\bowtie.\)

If axioms B1–B4 hold, then the pair \((X, \bowtie)\), or when no
confusion is likely, the set \(X\) itself, a
(*set-set*) *pre-apartness space*; and if \(A \bowtie
B\), we say that \(A\) is *apart from B*. By a
(*set-set*) *apartness* on \(X\) we mean a relation
\(\bowtie\) between subsets of \(X\) that satisfies axioms B1–B3
and

The relation \(\bowtie\) then also satisfies B4 and so is a
pre-apartness. Regarded as a point-set pre-apartness space, \(X\)
is then locally decomposable (this is precisely what B5 says) and
hence satisfies A5. In this case we call \((X, \bowtie)\), or
simply \(X\) itself, a (*set-set*) *apartness
space*.

The canonical example of a set-set apartness is again a metric space
\((X, \varrho)\), in which we define the *metric apartness*
by

A more general example is a uniform space, whose definition we pass over here.

The natural morphisms in the category of set-set pre-apartness spaces
are the functions \(f : (X, \bowtie_X) \rightarrow (Y, \bowtie_Y)\)
that are *strongly continuous*,in the sense that for all \(A, B
\subset X\),

Every uniformly continuous mapping between metric spaces is strongly continuous. Among other results connecting types of continuity for a mapping \(f : X \rightarrow Y\) between metric spaces we have these:

- \(f\) is uniformly continuous if and only if the mapping \(f \times f : (x, x') \rightsquigarrow (f(x), f(x'))\) is strongly continuous on the product metric space \(X \times X\).
- If \(f\) is strongly continuous, then it is uniformly sequentially continuous.
- If \(f\) is strongly continuous and \(f(X)\) is totally bounded, then \(f\) is uniformly continuous.
- If \(X\) is totally bounded and \(f\) is strongly continuous, then \(f\) is uniformly continuous.

The proofs of the second and fourth of these results are particularly involved, and introduce a proof technique that has other applications, for example in the theory of convergence of sequences of functions between apartness spaces. Note that we cannot pass, in general, from uniform sequential continuity to uniform continuity without using \(\BDN\).

We refer the reader to Chapter 3 of Bridges & Vîță [2011] for more information, including an extensive bibliography, about set-set apartness relations.

### Point-free topology

In point-free topology the ideal objects (points) \(X\) are taken as
basic and we group them together in ever narrower so-called *open
sets*. The set \(O(X)\) of open sets defines the topology, and is
required to be closed under arbitrary unions and finite
intersections. The open sets are often described in terms of basic
open sets, so that every open set may be written as a union of such
sets. These basic open sets can be thought of as approximations to the
points. To give a specific example, the topology of the real line
\(\bR\) may be described in terms of the basic open sets

where \(p\) and \(q\) are rational numbers. Each such basic open, an interval with rational endpoints, is specified by finite information and approximates all the real numbers \(x\) in the interval.

We may try to reverse the order of concepts, and take the basic opens,
or approximations, as fundamental, and derive the ideal objects or
points from the opens and their mutual relations. This is what is done
in point-free topology, a field which has a long history going back to
Wallman [1938], Menger [1940] and in its current form, Ehresmann &
Isbell; see Picardo & Pultr [2011]. There is also a precursor in
point-free geometry (Whitehead [1919]). We shall here concentrate
on *formal topology* (Sambin [1987]), which is a version of *
locale theory* (Johnstone [1982], Joyal & Tierney [1984], Picardo
& Pultr [2011]), where special consideration has been given to issues
of constructivity and predicativity. Some seminal examples in formal
topology were developed earlier in Martin-Löf [1970].

A *formal topology* is a triple \(\langle A, \le,
\cov \rangle\) consisting of a set \(A\) of basic opens, a
transitive and reflexive relation \(\le\) on \(A\), and a relation cov
between elements of \(A\) and subsets of \(A\). The relation \(a \le
b\) is understood as (formal) inclusion, whereas \(a\) cov \(U\) is
read \(a\) is covered by \(U\). These are supposed to satisfy the
following natural axioms.

- \(\mathbf{ER}\) (extension and reflexity): \(a \cov U\), whenever \(a \le b\) for some \(b \in U\)
- \(\mathbf{T}\) (transitivity): \(a \cov V\), whenever \(a \cov U\), and for each \(b \in U\), \(b \cov V\)
- \(\mathbf{L}\) (localization): If \(b \cov U\) and \(a \le b\), then \(a \cov a \downarrow U\), where \[ a \downarrow U \equiv \{x \in A : x \le a \wedge \exists y \in U (x \le y\}). \]

A *point* in this topology is an inhabited subset \(\alpha\) of
basic opens which satisfies these conditions:

- \(\mathbf{F}\) (filtering): If \(a, b \in \alpha\), then there exists \(c \in \alpha\) with \(c \le a\) and \(c \le b\).
- \(\mathbf{S}\) (splitting): If \(a \in \alpha\) and \(a \cov U\), then for some \(b \in U, b \in \alpha\).

We think of a point as a set of approximations. The filtering property insures that any two approximations have a common refinement, whereas the splitting property allows an approximation to be refined in any way the cover relation allows.

For any set \(U \subseteq A\), we let \(U^*\) be the set of all points \(\alpha\) where \(a \in U\) for some \(a \in \alpha\). It can be shown that the points together with the sets \(U^*\) form a point-set topology in the usual sense, and that formal cover implies point-wise cover:

\[ a \cov U \Rightarrow \{a\}^* \subseteq U^*. \]The converse implication usually fails.

For any \(S \subseteq A\), we may define an associated closed subspace of \(\bA \equiv\langle A, \le, \cov\rangle\) by redefining the cover relation:

\[ a \covs U \equiv a \cov S \cup U. \]Note that if \(a \cov S\), then \(a \covs \varnothing\), so, in effect, the open set determined by \(S\), gets identified with the empty set, as far as mutual covering goes. The topology

\[ \mathbf{A}\text{-}S \equiv \langle A, \le, \covs\rangle \]represents the subspace corresponding to the points not in \(S\).

To illustrate the methods of formal topology, we give a proof of
the point-free *Heine-Borel theorem*:

\(\mathbf{HBT}\) *Every cover of the unit interval by open
sets has a finitely enumerable subcover.*

Note the use of “finitely enumerable” here. A set \(S\) is
called *finitely enumerable* if there exist a positive integer
\(N\) and a mapping \(f\) of \(\{1, \ldots ,N\}\) onto \(S\). If the
mapping \(f\) is one-one, then we say that \(S\)
is *finite*. If the pairset \(\{0, x\}\) is finite, then we can
decide whether \(x\) equals 0 or not. Thus (see Section 1 above), the
statement “every finitely enumerable subset of \(\bR\) is
finite” implies LPO.

To prove HBT, we need to construct the point-free reals. Accordingly, let \(\bR \equiv\langle I, \le_I, \cov\rangle\) be the formal topology given by the following data: \(I\) is the set of pairs \((p, q)\) where

- \(p \lt q\) are rational numbers, and
- such pairs are ordered by setting \((p', q') \le_I (p, q)\) if and only if \(p \le p'\) and \(q' \le q\).

A pair in \(I\) is regarded as specifying an interval with rational end points. The cover relation \(\cov\) is the smallest cover relation that satisfies the following axioms:

\[\begin{align} \tag{R1} &\text{for } p \lt p' \lt q' \lt q, (p, q) \cov \{(p, q'),(p', q)\} \\ \tag{R2} &\text{for } p \lt q, (p, q) \cov \{(p', q') : p \lt p' \lt q' \lt q\} \end{align}\]
These axioms describe two principal ways of covering an interval by
shorter intervals. The points of \(\bR\) are the *real
numbers*. We define the order of the points by taking \(\alpha \lt
\beta\) if and only if there exist \((p, q) \in \alpha\) and \((p',
q') \in \beta\) with \(q \lt p'\); we then take \(\beta \le \alpha\)
to mean that \(\alpha \lt \beta\) is false. It is possible to show
using transfinite induction on covers (cf. Coquand *et al.*
2003) that we have the following alternative characterisation of the
above cover relation:

\((p, q)\) cov \(U\) holds if and only if for any \(r \lt s\) with \(p \lt r \lt s \lt q\), there exist \(t_1 \lt t_2 \lt \ldots \lt t_n, n \ge 3\), with \(r = t_1, s = t_n\), such that each \((t_i, t_{i+2}) (1\le i \le n - 2)\) is included in some interval of \(U\) (Cederquist & Negri [1996]).

Let

\[ S \equiv \{(p, q) \in I : q \lt 0\} \cup \{(p, q) \in I : 1 \lt p\}. \]It can be shown that the points of \(\mathbf{R}\text{-}S\) are the real numbers in the interval [0, 1].

We now have the ingredients to prove HBT. To say that \(U\) covers the unit interval \(\mathbf{R}\text{-}S\) means that \((p, q) \covs U\) for all \((p, q)\). In particular \((-2, 3) \covs U\); that is, \((-2, 3) \cov S \cup U\). Hence for \(r = -1 \lt s = 2\) there are \(t_1 \lt t_2 \lt \ldots \lt t_n\) with \(r = t_1\) and \(s = t_n\), such that each \((t_i, t_{i+2}) (1 \le i \le n-2)\) is included in some interval of \(S \cup U\). Thus for \(i = 1, \ldots ,n - 2\), there exists \((p_i, q_i) \in S \cup U\) with \((t_i, t_{i+2}) \le(p_i, q_i)\). It follows that there is a finitely enumerable \(F \subset U\) such that \((-1, 2) \covs F\). But \((p, q) \covs (-1, 2)\) for all \((p, q) \in I\), so by transitivity, \((p, q) \covs F\). Hence \(F\) is a finitely enumerable subcover of the unit interval. This establishes the theorem.

Another surprising result about compactness is that Tychonoff’s theorem holds for formal topologies (Coquand [1992]). In classical point-set topology this theorem is equivalent to the Axiom of Choice (Johnstone [1982]). Moreover, the classically highly non-constructive Stone-Čech compactification has as well a constructive point-free version (Curi [2010]).

The category of (set-presented) formal topologies has good properties from a topological point of view: it has (finite) limits and (finite) colimits. In particular, it is possible to construct quotient spaces and to attach subspaces, so the category seems adequate for doing algebraic topology; see Palmgren [2009].

Many results in functional analysis have natural point-free proofs (Johnstone [1982], Picardo & Pultr [2011]); some of them—for instance, the Riesz representation theorem (Coquand & Spitters [2009])—can also be proved completely constructively. There are, in addition, methods for dealing with the Zariski topology and spectra of rings in a point-free way (Johnstone [1982]); here, too, it is possible to make constructive developments (Schuster [2006], Coquand [2009]).