The existence or otherwise of extensional subspaces is a
point of demarcation between pure mathematics and computer science.
The ubiquitous axiom of comprehension seems to be what mainstream
mathematicians have in mind when they insist that Set Theory provides
the foundations of their subject. On the other hand, neither
programming languages nor the type theories that are most popular in
computer science admit subtypes. (We do *not* mean the notion of
this name in object-oriented programming, which is like an extension
of the signature of an algebraic theory.) Subtypes in our sense
*are* used in software development, in the form of Floyd–Hoare
logic, with pre- and post-conditions, but it is an up-hill struggle to
teach programmers to use them!

The reason for this demarcation is that the essence of the development
in a mathematical argument is quite different from that in a
computation. Before the referee will allow me to say that an element
belongs to a subset, I must prove that it satisfies the defining
property. Otherwise, the rest of the argument has no meaning
whatever, and my paper is not published. From this point of view,
compilation of high level programming languages lies on the
mathematical side of the boundary. A (low level) computation, on the
other hand, proceeds irrespectively of whether or not a purported
mid-condition is satisfied: if it doesn’t, the behaviour of the
program may not be what the programmer had in mind, but it
nevertheless does *something*.

I am, of course, in favour of *constructive* mathematics, and
appreciate the analogy between programs and proofs, but opinions
differ as to what is regarded as constructive: my notion is stronger
than Johnstone’s [Joh82] but weaker than
Martin-Löf’s [ML84]. I have argued that what Per
Martin-Löf calls the “existential quantifier” and the “axiom of
choice” are not those used in geometry
[Tay99, Section 2.4], and nor do I consider that an
element of a subset needs to be *accompanied* by a proof of the
defining predicate. Such proofs may serve as guarantees, but at some
point we must eventually *trust* (the verification of) the
guarantee and carry on with the computation.

In crossing the demarcation from pure mathematics to programming, we
therefore have to extend the definition of functions that were
intended to be defined on a subset to the whole of the ambient set,
possibly at the cost of results that lie outside the intended target.
A target object that permits such extension without itself being
expanded is called *injective*, and such objects will play an
important role in this paper.

I see the crossing as building a “mathematically comfortable”
*platform*,
with more types (sets, spaces) than the underlying programming language,
but such that the terms (elements) become
programs when the richer type information is erased. The programming
language that we shall use was justified and developed in the previous
paper [A], so now we must consider ways of building
mathematical platforms. Category theory provides the language in
which to express both our requirements for “comfort” and the means
of satisfying them, although equivalent λ-calculi are needed
for the idioms of both mathematics and programming.

Programming languages include constructors for making new types from
old ones, but the additional mathematical types depend on
*terms*. A very general theory of such dependent types is
formulated in [Tay99, Chapter VIII], although I now
consider that to be too complicated. Simpler notions than the axiom
of comprehension are familiar in category theory: equalisers,
pullbacks, coequalisers and pushouts.

The present work is by no means the first to provide such extensions. One very simple idea is to split idempotents (Remark 4.1), which Dana Scott developed [Sco76]. However, a great deal of artificiality was piled on top of this, notably sum types with spurious additional elements: we shall find in Section 11 that stable disjoint coproducts are a mathematical comfort that we may reasonably demand as standard.

Another idea is to expand the *monoid* of (partial general)
recursive functions on ℕ to the *category* whose objects
are recursively enumerable subsets. Giuseppe Rosolini formulated
the abstract notion of partial maps (composing a *p-category*),
and constructed a category with subobjects from it [Ros86].
Peter Freyd and Andre Scedrov started instead from binary relations
(composing an *allegory*) [FS90].
Their theory also accounts for the way in which general sets may be
obtained from iterated powersets, traditionally known as the von
Neumann hierarchy. Bill Lawvere’s treatment [Law70]
describes and generalises the behaviour of comprehension in
toposes and other categories in which it already exists, but does not
explain how it *creates* new sets [Tay99, Exercises 9.45ff].
Other ways of expanding the class of types include the regular
and exact completions of categories.

The particular construction performed in this paper is based on a monad.
In the original *mathematical* development of monads,
Eilenberg–Moore algebras were given a preferential role
[Eck69, BW85].
Later, Eugenio Moggi demonstrated how they could be used
to encode features of *computation* [Mog91],
but the new types that he introduced were objects of
the *Kleisli* category, which consists of just the *free* algebras.
So the literature that has ensued
illustrates the demarcation between mathematics and computer science.
In particular, the basic form of our construction without the subspaces
(Section A 6)^{1}is similar to work of Hayo Thielecke [Thi97a],
which uses the the Kleisli category.

In none of these constructions is a type defined as a “collection”,
as Solomon Feferman claimed to be a necessary ingredient of
mathematical foundations [Fef77],
and nor is a subtype a sub-collection selected by some kind of demon.
Both the underlying programming language and its mathematical enrichment
may be defined as λ-calculi with certain syntactic rules of formation.
Of course, there is a (recursive) collection of well formed formulae
(or of objects and morphisms in the category),
but this cannot be what Feferman’s argument means, as it applies
equally to Set Theory itself.
The metalanguage of category theory and type theory is not only
first order, as is that of Set Theory, but essentially algebraic.
In our case, the universal properties of Σ-split (co)equalisers
are *equational*, so the quantifier complexity is even less.

Many of the mathematical intuitions on which our calculus is based
come from general topology, regarded as a more subtle form of set theory.
This research programme is named after Marshall Stone
because he was the first to emphasise that
one should always look for the *topology* on any mathematical
object that one has constructed, since the appropriate morphisms are
*continuous* functions, not arbitrary set-theoretic ones
*à la* Cantor. (See the Introduction to [Joh82]
for a historical survey of this point of view.)

Contrary to what Richard Dedekind and Georg Cantor have told us,
*this is how the real line **ℝ** is defined*:
we understand the *topology* Σ^{ℝ}
because this is the abstraction of the convergence of sequences of rationals
(or of otherwise algebraically definable numbers),
and this is the *only* way
by which we gain access to transcendental numbers [I].
The space ℝ exists by *fiat*,
being defined *formally* as *pts*(Σ^{ℝ}).
Indeed, Bourbaki also constructed ℝ at the end of a tortuous chain of
definitions that spans an entire volume [Bou66],
but essentially recovers it from a topology
that is defined in terms of ℚ.

It was Dana Scott who promoted the analogy between continuity and
*computability*.
However, there cannot be a precise connection with
the *traditional* axiomatisation of general topology,
because it relies on *arbitrary* unions, rather than recursive ones.
It is principally this problem that Abstract Stone Duality seeks to address.

Monads provide a way of handling infinitary algebra of the kind that we need to re-axiomatise topology, and may be defined over any category, not just the category of sets. Specifically, we define the algebras that replace the lattices of open subsets of a space using a monad over the category of spaces itself.

This use of monads was also inspired by Marshall Stone’s work.
By *Stone duality* we understand the dual equivalence
between a category of algebraically defined objects
and another whose objects we think of as “spaces”,
though they may be sets, posets or algebraic varieties
as well as topological spaces.

By *abstract* Stone duality we mean some category ** S** of “spaces”
whose opposite category

The analogy between the two concrete examples of sets and locally compact spaces drives the intuition behind this programme. Temporarily using classical logic, including the axiom of choice, to present this intuition, these two monadic situations are illustrated by the following diagrams.

Adolf Lindenbaum and Alfred Tarski characterised full powerset
lattices classically as complete atomic Boolean algebras
[Tar35]. In modern terms, we formulate their result as
a mutually inverse pair of functors, one of which takes a set *X* to
its powerset ℘ *X*, and the other extracts the set of
“atomic” elements of any complete atomic Boolean algebra.

The morphisms of ** CABA** preserve arbitrary meets and joins, and
the forgetful functor

The equivalence of categories re-states this concrete adjunction in
more abstract terms: the contravariant powerset functor
℘:*Set*^{op}→** Set** is

In the second diagram, ** Frm** is the category of

** LKSp** and

Again, the monadic adjunction may be seen abstractly,
where the powerset ℘ *X*≅Ω^{X}
is replaced by the topology,
*i.e*. the lattice of open subsets of *X*,
and the lattice itself is regarded as a space with the Scott topology.
The topology may be expressed as Σ^{X},
where Σ is the ** Sierpiński space**.
Classically Σ also has two points, one of which is open.

The theorems of Stone, Tarski and Lindenbaum that we have given
identified “atoms” or “points” in the lattices
as sets of sets.
This turns the set-theoretic membership relation on its head:
each “open set” (element of the algebra)
*belongs to* certain “points”,
*i.e*. these correspond to certain subsets of the algebra.
However, the existence of *enough* ideal points
to separate the elements of the algebra
is equivalent to the axiom of choice,
or at least to some weaker proper axiom such as the prime ideal theorem.
Just the same problem arises in model theory,
models being the “ideal points” of the predicate calculus.

In the following two sections we show how, when the category of “spaces” satisfies the abstract Stone duality, it admits subspaces that carry the subspace topology. This is a special case of Jon Beck’s general characterisation of monadic adjunctions: under the duality, subspaces correspond to quotient algebras, and Beck’s theorem says that we may calculate certain kinds of quotient algebras simply as quotients of their carriers. For textbook accounts of monads and Beck’s theorem, see [Mac71, Section VI 7], [BW85, Section 3.3] or [Tay99, Section 7.5]. Our discussion in Section 3 is partly intended to amplify these accounts by giving a worked example of Beck’s theorem, in the hope that it will cross the demarcation and become better understood in the theoretical computer science community.

Theorem 3.11 gives an *intuitionistic* proof of
Stone duality for locally compact locales. After this, there is no
more topology in this paper: that story — in particular,
the equivalence between Eilenberg–Moore and frame homomorphisms —
is taken up in [C][G].

Sections 4–6 build a new category ** S**
with the abstract Stone duality from one that simply has products,
powers of Σ and all objects sober. The construction is based
directly on Beck’s theorem, formally adding Σ-split equalisers.
The main difficulty is in showing that

Section 7 briefly describes an alternative construction that uses algebras instead.

Sections 8–10 investigate an
equivalent λ-calculus, whose *types* admit subspaces that
are described using something like the axiom of comprehension in set
theory. However, these type annotations, like the mid-conditions in
Floyd–Hoare logic, are *computationally anodyne*: they remain in
the journal papers and are not used at run-time. The *terms* may
be stripped of this complex type information, leaving a simple
λ-calculus with application and abstraction.

The final section constructs stable disjoint coproducts and Σ-split coequalisers.

Some comment is in order on the fact that locally compact locales,
rather than *all* locales, provide the leading model of our axioms.
Fundamentally, it is the *category* that we seek to axiomatise,
not the spaces, and one category has the monadic property, whilst
the other doesn’t.
Indeed, the axioms for locales hardly enjoy the same unanimous acceptance
in the mathematical community as do those for, say, groups.
*Spatial* locales agree with *sober* spaces, but even then
disagree as to their products outside the locally compact case,
whilst there are numerous competing axiomatisations of convergence
and other features of topology.
The traditional one has also long been
regarded as unsatisfactory on the grounds that its *logical*
properties (such as cartesian closure) are inadequate.
This paper breaks new ground in treating topology as λ-calculus.

The simple technical reason for the “restriction” is that the
exponential Σ^{X} is only defined when *X* is locally compact.
However, Steven Vickers has shown how the functor Σ^{Σ(−)}
may be extended to all locales, decomposing it into two covariant
functors that are of interest in themselves [Vic04a].
However, the Eilenberg–Moore category for his monad is not the
category of frames, but one whose opposite he calls the category
of *colocales*.
When *X* is a locale, Σ^{X} is a colocale, and *vice versa*,
so observations belong not merely to a different *type* from
values, but to another *category*, whilst meta-observations
are again like values.
Our experience since Turing that computations are ultimately untyped
seems to have been sacrificed on the altar of conformity with a
pre-existing mathematical structure.

I acknowledge, on the other hand, that my mathematical platform is not
as comfortable as we might like. In particular, the
*intersection* of two Σ-split subspaces need not be
another locally compact space.
Before we are allowed to form an equaliser or
coequaliser, we have to satisfy a very awkward property,
which turns out to have no computational meaning anyway.
(It also leads to mis-conceived questions
such as largest cartesian closed categories:
the statement that “John is the tallest person who can stand up in here”
may say more about the ceiling than about John, if we are talking about
children in a tent.)
You pays your money, you takes your choice:
my construction has a good λ-calculus,
whilst locales have (infinitary) algebra,
which Vickers’ work has exploited very fluently.
Plainly we should be asking for both, and there is no fundamental
reason why we shouldn’t have them. The resulting category will have
many more objects besides locales and colocales,
and will in fact be cartesian closed.
So the argument from authority (or at least from familiarity)
seems to caution against a too hasty search for generality.

The applications to topology do, unfortunately,
go rather quickly outside local compactness.
Some account of the category of locales
is therefore needed quite urgently in abstract Stone duality,
and I hope that Vickers’ work will help towards this.
It is possible that such a construction would be the first step of
an iteration that would lead to the bigger category,
whilst retaining the *essence* of topology that we distill here.
I believe that this lies in the preservation by Σ^{Σ(−)}
of certain kinds of equalisers,
but more liberal notions of subspace and injectivity will be needed.

Nevertheless, both domain theory and rather a lot of the corpus of pure mathematics may be seen as going on in the category of locally compact spaces, so it is well worth continuing to investigate what can be done in the abstract setting that we have so far.