An Elementary Theory of Various Categories of Spaces in Topology

Paul Taylor

27 May 2005

Abstract

In Abstract Stone Duality the topology on a space X is treated, not as an infinitary lattice, but as an exponential space Σ^{X}. This has an associated lambda calculus, in which monadicity of the self-adjunction Σ^{−} ⊣ Σ^{−} makes all spaces sober and gives subspaces the subspace topology, and the Euclidean principle F σ ∧ σ = F ⊤ ∧ σ makes Σ the classifier for open subspaces. Computably based locally compact locales provide the leading model for these axioms, although the methods are also applicable to CCD^{op} (constructively completely distributive lattices).

In this paper we recover the textbook theories, using the additional axiom that the subcategory of overt discrete objects have a coreflection, the “underlying set” functor. This subcategory is then a topos, and the whole category is characterised in the minimal situation as that of locally compact locales over that topos.

However, by adding further axioms regarding the existence of equalisers and injectivity of Σ, we find the category of sober spaces or of locales over the topos as a reflective subcategory, whilst the whole category is cartesian closed and has all finite limits and colimits.

Instead of building cartesian closed extensions of the textbook categories by traditional set-theoretic methods, all of these categories (and their underlying topos) are developed entirely synthetically from the ASD lambda calculus, which is therefore logically complete. The methods are briefly applied to give a synthetic explanation of a topology on the set of continuous functions that has been known since the 1970s and satisfies the β- but not the η-law.

We conclude with a proposal for a new theory (in categorical and symbolic form) for a cartesian closed category for recursive topology.

This paper therefore puts the study of topological spaces and locales on a new foundation, just as elementary toposes did for sets.

Please note that the introduction to this paper is a rather hurried first draft, intended to allow me to put the paper on the Web in advance of my presentation at FMCS. This introduction also includes material that has been moved or duplicated from other parts in the paper, where the narrative consequently needs to be mended.

The final version of this paper is intended to consist only of the arguments within the ASD calculus that reconstruct locales etc., that is, what might be called the “syntactic” side. The “semantics”, i.e. the construction of a model for these axioms, probably starting from equilogical spaces, will end up in a separate paper. However, I intend to have the main parts of that construction in place before I submit this paper to a journal, in order to forestall any complaints regarding the consistency of the axioms.

1 Introduction

History and boundaries of topology

General topology grew throughout the twentieth century by accumulation of examples, from ℝ^{3} and ℝ^{n} to Banach spaces, Stone spaces and Scott domains. Many of its central concepts — convergence, continuity, compactness — have much deeper roots. It deals very well with these properties in individual spaces, or in many classes of spaces of varying generality that are intended for specific mathematical purposes. The subject shares its origins with set theory, indeed we think of many of the early authors — Hausdorff, Kuratowski and Sierpiński, for example — as belonging equally to the two displines.

These disciplines have not, however, been equally successful in defining the boundaries of their respective universes.

Remark 1.1 We learned from the tradition of Modern Algebra and its heir, category theory, that such universes of mathematical objects are not defined by the elements of the objects, or even by properties of the individual objects as a whole, but by saying what constructions generate newly admissible objects from old ones. For example, in set theory, we may form products, powersets and subsets of whatever sets we please. These operations ultimately acquired a very crisp categorical reformulation in the notion of an elementary topos. In linear algebra, there are agreements between products and coproducts and between subalgebras and quotients that became the notions of exact and Abelian categories.

The mechanics of general topology have not lent themselves to a similarly convincing account of the general constructions for topological spaces. Indeed, the subject is notorious for its chaotic assembly of definitions — whilst [34] provides an excellent census of this assembly, would anyone choose to organise a treatise on linear algebra or complex analysis around its counterexamples?

Remark 1.2 The “official” category of topological spaces and continuous functions that we have in the textbooks — we shall call them Bourbaki spaces to strip them of their official status — has been regarded by many as inconvenient. The usually cited reason for this is that it is not cartesian closed — it does not treat continuous functions as “first class citizens”, to borrow a slogan from functional programming. Of course, the notion of pointwise convergence has been employed for a long time, both directly in analysis, and indirectly to define a topology on sets of functions. But its inadequacy has also been long recognised, particularly in the case of Fourier series, where sequences of smooth functions converge to a discontinuous limit.

Sixty years have passed since Ralph Fox defined what we might analogously call compactwise convergence, usually known as the compact–open topology on the set of continuous functions X → Y. He pointed out that this was well behaved only when the space X was locally compact. It took another twenty years before the abstract notion of cartesian closed category was formulated, as a language in which to state this good behaviour, although we now know that Church’s λcalculus could already have done the job. But that didn’t solve the problem: it merely posed it more clearly.

The formal necessity of local compactness gradually became clear, at least if one wanted to stay within the official category of topological spaces and retain its continuous functions and products. The role of the Sierpiński space Σ as the crucial case for Y was identified by Dana Scott, although Day and Kelly had earlier shown the necessity of (what is now known as) the Scott topology on Σ^{X}.

The category of locally compact spaces is closed under the construction Σ^{(−)}, but it does not have general exponentials. In particular, whilst ℕ is locally compact, ℕ^{ℕ} is not, although this still exists in the category of Bourbaki spaces. But the next exponential, ℕ^{ℕ^{ℕ}} no longer exists there.

So, whilst there are far too few locally compact spaces, the category of all Bourbaki spaces does not solve the problem either.

[Hierarchies of continuous functionals; Filter spaces; Equilogical spaces.]

Remark 1.3 But now that the suitability of the official category has been brought into question, on the grounds of its lack of function-spaces, we should also examine how well it captures other traditional applications that might reasonably be called (generalised) topology.

Take differentiation and integration, for example: \frac{d}{dx}(−) and ∫_{a}^{b} (−)dx are linear functionals, i.e. they operate on (suitable) functions to yield functions or numbers, so we might expect them to belong to higher function-spaces. But these do not exist as Bourbaki spaces: quite different mathematical technology had to be invented to speak of them. If we had a notion of topological space that admitted such higher function-spaces, it would also encompass more general measures or distributions, and Dirac’s δ-“function” would become a genuine one.

In summary, we believe that there is some such more general notion of topological space, of which the definition that appears in the textbooks captures only a part. In other words, Bourbaki’s definition draws a certain boundary that is more a feature of its “co-ordinatisation” than of the geography of the subject itself. A corollary of this is that, if we chose a different “co-ordinatisation”, that is, if we made a new selection of basic concepts for topology instead of points and open subsets, we would draw different boundaries.

Products, topology and subspaces

Remark 1.4 Although Σ^{X} is a very special function-space, it has at least three methodological advantages:

• calculating with it is a great deal simpler than with the general case;

• there is an interesting and well known, if inadequate, subcategory (locally compact spaces) that is closed under it; and

• it exploits some of the intuitions of the powerset in set theory. Categorically, before we can define function-spaces (exponentials), we have first to have finite products. We also need to form subspaces, which we understand categorically to be equalisers of parallel pairs of continuous functions. Once again, not all equalisers exist in the category of locally compact spaces, so we may perhaps impose restrictions on the pairs whose equalisers we demand.

Axiom 1.5 Throughout, let S be a category with finite products and an object Σ of which the exponential Σ^{X} exists in S for every object X ∈ obS.

The construction Σ^{(−)} is a contravariant functor, Σ^{f} being the “inverse image” operation. Since we shall need to iterate it, we shall usually write ΣX for Σ^{X}, and Σ^{n}X for the “tower” of n Σs with X at the top.

[Equivalent λ-calculus.]

Example 1.6 In the category of locally compact spaces, Σ^{X} is the set of open subspaces of X, itself equipped with the Scott topology. The category of all Bourbaki spaces is not an example of the Axiom, but we shall show instead how it can be emdedded as a subcategory of one.

Example 1.7 Recalling the precedent of the common origins with set theory, a basic universe in that subject (an elementary topos) also can be axiomatised in terms of products, subsets and powersets. As is well known, these are enough to construct function-sets, sums, quotients by equivalence relations and many other things. Similarly, we shall find that Σ^{X}, products and subspaces suffice in general topology. □

Example 1.8 The category of posets and monotone functions also has this structure, Σ^{X} being the lattice of upper subsets of the poset X, ordered by inclusion. □

Sobriety

Remark 1.9 A feature of general topology that emerged from Grothendieck’s work in algebraic geometry was that the open subspaces of a space are more important than its points. Indeed, topology often enriches algebra with new points, such as irrational and p-adic numbers, and generic points on algebraic varieties. Locale theory has now succeeded in developing a large part of the corpus of general topology using open subspaces but without mentioning points.

A space that has exactly the points that its open subspaces require is called sober. Nonsober spaces are merely sets with topological decoration. They have been the source of numerous distracting counterexamples, for example in the theory of locally compact spaces and in the proof of Tychonov’s theorem about products of compact spaces.

Lemma 1.10 Σ^{(−)} ⊣ Σ^{(−)}, where the unit is x : X ⊢ ηx ≡ λϕ. ϕx : Σ^{Σ^{X}}. □

Definition 1.11 An object X is abstractly sober if this diagram is an equaliser in S:

[figure: X; ηX; Σ^{2}X; ηΣΣX; ΣΣηX; Σ^{4}X]

Remark 1.12 If, for the moment, we accept the claim that all topological constructions can be generated from products, equalisers and Σ^{(−)}, and also assume that the base types (ℕ and Σ) are sober, then we have no need ever to introduce non-sober objects. This is because the three basic constructions all take sober objects to sober objects.

Remark 1.13 Whilst we claim that objects whose significance is purely topological must be sober, for a variety of reasons we may wish to consider some other kind of mathematical structure (a group, for example), and endow that with a topology. In this situation, we have the Bourbaki idiom of a pair (X, 𝔒) consisting of a set X of points together with a topological structure 𝔒.

Classically, 𝔒 is a prescribed family of “open” subsets of X that is closed under finite intersections and arbitrary unions, which locale theory re-axiomatised in the obvious infinitary algebraic way. However, we may understand it more generally, to denote an abstractly sober object of our category S that is intended to be the new notion of topological space. In order to regard 𝔒 as a topological space (U𝔒, 𝔒) in the Bourbaki idiom, we need either to define what its underlying set U𝔒 is to be, or to regard any set as a space (X, ΔX) with the discrete topology.

How can we reconcile this with saying that all topological spaces are sober? Quite easily: as it says, this structure is a pair consisting of a set X and a (sober) topological structure 𝔒. These are linked by a function i : X → 𝔒. What sort of function? This depends on whether we reduce 𝔒 to its underlying set, in which case i is any function between sets, or endow X with the discrete topology, making i continuous.

Remark 1.14 Writing E and S for the categories of sets and of abstractly sober spaces (whatever these may be) and Δ : E → S for the functor that ends each set with its discrete topology, these pairs (X, 𝔒) form the comma category Δ ↓ S, whose morphisms are commutative squares

[figure: ΔX_{1}; i_{1}; 𝔒_{1}; ΔX_{2}; Δf; i_{2}; 𝔒_{2}; g]

where f : X_{1} → X_{2} in E and g : 𝔒_{1} → 𝔒_{2} in S. In locale theory, g is an abstract morphism of locales, whose concrete manifestation is a homomorphism g^{∗} in the opposite sense of the corresponding algebras.

Actually, Bourbaki spaces are not quite as general as this: since 𝔒 consists of subsets of X, the map i : ΔX → 𝔒 must be epi in the (weak) categorical sense. On the other hand, homotopy theory makes use of a similar structure in which i is mono, namely when we specify a subset of “base” points for a space [6]. Vickers’ category of topological systems [38] develops some of the basic ideas of topology in this way, neither requiring the map to be epi nor mono, and taking S to be the category of locales.

The comma categories Δ ↓ S and E ↓ U are equivalent when Δ ⊣ U. They have been studied and used extensively, and have a great deal of structure (limits, colimits and exponentials) that is derived by standard abstract methods from the corresponding structure of E and S [37, §7.7]. In fact, it is E that does most of the work in providing this structure in the comma category, which explains why not necessarily sober spaces have so many of the properties of sets: as we said, they are sets with topological decoration.

In conclusion, when we wish to “equip” a pre-existing set X with a topology 𝔒, we do so by providing a function X → 𝔒. The confusion that arises from non-sober spaces is attributable to the fact that we have a composite construction: we should recognise it as such, and not import set-theoretic clutter into topology itself.

Subspace topology and injectivity

Injectivity of Σ or subspace topology

Abstract Stone Duality

Remark 1.15 ASD is a re-axiomatisation of topology that is based on the ideas that we have just set out. It is called after Marshall Stone because it was he who first told us that mathematical objects (even those that arise from discrete algebra) should be regarded routinely as topological spaces, and not just as sets. The way in which we ensure that subspaces have the subspace topology was also conceived as an abstract formulation of Stone duality.

Because ASD has a different co-ordinatisation of the subject, it draws its boundaries in different places from the Bourbaki theory. The concluding discussion of this paper suggests that the extended boundaries of ASD and of traditional topology lie in roughly the same place, but their precise location will be subject to the same uncertainty until we have developed more applications of topology of this generality.

What is clear is that, since ASD is formulated in terms of exponentials that do not exist in the category of Bourbaki spaces, the boundaries of these two approaches cannot coincide. To achieve a match, we must either

• impose a very drastic constraint on S, leaving just locally compact locales, or

• extend the theory to include objects that are far too complicated to correspond to Bourbaki spaces or locales, but then concentrate on a subcategory L ⊂ S consisting of relatively simple objects, showing that this (rather than the whole model) agrees with the traditional theory.

This sets us two different mathematical tasks, but much of the reasoning that we use to accomplish these tasks is common to both of them: they will diverge only in Sections 11ff.

Remark 1.16 Whilst ASD seeks to re-axiomatise general topology, Examples 1.7 and 1.8 show that its core ideas are shared by broader notions of “space”, of which sets and posets are other examples. It is Scott continuity that distinguishes “topological” spaces from other kinds, but the relevant axiom is only invoked quite late in the theory. There are also intermediate examples in which the finite intersections of topology are replaced by intersections that are indexed by sets of cardinality < ℵ for suitable cardinals ℵ, but we leave the interested reader to investigate ℵ-topology.

The examples that the theory set out in this paper encompasses are summed up by the following table. The rows list the cases of set theory, order theory and topology; in all but the set-theoretic case all morphisms preserve the order defined by the lattice structure on Σ, whilst in the setand order-theoretic cases all objects are equipped with a “universal quantifier” that makes them compact. CCD is the category of (constructively) completely distributive lattices; the category Pos is non complete with respect to our notion of subspaces with the subspace topology, and CCD^{op} is its completion.

The columns, which we refer to as situations, correspond to the choice between the minimal theory (of locally compact spaces) and the extended one that we have motivated. Notice that this distinction does not apply to sets and posets.

minimal  extended
Set or topos  } all objects are compact
Pos ⊂ CCD^{op}
all maps are monotone { ℵ-LKLoc ℵ-Sob ⊂ S
LKLoc  Sob ⊂ S

Intrinsic and imposed structure

Remark 1.17 In the process of recovering locales and Bourbaki spaces from our axioms, we reverse the usual relationship between sets and other mathematical objects, in which the latter are manufactured from set-theoretic ballast.

Since we axiomatise the category S of spaces directly, its objects carry their topological structure intrinsically, by virtue of belonging to the category. Amongst this generality of spaces, we identify first the subcategory E of “sets” and then a larger subcategory L that is (in one situation) like the category of “locales”.

In order to study the relationship between L and the categories of locales and of Bourbaki spaces over E, we must of course also define the latter. This is done in the usual fashion: the objects have carrier “sets” chosen from E, on which structure (that of infinitary algebras) is imposed, in the sense that it must be given in addition to the carrier set.

In order to follow our argument in this paper, it is therefore crucial to understand this distinction between intrinsic and imposed structure.

Structure is being imposed whenever we formulate a definition such as that “a widget is a set equipped with ...” in mathematical discourse, for example when a Bourbaki space is defined as a set (of “points”) together with a collection of its (“open”) subsets. I have described this kind of topology as “chipboard” (sawdust plus glue), whereas ASD is about “real wood”. Bourbaki’s [4] is the canonical account of imposed structure as a foundation for mathematics.

In contrast, the quantifiers and equality predicates that we shall introduce are intrinsic structure on the objects that we shall call overt, compact and discrete. The use of intrinsic structure was pioneered in synthetic domain theory. In that subject there is, for example, and object ϖ whose definable elements are 0, 1, 2, ..., ∞, and form an ascending sequence according to the intrinsic order [36]. The usual arithmetic order on ℕ, by contrast, is imposed.

This distinction will start to play an important part in Section 8, where we study the underlying sets Ω and ΩX of the Sierpiński space Σ and the topology Σ^{X} of a space X.

Translating our results back to the traditional theory

Once we have shown how locales and Bourbaki spaces are embedded as subcategories of our newly axiomatised category S of generalised topological spaces, we may, on the face of it, deduce the

Theorem 1.18 Any theorem of the complete or exact ASD λ-calculus whose types lie in L ∩ P or L is valid in the categories of sober spaces or locales respectively. By this we mean, strictly, that:

• if a term is well formed in the calculus for S, and the types of the term itself and of its free variables all lie in L ∩ P or L, then that term denotes a morphism of Sob or Loc, and

• if any two such terms are provably equal in S then the corresponding morphisms are equal in Sob or Loc.

The ASD literature has already shown that a great many topological ideas can be expressed by such terms and equations. □

Remark 1.19 Unfortunately, there is a catch: in principle, the additional assumptions from which we have reconstructed Sob(E) and Loc(E) over the topos E may prove additional theorems about E itself. At worst this may make the whole theory inconsistent, but, short of that, could restrict our ability to substitute particular toposes for E. In other words, there is an issue of conservativity. We can tackle this either

• semantically, by finding a model over an arbitrary elementary topos, or

• syntactically, using proof theory to formulate a normalisation theorem for proofs in the calculus. Until this problem has been solved, our results remain “experimental”, but I am confident of

being able to find a model of the axioms as set out in this paper. On the other hand, these axioms are not intended to provide the definitive axiomatisation of the new category of topological spaces, and it may be much more difficult to find a model of the extended theory that I have in mind.

Remark 1.20 This brings us full circle, back to the cartesian closed extensions of the traditional category of topological spaces. There are essentially two of these: Martin Hyland’s filter spaces [13] and Dana Scott’s equilogical spaces [3], but Giuseppe Rosolini embedded them both in the exact completion of Sp [31]. However, all of these categories contain highly non-sober spaces and subobjects U ⊂ X for which Σ^{U} is larger than Σ^{X}. These objects are “builder’s rubble” — left-overs from the process of construction and not part of the architect’s plans — which we have to clear away.

Nevertheless, these categories are cartesian closed, and they contain Sob(E), which is enough. From any category S_{0} satisfying Axiom 1.5, we can construct one for which Σ^{(−)} ⊣ Σ^{(−)} is

monadic: it is simply S ≡ A^{op}, where A is the Eilenberg–Moore category for the monad on S_{0} [B].

We have to check that the sober topological spaces in the traditional sense are sober in S_{0} in the abstract sense of Axiom 3.3. Then the full subcategory Sob(E) ⊂ S_{0} is embedded unscathed in S, where Σ continues to enjoy its lattice structure, the Euclidean and Scott principles, and injectivity in L. The underlying set axiom also holds in S_{0} and S.

Hence we have a model of all of the Axioms up to 3.24.

But it may contain Loc(E) too, i.e. Σ is exactly injective (Theorem 12.9). This would follow from the property that X ∈ obL ⇒ Σ^{X} ∈ obP.

2 The underlying set functor

Abstract Stone Duality, as it has been studied in previous papers, has given an account of computably based locally compact spaces [G]. The way in which the earlier theory ensured that subspaces carry the subspace topology has to be strengthened, i.e. made to apply to more general subspaces, in order to extend the theory beyond local compactness.

However, since locale theory and Bourbaki spaces are formulated in the text books over a set-theoretic base, or over an elementary topos, we add another “underlying set” axiom that has no computational interpretation. In fact, we have already used this in Remark 1.14 to recover non-sober spaces from a theory of pure topology in which all spaces are sober.

Remark 2.1 In topological language, here is the central idea for the additional axiom. Recall that, classically, the category of (not necessarily T_{0}) spaces is related to the category of sets by the adjunctions

Sp

Set^{discrete }⊣ ⊣ indiscriminate

where the middle functor yields the underlying set of points of a space and the other two equip any set with its greatest and least topologies. On the left is the discrete one, in which all subsets are open. On the right is the indiscriminate one, in which only the empty set and the whole space are open. However, the rightmost functor no longer exists if we require the spaces to be T_{0} or sober, so it will not feature in this paper.

Remark 2.2 Although abstract Stone duality is formulated without any reference to “sets” at all, the full subcategory E ⊂ S of overt discrete objects has emerged as the replacement for the category of sets in various roles in general topology. The inclusion of this subcategory corresponds to the leftmost of the above functors, so we consider the hypothesis that this inclusion have a right adjoint.

Remark 2.3 We find in this paper that adding this hypothesis to the axioms of abstract Stone duality as studied elsewhere in the programme, together with others about subspaces, precisely recovers the theories of locally compact, spatial and general locales over E.

That is, apart from the fact that the topos E is itself constructed from the axioms. In other words, the elementary theory of toposes [23, 24] is essentially a part of our theory.

This is not the usual situation in a mathematical discourse, where the foundational system (whether it be Set, another topos, traditional set theory or a type theory) is an assumption, albeit a silent one. However, those who have studied constructive systems and compared them with their classical counterparts have learned that the latter must be observed in their native habitat, for example Bourbachiste topology has to be done in the context of the axiom of choice. In other words we must be holistic, taking the mathematical structure and its foundations together.

If, therefore, you require locales over a particular topos E_{0} (such as the one that you choose to call “Set”), the theory has to be extended with base types, constants and equations that force E ≃ E_{0}.

Remark 2.4 More significantly, the infinitary joins that are needed to axiomatise either traditional topology or locale theory are also a consequence of the axioms, and not a part of them. This is the sense in which the new axiomatisation deserves to be called elementary. In fact, the logical power of the theory (powersets in the topos, and the infinitary joins) arises out of the “underlying set” axiom.

Remark 2.5 The “underlying set” axiom is also equivalent to saying that the category S of “spaces” is enriched in or locally internal to the category E of “sets”, i.e. that the hom-objects S(X, Y) belong to E. (In particular, we say that S is locally small when S(X, Y) ∈ Set.) The “underlying set” is a special case, UY = S(1, Y), and we derive the functor S(−, −) : S^{op} × S → E from U : S → E in Theorem 5.6.

Remark 2.6 Enrichment of S in E_{0} is needed before we can define sheaves or “variable sets” over S, where the “sets” are to be objects of E_{0}. This question is of interest because sheaves provide one of the techniques that have been proposed for extending the category of spaces or locales, for example in order to obtain a cartesian closed category. Of course, there’s no problem if we have E_{0} = Set, but then we’re hardly getting very far away from the classical situation. If we want the subcategory E ⊂ S of overt discrete spaces to play the role of E_{0} then S must be E-enriched, so the “underlying set” functor must exist, E itself must be a topos,

Recursion

Remark 2.7 Abstract Stone duality is a re-axiomatisation of general topology that is intended to unify it with recursion theory. Its motivation was to make bi-directional the connection that Dana Scott made with programming languages via denotational semantics. The category defined by the term model has been shown to be equivalent to the category of computably based locally compact spaces and computable continuous functions [G].

To do this, the new recursive theory of topology must, of course, be logically much weaker than the traditional one. In this paper, on the other hand, we identify the additional ingredient that is needed to make ASD equivalent to standard topology, or rather to an extension of intuitionistic locale theory over an elementary topos.

As far as the development of ASD in itself is concerned, this paper investigates a natural way in which its spaces can be assigned “underlying sets” such as they have in other theories. However, this investigation also provides the precise connection with some of those other theories. Curiously, the boundaries of those theories (locales and sober spaces) turned out to be like “reflections” or “shock waves” from the boundary of the “underlying sets”, in the sense that the axioms which secure the connection as far as those boundaries become impotent immediately outside them.

In particular, we would like a “recursive” version of the theory, i.e. not involving the “underlying set” axiom. As we shall see, this axiom is implicit in the statement of injectivity, which as it stands cannot be extended (much) beyond L. So injectivity needs to be replaced by a more sophisticated property, for which we make a proposal in Section 14.

The “underlying set” axiom is also computationally unacceptable.

and we have lost the intended unification with recursion theory.

Remark 2.8 As well as enlarging the classes of spaces and continuous functions to include noncomputable ones, the extra feature adds more proofs. In particular, it has the effect of replacing the intensional equality of the recursive theory (in which programs have to be specified, at least up to provable equivalence, in order for things to be considered “computable”) by the more traditional extensional equality.

Since the “underlying set” that this right adjoint assigns to any space lies in the subcategory of overt discrete objects, it is equipped with an equality test and an existential quantifier.

Remark 2.9 But the purpose of abstract Stone duality was to unify general topology with recursion theory, and in particular to legitimise the class of recursively enumerable subsets as a (indeed, the) topology on ℕ. This cannot have an “underlying set”, because the equality operation on that space would solve the Halting Problem. The new axiom would, therefore, not be an acceptable addition to the principal version of the theory.

Generally speaking, moreover, although the structures that we discuss in this paper, especially in Section 9 (Heyting implication, direct image, arbitrary joins), are very familiar from the literature of locale theory and categorical logic, they are just the structures that are forbidden in the main (recursive) version of ASD, which must therefore be developed using different techniques.

Footnotes

The fact that our central idea is that sets with equality form a coreflective subcategory of the category of spaces brings to mind some other points of view that have arisen in the background to this subject, which we pause to consider.

Remark 2.10 In set theory the axiom of extensionality, though it may appear innocuous to the naïve observer, actually carries much of the force of the theory. Dana Scott showed [32], for example, that Zermelo–Fraenkel set theory (ZF) without extensionality is provably consistent within Zermelo set theory (Z). (Recall that ZF is Z plus the axiom of replacement.)

Remark 2.11 When well-foundedness is presented in categorical terms using coalgebras, the extensional ones form a reflective subcategory, but the axiom of replacement may be needed to construct the reflection functor [37, Exercise 9.62].

Remark 2.12 In synthetic domain theory the category of predomains is a reflective subcategory of some topos, where here the topos is coreflective in the category of spaces. Beware that some of the remarks in the (historically) first paper on ASD, Geometric and Higher Order Logic [C], were written with that situation in mind, rather than the present one. This applies specifically to 2.10(b), 2.13 and especially 8.9 in that paper.

Nevertheless, the present paper follows on very closely from that one, which you would be well advised to have to hand. It tidies up a few of the many loose ends, developing in particular Remarks 6.14–15 from there.

3 Axioms

For the sake of brevity, we state the axioms here in categorical form, and develop the standard examples and theory from them in the following sections in the same way. But we then introduce a symbolic language for the “underlying set” axiom in Section 7. Such languages corresponding to the other categorical axioms (1–6) are summarised in [B, §8].

The correspondence between type theory and category theory is explored in my book.

In order to emphasise the importance of certain axioms of ASD that other authors have chosen to omit from their systems, we mention a few of their “higher level” consequences, or present them as equivalences (in the context of the preceding axioms) with other principles of categorical logic.

Monadic structure

Axiom 3.1 Throughout, let S be a category with finite products and a pointed object ⊤ : 1 → Σ, such that the exponential Σ^{X} exists in S for every object X ∈ obS.

This structure can equivalently be expressed symbolically by a simply typed λ-calculus in which the formation of function-types and λ-abstraction is restricted [A, §2]. Topologically, Σ^{X} will be the lattice of open subspaces of X, where (the carrier of) this lattice is itself considered as another “space” (object of S), not as a set. We shall usually write ΣX for Σ^{X}, and Σ^{n}X for iterations (“towers”) of this functor.

Lemma 3.2 Σ^{(−)} ⊣ Σ^{(−)}, where the unit is x : X ⊢ ηx ≡ λϕ. ϕx : Σ^{Σ^{X}}. □

Axiom 3.3 Every object X ∈ obS is sober in the sense that the diagram

[figure: X; ηX; Σ^{2}X; ηΣΣX; ΣΣηX; Σ^{4}X]

is an equaliser in S.

The intuition is that an object is sober when it is determined by its topology. Classically, this means that we may recover a point as the “limit” or “focus” of its Scott-open prime filter of open neighbourhoods. Categorically, the topology functor Σ^{(−)} is faithful and reflects invertibility.

The symbolic calculus for this adds an operator called focus [A, §8], which we shall use in Remark 6.3. In the context of the lattice structure, sobriety of ℕ is equivalent to definition by description [A, §§9–10], and to general recursion [D].

Definition 3.4 A map i : X ↣ Y is called a Σ-split inclusion if there is some map I : Σ^{X} ↣ Σ^{Y} with Σ^{i} · I = id_{Σ^{X}}. For example, ηX is Σ-split by ηΣX. The endomorphisms of Σ^{Y} that arise as I · Σ^{i} can be characterised by a certain λ-equation [B].

Axiom 3.5 The self-adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic.

By Jon Beck’s famous theorem characterising monadic adjunctions, this says that (all objects are sober,) certain equalisers exist in S and that Σ^{(−)} takes them to coequalisers.

More formally, every endomorphism of Σ^{Y} satisfying the λ-equation that we mentioned actually defines a Σ-split subspace. There is a symbolic calculus for this [B, §8], but we shall (largely) avoid using it here.

Topologically, this provides certain subspaces and ensures that they have the subspace topology. A significant example of the importance of this in the recursive version of the calculus is that the closed real interval [I] and Cantor space (2^{ℕ}) are compact, whereas they fail to be so in other systems of recursive analysis.

It turns out, however, that we shall need to strengthen (NB not alter) the monadicity requirement in order to capture more general topological spaces.

This much is already enough to prove a basic property that any category of “spaces” ought to have.

Theorem 3.6 The category S has stable disjoint coproducts [B, §11]. □

A summary of the type-theoretic formulation of these axioms is given in [B, §8].

Lattice structure

So far we have said nothing to identify Σ as a special object of the category S. Indeed, any set with at least two elements satisfies the axioms stated so far in the case where S is Set and obeys the axiom of choice. It is the next property that makes it the “set of truth values”.

Definition 3.7 ⊤ : 1 → Σ in S is called a dominance [30] [37, §5.2] if

(a) the pullback of ⊤ : 1 → Σ along any map ϕ : X → Σ exists in S

[figure: U; 1; X; i; ∩; ϕ; ψ; Σ; ⊤]

(in this case we say call i an open inclusion and say that ϕ classifies it);

(b) if ϕ, ψ : X ⇉ Σ classify isomorphic inclusions i : U ↪ X then ϕ = ψ; and

(c) if i : U → V and j : V → W are open inclusions (classified by ϕ : V → Σ and ψ : W → Σ respectively) then so is j · i : U → W (and we write ∃_{j}ϕ : X → Σ for their classifier).

Notice that ⊤·!_{X} : X → 1 → Σ classifies id_{X}, and ϕ·f : Y → X → Σ classifies the pullback f^{−1}(i) of i along f : Y → X.

Theorem 3.8 If ⊤ : 1 → Σ is a dominance then there is a (unique) binary operation ∧ : Σ×Σ → Σ such that (Σ, ⊤, ∧) is an internal semilattice satisfying the Euclidean principle

σ : Σ, F : Σ^{Σ} ⊢ σ ∧ F σ = σ ∧ F ⊤.

Conversely, given such a Euclidean semilattice, Axiom 3.5 provides the open subspace i : U ↪ X that is classified by any given ϕ : X → Σ, as an equaliser. Moreover, since Σ^{(−)} takes this equaliser to a coequaliser, U has the subspace topology (the lower subset Σ^{X} ↓ ϕ).

Indeed, for any such open inclusion i : U ↪ X, there is a map ∃_{i} : Σ^{U} → Σ^{X} that satisfies ∃_{i} ⊣ Σ^{i} and the Frobenius and Beck–Chevalley equations [C, Sections 2–3]. □

We take as another Axiom the equivalent conditions of this Theorem.

Definition 3.9 An object N ∈ obS is called discrete if the diagonal subspace N ⊂ N × N is open, in which case we write (=_{N}) for the classifying map [C, Section 6].

[figure: N; 1; N × N; ∩; (=_{N}); Σ; ⊤]

Definition 7.1 says the same thing symbolically.

Definition 3.10 An object X ∈ obS is called overt if Σ^{!_{X}} : Σ → Σ^{X} (where !_{X} is the unique map X → 1) has a left adjoint (written ∃_{X}) and compact if there is a right adjoint (∀_{X}). The Beck–Chevalley laws, which allow substitution under the quantifiers, are inherited from the corresponding property of the λ-calculus, whilst the Frobenius law for ∃_{X} follows from the Euclidean principle [C, Section 8]. Definitions 7.2–7.3 provide the type-theoretic rules for the quantifiers.

Notation 3.11 We write E ⊂ S for the full subcategory of overt discrete objects, and K ⊂ E for those that are also compact. We typically use N and M (and Ω) for overt discrete objects, as these are the topological properties of ℕ, though “uncountable” sets are also overt discrete.

A summary of the type-theoretic formulation of these axioms is given in [I].

The minimal and other situations

Definition 3.12 In the minimal situation, each object X ∈ obS is a Σ-split subspace of some X Σ^{N} with N overt discrete. This says that S contains only the objects that are generated from overt discrete ones by means of exponentials Σ^{(−)} and monadicity (Axiom 3.5). Minimality is consistent with the existence of exponentials because, in topology and the other examples, each Σ^{Σ^{N}} is a retract of some Σ^{M} (cf. Corollary 10.5).

The fact that we obtained locally compact locales as the outcome of [G] is directly attributable to this axiom, and not, as certain people have claimed, to the assumption that all exponentials Σ^{X} exist, or to monadicity.

Lemma 3.13 In the minimal situation, each object X is an equaliser X ↣ Σ^{N} ⇉ Σ^{M} with N and M overt discrete.

[figure: X; i; Σ^{N}; ξ ↦ λΦ. Φξ; ξ ↦ λΦ. I(Φ · i)ξ; ΣΣΣN; j; Σ^{M}]

Proof Using Definition 3.12 both for X itself and again for Σ^{Σ^{N}}, let i : X ↣ Σ^{N} with Σ^{i} · I = id_{Σ^{X}} and j : ΣΣΣN ↣ Σ^{M}. Then, since X is sober (Axiom 3.3), the diagram above is an equaliser [B, Section 4]. □

Notation 3.14 In general, let L ⊂ S be the full subcategory of objects that can be expressed as equalisers X ↣ Σ^{N} ⇉ Σ^{M} with N, M ∈ obE. The sets N and M behave as “generators” and “relations” respectively for the algebra Σ^{X}, which is the coequaliser of Σ^{Σ^{N}} ⇇ Σ^{Σ^{M}} in the category of algebras, Σ^{Σ^{N}} being the free algebra on N. Corollary 6.9 provides a canonical choice for N and M.

The underlying set functor

Theorem 3.15 In the minimal situation, the following are equivalent:

(a) E ⊂ S is coreflective, i.e. the inclusion has a right adjoint U : S → E;

(b) S is E-enriched, so there is a functor S(−, −) : S^{op} × S → E with S(Γ × X, Y) ≅ S(X, Y)^{Γ} for Γ ∈ obE and X, Y ∈ obS;

(c) E is an elementary topos. Without minimality, (a) and (b) are still equivalent and imply (c), but (c) only provides a right adjoint L → E (not S → E) and gives L an E-enriched structure.

Coreflectivity means that for every object X ∈ obS there is a couniversal map ε_{X} : UX → X with UX ∈ obE, i.e. any map Γ → X with Γ ∈ obE factors uniquely as Γ → UX → X. Notation 7.4 expresses this type-theoretically.

Again we take as an Axiom the equivalent conditions (a,b) of this Theorem. One effect of it is to emphasise certain objects of the category:

Definition 3.16 An object X ∈ obS has enough points if the counit ε_{X} : UX ↠ X is epi. We write P ⊂ S for the full subcategory of such objects; Lemma 7.8 gives some equivalent properties.

Most of the development of this paper is also valid in Set and CCD^{op} — although the topological case is much more challenging. The recursive version of the theory may also have other applications, but the “underlying set” axiom has a consequence for the elementary structure of the theory which means that, qualitatively, it only applies to these three cases:

Proposition 3.17 Σ is a distributive lattice. Proof Any coreflective subcategory is closed under (colimits, but in particular) finite coproducts, which S has by Theorem 3.6 or, more simply, because S^{op} is monadic over S, which has finite products. Thus 0 and 2 are overt, and their existential quantifiers are ⊥ and ∨ respectively [C, Proposition 9.1]. We give a more detailed symbolic proof of this result in Section 8. □

A new type-theoretic formulation of these axioms will be given in Section 7.

Continuous structure

Only in Section 10 do we specialise to the topological case, but for completeness here is the axiom that does this. Even when we do specialise, it is largely so that we can use the traditional vocabulary in more or less its standard sense. We make surprisingly little use of the axiom: most of the structure that we develop after invoking it is not contradictory but redundant in Set and CCD^{op}.

Theorem 3.18 In the minimal situation, S is equivalent to the category of locally compact locales over E iff it satisfies the Scott principle that, for each N ∈ obE,

Φ : ΣΣN, ξ : ΣN ⊢ Φξ = ∃ℓ:KN . Φ(λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ξn,

where KN denotes the free semilattice or Kuratowski-finite powerset of N in the topos E.

As the other ASD literature shows, many of the familiar ideas in topology, domain theory and real analysis can be developed from three special cases of this principle:

Corollary 3.19 With N = 1, so KN = {0, 1}, we obtain the Phoa principle [C, §5],

F : Σ^{Σ}, σ : Σ ⊢ F σ = F ⊥ ∨ σ ∧ F ⊤,

which combines the Euclidean principle (Theorem 3.8), its lattice dual,

σ ∨ F σ = σ ∨ F ⊥,

and monotonicity of F. Then ⊥ : 1 → Σ is a dominance like ⊤, the subspaces that it classifies being called closed. □

Corollary 3.20 Let A ≡ Σ^{U} and Γ ⊢ F : A^{A}. Then Γ ⊢ α ≡ ∃n. F^{n}⊥ : A is the least (pre-) fixed point of F in the sense that Γ ⊢ F α = α and

{Γ ⊢ β : A  Γ ⊢ F β ≤ β \atop Γ ⊢ α ≤ β}  □

Corollary 3.21 Semicontinuity from [J].

Cartesian closure and injectivity

In the topological case we want to go beyond the minimal situation, but we then need some more axioms. According to categorical orthodoxy, the first of these should have been part of Axiom 1.5.

(We ask for general equalisers in S only in the following result. For the main development of the paper in the complete situation, we require equalisers only in L. I will revise this when I am sure whether or not the model that I have in mind has general equalisers.)

Theorem 3.22 If S has equalisers then it has all finite limits, colimits and exponentials Y^{X}, i.e. it is cartesian closed. Proof Any finite limit can be calculated using products and equalisers. Then since S^{op} is monadic over S, it “creates” finite limits, so S has colimits (this was Paré’s motivation [29]). Sobriety expresses any object Y as an equaliser of powers of Σ (Axiom 3.3); then for another object X we may form the diagram

[figure: Y^{X}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; η_{Y}^{X}; Σ(Σ^{Y} × X); Σ(Σ^{η_{Y}} × X); η_{Σ^{Σ^{Y}}}^{X}; Σ(Σ^{Σ^{Σ^{Y}}} × X)]

and verify that its equaliser also enjoys the universal property of the required exponential.

John Isbell [15, 16] used essentially this idea to define a topology on the set of continuous functions X → Y. It also provides the “continuation passing” interpretation of functions. □

Definition 3.23 The object Σ is injective (with respect to regular monos in L) if, for any equaliser diagram in L and ψ : U → Σ, there is some ϕ : X → Σ with ψ = ϕ · i.

[figure: U; i; X; f; g; Y]
[figure: ψ; .........; ϕ]

Σ

The Sierpiński space has this property in the categories of T_{0} topological spaces and of locales. Another way of saying this is that U has the subspace topology: every open subspace ψ of U is the restriction ϕ · i of some open subspace ϕ of X. This is important not only in topology but also set theory and order theory: the subobject classifier is injective in a topos or CCD^{op}.

In fact there is a good reason why the Sierpiński space fails to be injective in cartesian closed supercategories of spaces (Section 14), and this is why we only assert this property for L rather than S. Loc has a stronger property called exact injectivity that we shall explain in Definition 12.8.

Summing up these additional axioms, we make

Definition 3.24 In the complete and exact situations^{1}, L has all finite limits (i.e. equalisers as well as products and the other Axioms named above) and Σ is (exactly) injective in L.

Theorem 3.25 Our main results about the complete situation are that

(a) L is reflective in S (Section 13);

(b) L^{op} is a full subcategory of the category of algebras for a monad over E (Section 6). In the topological case these algebras are frames, so

(c) L ⊂ Loc(E) (Section 10) and

(d) L ∩ P is equivalent to Sob(E), the category of sober topological spaces or spatial locales;

(e) in the exact situation L^{op} is monadic over E, so L ≃ Loc(E) (Section 12). □

1Please do not use the words minimal, complete and exact elsewhere (especially complete): their purpose is merely organisational within this paper. You should refer instead to “Taylor’s synthetic characterisation of locally compact, spatial or general locales” or similar.

4 Semantic examples

Example 4.1 S may be the classical category of sets and functions, with Σ = {⊤, ⊥}. More generally, S may be any elementary topos, with Σ = Ω.

This is Paré’s theorem [29], and is treated in [C, §11]. It “cuts short” the theory in this paper, since all objects are overt discrete: K = E = L = P = S, Δ = U = id and ε = id. The requirements of the minimal, complete and exact situations are all met: all equalisers exist, all monos are Σ-split, and Σ is exactly injective.

Examples 4.2 The topological case is characterised by the Scott principle (Theorem 3.18), and K is the class of Kuratowski-finite objects. There are three sub-cases: the minimal, complete and exact situations, of which we consider the last two in the next section. The first can itself be presented in two ways, with or without the axiom of choice.

(a) S may be LKSp, the classical category of locally compact sober spaces, and Σ the Sierpiński space. Then the topos E is again Set, which must satisfy Choice. The inclusion functor Δ endows any set with its discrete topology, whilst the right adjoint U yields the underlying set (of points) of any locally compact space [A, Theorem 5.12]. The counit ε_{X} : UX → X is epi for all X ∈ obS, so P = S, and U is faithful.

(b) S may be LKLoc, the category of locally compact locales (i.e. the opposite of the category of distributive continuous lattices and frame homomorphisms) over an elementary topos. Now Σ is the free frame on one generator [B, Theorem 3.11]. Then E is equivalent to the given topos and, for N ∈ obE, ΔN is the powerset P(N) considered as a frame. Conversely, UX is the set of “points” of the locale X ∈ obS, in the sense of locale theory, i.e. homomorphisms from the frame (corresponding to) X to Σ [18, §II 1.3–7]. This functor (the right adjoint to Δ) exists in general in intuitionistic locale theory, but it is only faithful if we assume the axiom of choice.

Remark 4.3 Whereas countably (or rather recursively) based locally compact spaces or locales form a model of the recursive version of ASD [G], with the “underlying set” axiom, Set has to be a subcategory, so the category must include spaces of arbitrary cardinality too.

We need a couple of results in the standard formulation of the category LKLoc(E) of locally compact locales over any elementary topos E in order to connect this category with our new synthetic formulation in Section 11.

Lemma 4.4 Let N be a set (object of the topos E) and ΔN the corresponding object of S = LKLoc(E) as above. Then ΔN is overt discrete. Proof Its usual external (=_{N}) and ∃_{N} provide the required internal structure. □

Proposition 4.5 Let (A, ≼) be a complete lattice in E. This is a continuous [12] frame iff there is a set N ∈ obE and there are functions

A[figure: J; \underline{H}] ΥKN

such that J preserves directed joins, H preserves finite meets and arbitrary joins and H · J = id_{A} [G, Theorem 5.10]. □

Proposition 4.6 All overt discrete objects of LKLoc are sets. Proof By the previous result, any locally compact locale X can be represented as X ↣ Σ^{N} in LKLoc(E) for some N ∈ obE. Now, if X has internal structure making it overt discrete then it is the quotient of N by a partial equivalence relation [G, Proposition 7.1], and therefore X is a set too. □

Example 4.7 Consider the subobject classifier with its order: this classifies upper subsets of posets. However, Pos itself does not obey the monadic property: we have to “complete” it to S ≡ CCD^{op}, where CCD is the category of (constructively) completely distributive lattices and their homomorphisms [26]. In this representation, Σ is the free such lattice on one generator.

Now E is the base topos and ΔN is the powerset of N, considered as a completely distributive lattice. UX is the set of complete lattice homomorphisms from X (quâ lattice) to Σ. Again the mimimal, complete and exact requirements are all met (L = S), but P ⊂ S is Pos ⊂ CCD^{op}.

The characteristic property of this example is that every object is compact (K = E). However, to develop our type theory and so recover CCD^{op} from the axioms, we require compactness of “dependent types”, which can be avoided in the topological case (Remark 8.10). The study of CCD^{op} is therefore outside the scope of this paper.

There is a family of models that “interpolate” between the topological and order-theoretic models, which are the extreme cases ℵ = ℕ and ∞ respectively.

Example 4.8 Let ℵ be a regular cardinal. What we mean by this categorically is a class K ⊂ E of sets that includes 0 and 2, is closed under isomorphism, products and quotients, and also under unions indexed by members of the class [19]. The finite meets in the definitions of topological spaces, locales and local compactness may be generalised to those indexed by object of size < ℵ (or belonging to K), and the resulting locally ℵ-compact locales provide another minimal model.

These examples share a great deal of theory in the traditional presentation, notably the adjoint direct and inverse image operators corresponding to each map in the category (Section 9). We too shall find that they develop naturally in parallel, so we postpone the “Scott continuity” axiom until the end. Our techniques could therefore be applied to the somewhat less familiar CCD^{op}, which has hitherto been studied using lattice-theory and adjunctions, rather than either topological or symbolic methods.

Remark 4.9 It would also be possible to develop abstract Stone duality (with the monadic and Euclidean axioms) for models based on stable domains [C, Example 4.5] or maybe other treatments of sequential functions. In this case Σ does not have binary joins. Hence by Proposition 3.17 there is no “underlying set” functor, and S is not E-enriched. But as E doesn’t even have coproducts, maybe it is unsuitable as a category of “sets” anyway. □

5 The topos of overt discrete objects

We now begin the reconstruction of the traditional categories of spaces from the axioms in Section 3, starting with the category of “sets”. Specifically, this section proves Theorem 3.15, that the full subcategory E ⊂ S of overt discrete objects is a topos iff it is coreflective (in L).

However, the greater part of the proof was already in [C], which culminated in the blunter result that S itself is a topos iff all objects are overt and discrete, i.e. E = S. In particular, we rely heavily on the result proved there that any mono from an overt object into a discrete one is an open inclusion.

We begin with the proof of [C, Lemma 3.9(d)], which was missing.

Lemma 5.1 Let V ^{⊂} ^{j} U ^{⊂} ^{i} X be classified by ψ : U → Σ and ϕ : X → Σ respectively. Suppose E : Σ^{U} → Σ^{X} satisfies ϕ ≤ ψ ⇒ Eϕ ≤ Eψ, Σ^{i} · E = id_{Σ^{U}} and E · Σ^{i} = (−) ∧ ϕ. Then Eψ classifies V ↪ X.

Γ

[figure: . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .; u; .......; v]

[figure: V; 1; = = = = =; 1]

[figure: U; j; ∩; ψ; Σ; ⊤; 1; ‖]

[figure: x; X; i; ∩; ϕ; ∨; Eψ; Σ; ⊤]

Proof Let x : Γ → X form a commutative square to test the pullback of ⊤ and Eψ, so Eψ · x = ⊤ : Γ → Σ.

But Eψ ≤ E⊤ = ϕ, so ϕ · x = ⊤ also. Hence we have a mediator u : Γ → U to the pullback along ϕ, such that x = i · u and the composite

[figure: Γ; u; U; ⊂; i; X; Eψ; Σ]

is ⊤. But Eψ · i = Σ^{i}(Eψ) = ψ, so u forms a commutative square testing the pullback along ψ. Hence it has a mediator v with u = j · v.

Then x = i · j · v is the required mediator to the pullback along Eψ, and is unique since i · j is mono. □

Proposition 5.2 E ⊂ S is closed under finite limits. Proof In the following, the numbers refer to Propositions in [C].

(a) 1 is overt [8.3(a)];

(b) 1 is discrete [6.11(a)];

(c) if X and Y are overt then so is X × Y [8.3(b)];

(d) if X and Y are discrete then so is X × Y [6.11(c)];

(e) pullbacks at discrete objects exist in S, even in the minimal situation [10.1];

(f) if U → X is mono and X is discrete then so too is U [6.11(e)];

(g) if U ↪ X is an open inclusion and X is overt then so too is U [8.3(c)]. □

Proposition 5.3 Any mono i : X → D from an overt object to a discrete one is an open inclusion. [C, Sections 8,10; Corollary 10.3]. □

Theorem 5.4 If Δ ⊣ U exists then E is an elementary topos. Proof We shall show that UΣ^{Y} is the powerset of Y ∈ obE. Given that E also has finite limits, by [2, Section 2.1] this is sufficient to make E a topos, with subobject classifier Ω ≡ UΣ,

Let i : R ↪ X × Y be any mono in E (a “binary relation” from X to Y). As this goes from an overt object to a discrete one, it is an open inclusion in S, and is therefore classified by some unique ϕ : X × Y → Σ:

[figure: R; 1; X × Y; i; ∩; ϕ; Σ; ⊤]

Using the exponential transpose, ϕ̃: X → Σ^{Y}, this square factorises into the two pullback squares at the back of the diagram

[figure: R; (∈_{Y}^{Σ}); 1]
[figure]
(∈_{Y}^{Ω})  \overline{}1

[figure: X × Y; i; ∩; Y × Σ^{Y}; Σ; ⊤]
[figure: ε]
[figure: Y × UΣ^{Y}; UΣ]

Since U is right adjoint to a full inclusion, it preserves the objects of the subcategory, together with, 1, × and pullbacks. Applying U to the squares at the back of the diagram, those at the front (from R to UΣ) are also pullbacks, where

(∈_{Y}^{Ω}) ≡ U(∈_{Y}^{Σ}) ^{⊂} Y × UΣ^{Y}

is therefore the generic binary relation on Y, as required. □

Theorem 5.5 Conversely, if E is a topos then the inclusion E ⊂ L (or E ⊂ S in the minimal situation) has a right adjoint. Proof The generic subobject ⊤ : 1 → Ω in the topos E is a mono between overt discrete objects in S, which is therefore open and classified by some map ε_{Σ} : Ω ≡ UΣ → Σ by Proposition 5.3.

In order to have Δ ⊣ U, maps Γ → UΣ^{N} (for Γ, N ∈ obE) must correspond to Γ → Σ^{N} and to Γ × N → Σ, and hence to Γ × N → UΣ = Ω and to Γ → Ω^{N}.

So we define UΣ^{N} ≡ Ω^{N} and ε_{Σ^{N}} = ε_{Σ}^{N}, for any N ∈ obE.

Note that Γ × N → Σ classifies an open subspace of the overt discrete space Γ × N, which is the same as a subobject of this object of the topos E, and this is classified by Γ → Ω^{N}.

[figure: Γ; X; i; Σ^{N}; u; v; Σ^{M}]

[figure: ..............]

[figure: UX; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Ui; Ω^{N}; ε_{Σ}^{N}; Uv; Ω^{M}; ε_{Σ}^{M}]

The right adjoint U must also preserve equalisers. But any object X of L is by definition an equaliser of the form in the top row, so define UX as the equaliser on the bottom row.

Now let Γ → X with Γ ∈ E. Then Γ → X → Σ^{N} corresponds to Γ → Ω^{N} and similarly the common composite Γ → Σ^{M} corresponds to Γ → Ω^{M}. As the composites are equal, they factor through the equaliser UX, which is therefore the coreflection of X ∈ obL into E. □

This construction does not extend beyond L because the correspondence between Γ × N → Σ and Γ × N → UΣ = Ω requires N to be overt discrete. The generalisation of this property to arbitrary N ∈ obS is essentially enrichment.

Theorem 5.6 If Δ ⊣ U then S is E-enriched, where

[figure: S(X, Y); U( (ΣΣY)^{X}); U(ηΣΣY)^{X}; U(ΣΣηY)^{X}; U( (Σ^{4}Y)^{X})]

is defined to be an equaliser in E, and S(Γ × X, Y) ≅ S(X, Y)^{Γ} naturally in Γ ∈ obE and X, Y ∈ obS. (This equaliser is based on the same idea as that in Theorem 3.22, but in this case it is calculated in E, so it is also valid in the minimal situation.) Proof Using sobriety of Y (Axiom 3.3), maps Γ × X → Y in S correspond to Γ × X → Σ^{2}Y ⇉ Σ^{4}Y with equal composites, and so to Γ → Σ^{ΣY ×X} ⇉ Σ^{Σ^{3}Y ×X}. Using U and the equaliser, these correspond to maps Γ → S(X, Y) in E. By a similar argument, maps Γ′ → S(Γ × X, Y), Γ′ × Γ → S(X, Y) and Γ′ → S(X, Y)^{Γ} also correspond bijectively, since E, being a topos, is cartesian closed. □

Notation 5.7 We write ΩX ≡ U(Σ^{X}) ≡ S(X, Σ) and, for f : X → Y in S,

Ωf ≡ f^{∗} ≡ U(Σ^{f}) : ΩY → ΩX in E.

Although ΩY is the exponential Ω^{Y} within the topos E, when we try to extend its universal property (i.e. the bijection between maps Γ → ΩY and Γ × Y → Ω) to the larger category S, we find that it only holds when Γ and Y are overt discrete. So the property does not extend at all.

In the type theory that we develop for S in Section 7, we shall therefore not use ΩY directly as an exponential, but always via the adjunction Δ ⊣ U, so application and formation of terms of type ΩY will always involve the new connectives (ε and τ) explicitly.

Remark 5.8 As S is E-enriched, it would be possible to develop S as a fibred category over E. Briefly, for N ∈ obE, we define an N-indexed family of S-objects to be an (arbitrary) map X → N in S. This is re-indexed along u : M → N by forming the pullback, which exists, even in the minimal situation, since N is discrete.

Corresponding to this would be a symbolic calculus of dependent types n : N ⊢ X[n] whose parameters are of overt discrete type.

We avoid doing either of these because both fibred categories and dependent types add significantly to the notational complexity. These technologies have been employed to handle sums, products, limits and colimits of “infinite” families of objects, but we do not intend to consider such things in this paper. We do deal with joins of families of open subobjects of a particular object X, but we can represent them by dependent terms of type ΣX or ΩX (Remark 8.9).

On the other hand, fibred category theory was originally introduced [1, Exposé VI] to model, not set theory or symbolic logic, but the variation of combinatorial structures over geometrical ones. Now that we are in possession of a type theory that is designed to do topology rather than set theory, we can treat many of the issues that arise in that context in a notationally far clearer way; for example [J] applies it to the solution of polynomial equations parametrically in their coefficients. In a symbolic language it is of course very natural for terms to depend on parameters. In Section 10 in particular, their types may in some situations be general (in S) and in others be required to be overt discrete (in E).

Remark 5.9 What we lose by not introducing dependent types is the ability to discuss exponentiable maps. However, a category of sober topological spaces cannot be locally cartesian closed, since the epi ℕ → ϖ is not stable under pullback, where ϖ is the domain of “ascending” natural numbers with ⊤ ≡ ∞. This means that dependent types and their exponentials are not as simple as type theorists and categorical logicians would have us believe — they are axiomatising set theory, whereas we want to study topology. One must first identify particular classes of objects that will be allowed as indices and fibres, or equivalently a pullback-stable class of “display” maps [37, Chapter VIII]. Two obvious choices are general spaces indexed by overt discrete ones (which we have just mentioned) and vice versa (étale maps [20, §V 5]). Plainly an investigation along the lines of [28] needs to be done separately from this one. Where it is appropriate to comment on such matters, we shall do so in the traditional way in which concrete categories have been used for semantics: We treat the display maps in detail first as maps, and then add informal remarks about their interpretation as dependent types.

6 Comparing the monads

Having identified the category “sets”, we can now look for the category of “locales”.

Notation 6.1 We have the following composition of adjunctions over a topos E:

\overline{}S^{op}

S \begin{aligned}Σ^{(−)} &  \\ & ⊣ \begin{matrix}Σ^{(−)} \\  \end{matrix} \end{aligned}

Σ  E \begin{aligned}Δ &  \\ & ⊣ {U \atop } \end{aligned} \underline{}Ω

A covariant adjunction such as Δ ⊣ U has a unit and a counit, but it is convenient to regard the composite adjunction between Σ ≡ Σ^{Δ(−)} and Ω ≡ UΣ^{(−)} as between contravariant functors that relate S (not S^{op}) to E. Then, instead of a unit and counit, we have two units, called

ε̃: X → ΣΩX in S  and  ι : N → ΩΣN in E,

where N is overt discrete. The first is the double exponential transpose of ε : ΩX ≡ UΣ^{X} → Σ^{X}, whilst the second is obtained from η_{N} : N → ΣΣN using the coreflection Δ ⊣ U.

Remark 6.2 In this section we compare L^{op} and S^{op} with the category of algebras for the monad over E. The main task is to investigate the correspondences amongst

(a) morphisms f : Γ → X in S,

(b) Eilenberg–Moore homomorphisms Σ^{X} → Σ^{Γ} for the monad on S and

(c) Eilenberg–Moore homomorphisms ΩX → ΩΓ for the monad on E. In fact, sobriety (Axiom 3.3) already tells us that the first two are the same [A, Theorem 4.10], but only within L do we obtain a bijection between them and (c). Also, instead of working with Eilenberg–Moore homomorphisms, it is more convenient to work with their exponential transposes.

Remark 6.3 A map H : Σ^{X} → Σ^{Γ} is an Eilenberg–Moore homomorphism for the monad on S iff its double exponential transpose P has equal composites

[figure: Γ; P; ΣΣX; ΣΣηX; ηΣΣX; ΣΣΣΣX,]

and in this case P is said to be prime [A, §4]. But by Axiom 3.3, X is the equaliser of this parallel pair. Hence when P is prime it is of the form P = η_{X}(a) for some unique Γ ⊢ a : X, and we write a ≡ focus P [A, §8]. □

Remark 6.4 An Eilenberg–Moore homomorphism ΩX → ΩΓ for the monad on E can also be expressed in this way, using its double exponential transpose Q, which has equal composites along the bottom of this diagram:

[figure: X; ηX; ΣΣX; ΣΣηX; ηΣΣX; Σ^{4}X]

[figure: Γ; Q; ΣΩX; ΣεΣX; ΣΩε̃X; ε̃ΣΩX; ΣΩΣΩX]

We shall say that P and Q are Σ-prime and Ω-prime respectively. Since these two notions correspond to the two equalisers, we have to show that the latter are are isomorphic. However, this can only happen when X ∈ obL, since the lower equaliser is itself of the form Σ^{N} ⇉ Σ^{M} with N, M ∈ obE.

We start by proving the property for X ≡ Σ^{N}.

Lemma 6.5 In the following diagram, the two triangles (!) on the left commute, and both rows are split equalisers.

[figure: ΣN; ηΣN; \underline{ΣηN}; Σ^{3}N; Σ^{2}ηΣN; \underline{Σ^{3}ηN}; ηΣ^{3}N; Σ^{5}N]

ΣN

‖

[figure: ε̃ΣN] [figure: \underline{ΣιN}]
ΣΩΣN

\begin{aligned}ΣεΣΣN \\ & \end{aligned}

ΣΩε̃ΣN ΣΩΣιN ε̃ΣΩΣN

ΣΩΣΩΣN

Proof Each row is the standard resolution of the free algebra on N with respect to the monad in question. □

When we extend this result to subspaces i : X ↣ Σ^{N} in Proposition 6.8, we shall need ΣΩi to be mono. This is very easy in the minimal situation (but beware that we use both i and ι).

Lemma 6.6 If i : X ↣ Y is Σ-split mono (by I) then ΣΩi is split mono (by ΣUI). □

In the complete situation, on the other hand, we need injectivity of Σ.

Lemma 6.7 If i : X ↣ Y is regular mono in L then Ωi : ΩY ↠ ΩX is split epi in E and ΣΩi is split mono in L. Proof For any Γ ∈ obE ⊂ L, the map Γ × i : Γ × X ↣ Γ × Y is also a regular mono in L. Let ψ : Γ × X → Σ be the transpose of εΣX : Γ ≡ ΩX → ΣX. Then injectivity and the coreflection provide the splitting of Ωi, as illustrated by the dotted arrows.

Γ × Y  ΩY \overline{εΩY} ΣY
[figure: ..............; ϕ; ..............; ..................................]
Σ  Γ
[figure: ψ; id]
[figure: Γ × X; Γ × i; ΩX; Ωi; εΩX; ΣX; Σi]

Finally, any contravariant functor takes split epis to split monos. □

Proposition 6.8 Any object X ∈ obL (or X ∈ obS in the minimal situation) is the equaliser of both parallel pairs in the top face of the following diagram.

[figure: X; η; ΣΣX; ΣΣΣΣX]
[figure: ............; a; ΣεΣX]
[figure: Γ; Q; ΣΩX; ΣΩΣΩX]

[figure: ΣN; i; ηN; Σ^{3}N; Σ^{5}N]
[figure]
[figure: ΣN; . . . . . . . . . . . . . . . . . . . . . . . . .; ϵ̃N; ΣΩΣN; ΣΩi; ΣΩΣΩΣN]

[figure: ΣM; ηM; Σ^{3}M; Σ^{5}M]
[figure]
[figure: ΣM; ϵ̃M; ΣΩΣM; ΣΩΣΩΣM]

Proof As X ∈ obL, let it be the equaliser of ΣN ⇉ ΣM (down the left side). By sobriety, X is also the equaliser of Σ^{2}X ⇉ Σ^{4}X (along the top), although we could deduce that by an argument similar to the following one.

To test the other equaliser, let Q be an Ω-prime, i.e. the composites along that row are equal. The composites Γ → ΣΩΣΩΣN are also equal, by naturality of ΣΩε̃ and ε̃ΣΩ with respect to

i : X → ΣN. But ΣN is the equaliser of the middle front row, so we have Γ → ΣN. As this equaliser is split (Lemma 6.5), this is actually given by composition: ΣιN · ΣΩi · Q.

Similarly, we have a unique map Γ → ΣM, and therefore a map a : Γ → X, since X is the equaliser of ΣN ⇉ ΣM.

In the top left cube, we now have equal composites from Γ to ΣΩΣN. Since ΣΩX ↣ ΣΩΣN is (split) mono by the preceding Lemmas, we deduce that the top square commutes, i.e. Q = ΣεΣX(ηa). The mediator a is unique because X ↣ ΣΩΣN is mono. □

We shall prove the same result again symbolically in Proposition 7.11.

Corollary 6.9 The minimal and complete requirements can be expressed canonically:

(a) if X ↣ Σ^{N} is Σ-split then so is ε̃_{ΣX} : X ↣ Σ^{N′};

(b) if X ↣ Σ^{N} ⇉ Σ^{M} is an equaliser then so is X ↣ Σ^{N′} ⇉ Σ^{M′} where N′ ≡ ΩX and M′ ≡ ΩΣΩX. □

Theorem 6.10 L^{op} (or S^{op} in the minimal situation) is a full subcategory of the Eilenberg–Moore category for the monad ΩΣ(−) over E. Proof We have shown that Σ- and Ω-primes are in bijective correspondence, and therefore so too are the maps and homomorphisms in Remark 6.2. □

Corollary 6.11 In order to identify the category L (or S in the minimal situation), it suffices to characterise the algebras ΩX and their homomorphisms f^{∗} ≡ Ωf ≡ UΣ^{f} for the monad on E. (Remember that S can still be a topos or CCD^{op} until we assert the Scott principle in Section 10.)

□

Corollary 6.12 Let f : X → Y in L. Then

(a) f is regular mono in L iff Ωf is split epi in E, and

(b) f is epi in L iff Ωf is split mono in E, but (c) for f ∈ S we only have f epi implies Ωf split mono. □

In the following sections we develop a symbolic calculus to exploit the “underlying set” axiom, and then recover the traditional technology of inverse and direct images for (toposes, CCD^{op} and) locales. We conclude the story of the identification of L with LKLoc, Sob or Loc in Sections 11 and 12.

Remark 6.13 Beware, however, that the results that rely on the functor Ω only really apply to the subcategory L. Although the hypotheses of most of the lemmas allow arbitrary objects and morphisms of S, their results involve only E or L. In particular, when Theorem 12.7 characterises morphisms in terms of the traditional definition of continuity, it will require the source and target to be spatial and localic respectively.

The other results appear to be more general because they actually tell us about the reflection of S in L. This is obtained by forming, for any X ∈ obS, the equaliser that we used to characterise X ∈ obL. We discuss this in Section 13.

7 A type theory for underlying sets

In this section we introduce a (fragment of) type theory in which the “underlying set” axiom may be manipulated. In particular, we use it to develop some of the main structure of locale theory. This shows how we can reason in general topology with a calculus whose terms denote points, but which is nevertheless equivalent to the intuitionistic locale theory that has hitherto required the use of infinitary lattice theory.

First we recall the rules for equality and the quantifiers, applicable to discrete, overt and compact objects.

Definition 7.1 A type N is a discrete object if there is a binary predicate n, m : N ⊢ n(=_{N})m : Σ such that

for terms Γ ⊢ n, m : N,  Γ ⊢ (n =_{N} m) = ⊤ : Σ ; = ; Γ ⊢ n = m : N

where (=) below the line denotes provable equality of terms of type N, whilst (=_{N}) above the line is the new structure.

Definition 7.2 A type N is an overt object if it comes equipped with ϕ : Σ^{N} ⊢ ∃_{N}ϕ : Σ such

that Γ, x : N ⊢ ϕx ≤ σ : Σ

= Γ ⊢ ∃x:N . ϕx ≤ σ : Σ

where we write ∃x:N . ϕx for ∃_{N}(λx:N . ϕx). The Frobenius law,

σ ∧ ∃x. ϕx = ∃x. σ ∧ ϕx,

follows automatically from the Euclidean principle (Theorem 3.8), whilst the Beck–Chevalley condition follows from the λ-calculus formulation.

Definition 7.3 A type K is a compact object if it comes equipped with ϕ : Σ^{N} ⊢ ∀_{K}ϕ : Σ such

that Γ, x : K ⊢ σ ≤ ϕx : Σ

= Γ ⊢ σ ≤ ∀x:K. ϕx : Σ

Again the Beck–Chevalley condition is automatic.

We can now formulate the rules for the “underlying set” (Δ ⊣ U).

Notation 7.4 For any type (space, object of S) X, we have (a) another type, the underlying set, UX;

(b) as this is discrete, an equality, (=_{UX}) : UX × UX → Σ, satisfying the rules in Definition 7.1;

(c) as it is overt, an existential quantifier, (∃_{UX}) : Σ^{UX} → Σ, satisfying the rules in Definition 7.2;

(d) for any overt discrete context Γ (so Γ ∈ obE) the transformation (U-introduction)

{Γ ⊢ a : X \atop Γ ⊢ τ. a : UX}

where the τ is accompanied by a dot because, like λ-abstraction, it is not an algebraic symbol but an operation on terms-in-context (whilst τ doesn’t change the context Γ, it does depend on its belonging to E);

(e) the counit (U-elimination), which is a function-symbol x : UX ⊢ εx : X;

(f) satisfying the β- and η-rules

Γ ⊢ ε(τ. a) = a : X  and  x : UX ⊢ x = (τ. εx) : UX.

In short, τ. may be applied to any term so long as all of its free variables are of overt discrete type. In other words, it allows variation over a combinatorial structure but not a geometrical one, cf. Remark 5.8.

This notational trick with ε and τ. is applicable to any coreflective subcategory, as [37] explains; in particular Section 9.5 uses it for comprehension. Also, in the language of Remark 7.2.4 there, since the new operator U is a right adjoint, naturality of τ. on the old (left) side gives substitution invariance:

Proposition 7.5 The operator τ. commutes with substitution:

{u : Δ → Γ in E  Γ ⊢ a : X \atop Δ ⊢ u^{∗}(τ. a) = τ. (u^{∗}a) : UX}  [figure: Δ; u; Γ; ..........; τ. a; UX; ε; X; a]

Proof

Δ ⊢ u^{∗}(τ. a) = τ. ε(u^{∗}τ. a)  U-η
= τ. u^{∗}(ετ. a)  ε is a function-symbol
= τ. u^{∗}a  U-β □

The new type theory helps to explain what was going on with the two monads in the previous section.

Example 7.6 The units of the contravariant adjunction between Σ and Ω in Notation 6.1 are

ι_{N} : N → ΩΣ^{N} by n : N ⊢ τ. λϕ:Σ^{N} . ϕn
ε̃_{X} : X → Σ^{ΩX} by x : X ⊢ λϕ:ΩX. εϕx

Then Γ ⊢ P : Σ^{Σ^{X}} and Γ ⊢ Q : ΣΩX are Σ- and Ω-prime respectively according to Remarks 6.3f iff

Γ, F : ΣΣΣX ⊢ FP = P (λx:X. F(λϕ:ΣX. ϕx)) : Σ
Γ, G : ΩΣΩX ⊢ εGQ = Q(τ. λx:X. (εG)(λψ:ΩX. εψx)) : Σ

Note that the sub-term to which Q is applied is well formed because its only free variable is G, whose type is overt discrete by hypothesis, irrespectively of whether Γ is.

Exercise 7.7 Use the type theory to prove (a) Lemma 6.5, (b) this characterisation of Ω-primes, and (c) if P is Σ-prime then Q ≡ λψ:ΩX. P (εψ) is Ω-prime. □

We can also easily apply the new notation to Definition 3.16:

Lemma 7.8 X ∈ obS has enough points (viz. to distinguish ϕ from θ as open subsets of X) iff the following rule is valid for Γ ⊢ ϕ, θ : Σ^{X}:

{Γ, p : UX ⊢ θ(εp) ≤ ϕ(εp) : Σ \atop Γ, x : X ⊢ θx ≤ ϕx : Σ}

There are several equivalent ways of saying this:

(a) there is some p : N ↠ X with N overt discrete and p epi, i.e. Σ^{p} is mono;

(b) ε : UX ↠ X is epi and Σ^{ε} is mono;

(c) U : S → E is faithful for maps with source X, i.e. U_{X,Y} : S(X, Y) ↣ E(UX, UY) for all Y ∈ obS;

(d) ε^{∗} ≡ Ωε : ΩX → ΩUX is mono;

(e) ε_{∗} · ε^{∗} = id_{ΩUX}, where the last two only imply the others only when X ∈ obL, by Corollary 6.12(b). □

The concept of overtness was not recognised in traditional topology because there every space has enough points:

Proposition 7.9 Overt discrete ⇒ enough points ⇒ overt. Proof [a] ε = id [b] ∃x:X. ϕx ≡ ∃p:UX. ϕ(εp) by [C, Lemma 7.2]. □

Before we can re-prove Proposition 6.8 symbolically, we have to state injectivity (cf. Lemma 6.7).

Lemma 7.10 Let X ^{i} Y ⇉ Z be an equaliser in L, and Δ any context in L. Then

(a) for any Δ, x : X ⊢ ϕx : Σ there is some Δ, y : Y ⊢ Φy : Σ such that Δ, x : X ⊢ ϕx = Φ(ix) : Σ;

(b) in particular, putting Δ ≡ [ψ : ΩX] and ϕx ≡ εψx, the map Ωi : ΩY ↠ ΩX is split epi. □

Proposition 7.11 Let X ∈ obL and Γ ⊢ Q : ΣΩX be Ω-prime. Then there exists Γ ⊢ a : X such that Γ ⊢ Q = λψ. εψa. Proof In the course of the earlier proof, we found a map Γ → Σ^{N}, namely

Γ ⊢ λn. Q(τ. λx. ixn) : Σ^{N},

and this has equal composites with Σ^{N} ⇉ Σ^{M}. So, seriously abusing the notation in both [A, §8] and [B, §8], we define

Γ ⊢ focus Q ≡ a ≡ admit (λn. Q(τ. λx. ixn)) : X.

Now let Δ be the context [ψ : ΩX] ∈ E, so Δ, x : X ⊢ εψx : Σ is an open subspace of Δ × X in L.

a : X
[figure: ψ]

Σ

.............. Ψ
λn. Q(τ. λx. ixn) : Σ^{N} [figure: i]

By Lemma 7.10, there is some Δ ⊢ Ψ : ΩΣN with Δ, x : X ⊢ εψx = εΨ(ix), so consider

Δ, x : X ⊢ G ≡ τ. λQ′. εΨ(λn. Q′(τ. λx. ixn)).

Then εG(λψ′. εψ′x) = εΨ(λn. (λψ′. εψ′x)(τ. λx. ixn)) = εΨ(λn. ixn) = εψx,

and the right hand side of the primality equation for Q with respect to G is Q(τ. λx. εψx) ≡ Qψ. Hence

Γ, ψ : ΩX ⊢ Qψ = εGQ = εΨ(λn. Q(τ. λx. ixn)) = εΨ(ia) = εψa

and so Q = λψ. εψa. It is unique since X ↣ ΣΩX as X ∈ obL. □

Corollary 7.12 Whereas the β- and η-rules for a Σ-prime Γ ⊢ P : ΣΣX [A, §8] were

Γ, ϕ : ΣX ⊢ ϕ(focus P) = P ϕ and x : X ⊢ focus(λϕ:Σ^{X} . ϕx) = x,

those for an Ω-prime Γ ⊢ Q : ΣΩX are

Γ, ψ : ΩX ⊢ εψ(focus Q) = Qψ and x : X ⊢ focus(λψ:ΩX. εψx) = x,

or just ϕ(admit Q) = Q(τ. ϕ), so long as the free variables of ϕ are all of overt discrete type. □

8 Lattice structure on Σ and Ω

Beware, nevertheless, that both (Σ^{X}, ⊤, ⊥, ∧, ∨) and (ΩX, ⊤, ⊥, ⋏, ⋎) are internal lattices in S in the usual categorical sense.

Remark 8.1 Indeed, the point at which the dichotomy is most apparent is where we consider the order relations on Σ^{X} and ΩX. In particular

(a) all maps Σ^{Y} → Σ^{X} preserve the order ≤ that is defined by the lattice structure (that is, in the topological and order-theoretic cases, but not Set, where Σ = Ω), whereas

(b) since ΩY and ΩX are merely “sets” (overt discrete objects), maps ΩY → ΩX may preserve, reverse or ignore the order ≼ as they please.

In the second case, the order on ΩX is an open subobject

(≼) ^{⊂} ΩX × ΩX,

which is classified by a map

(≼) : ΩX × ΩX Σ or ψ_{1}, ψ_{2} : ΩX ⊢ (ψ_{1} ≼ ψ_{2}) : Σ.

The order ≤ on Σ^{X} is also a subspace of Σ^{X} × Σ^{X}, in fact a retract of it, but it is neither open nor closed, and therefore has no classifier. Indeed, for ϕ, ψ : Σ^{X}, the statement (ϕ ≤ ψ) is contravariant in ϕ, so such a classifier would violate the monotonicity property, cf. [G, Remark 2.7]. In the application to recursion theory, this would solve the Halting Problem.

Notation 8.2 Established mathematical usage and the availability of suitable symbols make it impossible to be consistent in the notational distinction between imposed and intrinsic structure. We shall employ the correspondence,

intrinsic Σ S ⊤ ⊥ ∧ ∨ ≤ ∃ ∀ ⊣
imposed Ω E ⊤ ⊥ ⋏ ⋎ ≼ ⋁ ⋀ ⊣

so some of the symbols will have to be dis-ambiguated by context. Certain others, notably =, ≠, ⇒, ¬ and ↓, will only occur as imposed structure.

Later in this section we develop the basic results concerning the relationship between the intrinsic structure on Σ^{X} and the imposed structure on ΩX. But first we re-prove Proposition 3.17, that Σ is a distributive lattice and not merely a ∧-semilattice as Theorem 3.8 said. This gives us some practice in using the type-theoretic notation. However, it also uses the “comprehension” calculus in [B, §8]. If you do not have [B] to hand, you should skip the next two lemmas, and take disjunction in Σ as additional structure.

Lemma 8.3 Σ has a least element, and 0 is overt.

Proof We define 0 ^{i} Σ by E ≡ λF:Σ^{Σ}. λσ:Σ. σ. Then by {}E0 of [B, §8],

x : U0, F : Σ^{Σ} ⊢ F (i(εx)) = (EF)(i(εx)) ≡ i(εx).

Applying this with θ : Σ ⊢ F ≡ λy. θ and F ≡ λy. ⊤,

x : U0, θ : Σ ⊢ ⊤ = (λy. ⊤)(i(εx)) = i(εx) = (λy. θ)(i(εx)) = θ ≤ θ

so, by Definition 7.2, θ : Σ ⊢ (∃x:U0. ⊤) ≤ θ. Hence ⊥ ≡ (∃x:U0. ⊤) is the least element of Σ, and ∃_{0} ≡ ⊥ : Σ^{0} ≡ 1 → Σ is the quantifier that makes 0 overt. □

Lemma 8.4 Σ has binary joins, and 2 is overt.

Proof We define 2 ^{i} Σ^{Σ×Σ} by E ≡ λF:ΣΣ(Σ × Σ). λF:Σ^{Σ×Σ}. F (Fπ_{0}, Fπ_{1}) as in [B, Lemma 11.5]. Then for x : U2, P ≡ i(εx) : Σ^{Σ×Σ} satisfies

x : U2, F : ΣΣ(Σ × Σ) ⊢ P (Fπ_{0}, Fπ_{1}) = FP.

In this, consider σ ≤ θ ≥ τ ⊢ F ≡ λF. F (σ, τ) ∧ θ, so

i(εx)(σ, τ) ≡ P (σ, τ) ≡ P (σ ∧ θ, τ ∧ θ) ≡ P (Fπ_{0}, Fπ_{1}) = FP ≡ P (σ, τ) ∧ θ ≤ θ,

so, by Definition 7.2, σ ≤ θ ≥ τ ⊢ (∃x:U2. i(εx)(σ, τ)) ≤ θ.

On the other hand, 0, 1 : U2 are (τ. admit π_{0}) and (τ. admit π_{1}). Then

σ = π_{0}(σ, τ) = i(ε0)(σ, τ) ≤ ∃x:U2. i(εx)(σ, τ).

Hence σ ∨ τ ≡ (∃x:U2. i(εx)(σ, τ)) is the join, and ∃_{2} ≡ ∨ : Σ^{2} ≡ Σ × Σ → Σ is the quantifier that makes 2 overt. □

Proposition 8.5 Σ is a distributive lattice, and all finitely enumerable objects are overt discrete. Proof For α ∧ (β ∨ γ) = (α ∧ β) ∨ (α ∧ γ), consider F (σ) ≡ (σ ∧ β) ∨ (σ ∧ γ) in the Euclidean principle (Theorem 3.8). □

Corresponding to this intrinsic structure on the “spaces” Σ and Σ^{X}, we have imposed structure on their “underlying sets” Ω and ΩX.

Notation 8.6 Since U is a right adjoint, it preserves finite limits and equations, so in particular it takes the lattice structure (⊤, ⊥, ∧, ∨) on Σ^{X} to another such structure (⊤, ⊥, ⋏, ⋎) on ΩX ≡ UΣ^{X}. Symbolically,

(a) ⊤ ≡ U⊤ ≡ τ. λx. ⊤ : ΩX, so ε⊤ = ⊤ : Σ^{X};

(b) ⊥ ≡ U⊥ ≡ τ. λx. ⊥ : ΩX, so ε⊥ = ⊥ : Σ^{X};

(c) ⋏ ≡ U∧ : ΩX × ΩX → ΩX by ϕ ⋏ ψ ≡ τ. λx. (εϕ)x ∧ (εψ)x, so

[figure: ΩX × ΩX; .; .; .; .; .; .; .; .; .; ⋏; ΩX; Σ^{X} × Σ^{X}; ε × ε; ∧; Σ^{X}; ε]

(d) ⋎ ≡ U∨ : ΩX × ΩX → ΩX by ϕ ⋎ ψ ≡ τ. λx. (εϕ)x ∨ (εψ)x; (e) ≼ by (ϕ ≼ ψ) ≡ ((ϕ ⋏ ψ) =_{ΩX} ϕ) : Σ, where we recall that ΩX, being discrete, is equipped

with an equality test (=_{ΩX}) : ΩX × ΩX → Σ. We can also define (ϕ ⇒ ψ) on Ω as τ. (ϕ ≼ ψ), and ¬ϕ ≡ τ. (ϕ =_{Ω} ⊥), but Proposition 9.2 does this more generally for ΩX.

The imposed order ≼ on ΩX agrees with the intrinsic pointwise order on Σ^{X}, in the following sense.

Proposition 8.7 Let Γ ⊢ ϕ, θ : ΩX, where the context Γ ∈ obE is overt discrete. Then

Γ ⊢ (ϕ ≼_{ΩX} θ) = ⊤ : Σ = Γ, x : X ⊢ (εϕ)x ≤ (εθ)x : Σ

Proof We may deduce in both directions,

Γ  ⊢ (ϕ ≼_{ΩX} θ) = ⊤ : Σ
Γ  ⊢ ((ϕ ⋏_{ΩX} θ) =_{ΩX} ϕ) = ⊤ : Σ  def ≼_{ΩX}
Γ  ⊢ ϕ ⋏_{ΩX} θ = ϕ : ΩX  def =_{ΩX}
Γ  ⊢ ε(ϕ ⋏_{ΩX} θ) = εϕ : Σ^{X}  Δ ⊣ U
Γ  ⊢ εϕ ∧_{Σ^{X}} εθ = εϕ : Σ^{X}  def ⋏_{ΩX}
Γ, x : X ⊢ εϕx ∧_{Σ} εθx = εϕx : Σ  def ∧_{Σ^{X}}
Γ, x : X ⊢ εϕx ≤_{Σ} εθx : Σ  def ≤_{Σ}

where the deduction upwards from the line marked “Δ ⊣ U” relies on the hypothesis that the context Γ be overt discrete. □

Remark 8.8 The lattice Σ^{X} also has intrinsic M-indexed joins, for any overt object M. These are given by ∃m:M . ϕ^{m}. The corresponding imposed structure on ΩX is

⋁ ≡ U∃_{M} : (ΩX)^{M} → ΩX so ⋁_{m:M} ψ^{m} ≡ τ. λx. ∃m:M . εψ^{m}x.

Remark 8.9 However, when we use this, we shall need M to be a dependent type (cf. Remark 5.9), given, in traditional comprehension notation (not that of [B]), by

M ≡ {n : N | α_{n}} ⊂ N,

where α_{n} selects the subset of indices n for which ϕ^{n} : Σ^{X} or ψ^{n} : ΩX is to contribute to the join. This subset will always be open, and α_{n} : Σ. We use the sub- and super-script notation here (and in [G]) to indicate that ϕ^{n} typically varies covariantly and α_{n} contravariantly with respect to an imposed order on N.

Remark 8.10 This means that, when using the existential quantifier, we can avoid introducing dependent types by defining

∃n:{n : N | α_{n}}. ϕ^{n} as ∃n:N . α_{n} ∧ ϕ^{n}

and, for ΩX, ⋁_{n∈M} ψ^{n} ≡ τ. ∃n:N . α_{n} ∧ εψ^{n}.

Then, when Propositions 10.9, 10.10 and 11.9 say that Q : ΣΩX preserves this join, they mean that

Q( ⋁_{n∈M} ψ^{n}) ≡ Q(∃n:{n : N | α_{n}}. ψ^{n}) ≡ Q(τ. ∃n:N . α_{n} ∧ εψ^{n})

is equal to ⋁_{n∈M} Qψ^{m} ≡ ∃n:{n : N | α_{n}}. Qψ^{n} ≡ ∃n:N . α_{n} ∧ Qψ^{n}.

Unfortunately, we cannot use the same trick to eliminate dependent types from the universal quantifier, which is needed for the study of CCD^{op}.

Whereas ΩX is simply a set (overt discrete object) with an imposed lattice structure, the intrinsic structure on Σ also enjoys a correspondence with inclusions of open subspaces (Definition 3.7).

This in turn gives rise to a calculus of predicates [C, §8]. Whilst this is logically rather weak (Σ_{1}^{0}), it is important to the structure that we develop in the next section. For that we need a couple of reasoning principles about Σ.

Lemma 8.11 Let Γ ⊢ α, β, γ : Σ. Then

Γ, α = ⊤ ⊢ β ≤ γ : Σ = Γ ⊢ α ∧ β ≤ γ : Σ

Proof By Theorem 3.8, we may work in terms of the open subobjects of Γ that these terms classify. On the top line, β and γ are interpreted as

[α] ∩ [β] ⊂ [α] ∩ [γ] ^{⊂} [α] ^{⊂} Γ

so Γ ⊢ α ∧ β ≤ α ∧ γ : Σ, which is just Γ ⊢ α ∧ β ≤ γ : Σ, and conversely. □

Lemma 8.12 If there is a proof of

{Γ ⊢ α = ⊤ : Σ \atop Γ ⊢ β = ⊤ : Σ}

then Γ ⊢ α ≤ β : Σ. Proof Add α = ⊤ to the context in each line of the proof, and deduce α ≤ β. □

9 Direct and inverse images

The constructions in this section use joins over the dependent subtypes of ΩX classified by

α_{θ} = (ϕ ⋏ θ ≼ ψ), (F θ), and (f^{∗}θ ≼ ϕ).

These are essentially applications of the adjoint function theorem for the imposed complete lattices ΩX and ΩY. Unfortunately, the cost of the trick that we used in Remark 8.10 to eliminate dependent subtypes is that the proofs of the adjunctions are more difficult.

Notation 9.1 Let X ∈ obS. Define

(a) the Heyting implication, (⇒) : ΩX × ΩX → ΩX by

ϕ, ψ : UΣ^{X} ⊢ (ϕ ⇒ ψ) ≡ τ. λx. ∃θ:UΣ^{X} . εθx ∧ (ϕ ⋏ θ ≼ ψ) : UΣ^{X},

so ε(ϕ ⇒ ψ)x = ∃θ. εθx ∧ (ϕ ⋏ θ ≼ ψ),

(b) the Heyting negation, (¬) : ΩX → ΩX by ¬ϕ ≡ (ϕ ⇒ ⊥),

(c) the lower sets, ↓ : ΩX → ΩΩX by

ϕ : UΣ^{X} ⊢ ↓ ϕ ≡ τ. λψ:UΣ^{X} . (ψ ≼ ϕ) : UΣ^{UΣ^{X}} ,

(d) the join, ⋁ : Σ^{ΩX} → Σ^{X} by

F : Σ^{UΣ^{X}} ⊢ ⋁ F ≡ λx:X. ∃θ:UΣ^{X} . F θ ∧ (εθ)x : Σ^{X}.

As we typically form the join of a lower subset, F cannot be monotone, or act on Σ^{X}: it is usually contravariant, taking the imposed order ≼ on ΩX to the intrinsic order ≥ in the opposite sense on Σ.

Proposition 9.2 (−) ⋏ ϕ ⊣ ϕ ⇒ (−) in the sense that

ϕ, ψ, θ : ΩX ⊢ ((θ ⋏ ϕ) ≼ ψ) = (θ ≼ (ϕ ⇒ ψ)) : Σ

Proof ((θ ⋏ ϕ) ≼ ψ) ≤ (θ ≼ (ϕ ⇒ ψ)) because (using Lemma 8.12)

Γ  ⊢ (θ ⋏ ϕ ≼ ψ) = ⊤
Γ, x, εθx = ⊤ ⊢ εθx ∧ (θ ⋏ ϕ ≼ ψ) = ⊤  weakening
Γ, x, εθx = ⊤ ⊢ ∃ξ. εξx ∧ (ξ ⋏ ϕ ≼ ψ) = ⊤  Definition 7.2
Γ, x  ⊢ εθx ≤ ∃ξ. εξx ∧ (ξ ⋏ ϕ ≼ ψ)  Lemma 8.11 (*)
Γ, x  ⊢ εθx ≤ ε(ϕ ⇒ ψ)x  def ⇒
Γ  ⊢ (θ ≼ (ϕ ⇒ ψ)) = ⊤  Proposition 8.7

where the last three deductions are reversible, Γ ∈ E, x : X and θ, ϕ, ψ, ξ : ΩX ≡ UΣ^{X}. For the converse we first need

Γ, ξ, x, (ϕ ⋏ ξ ≼ ψ) = ⊤
⊢ εϕx ∧ εξx ≤ εψx  Notation 8.6, Proposition 8.7
Γ, ξ, x, εϕx = ⊤ ⊢ εξx ∧ (ϕ ⋏ ξ ≼ ψ) ≤ εψx  Lemma 8.11 twice
Γ, x, εϕx = ⊤  ⊢ (∃ξ. εξx ∧ (ξ ⋏ ϕ ≼ ψ)) ≤ εψx  Definition 7.2

Combining this with (*), which is equivalent to (θ ≼ (ϕ ⇒ ψ)) = ⊤, we deduce

Γ, x, εϕx = ⊤ ⊢ εθx = ⊤ ≤ ∃ξ. εξx ∧ (ξ ⋏ ϕ ≼ ψ) ≤ εψx
Γ, x  ⊢ εϕx ∧ εθx ≤ εψx  Lemma 8.11
Γ  ⊢ (ϕ ⋏ θ ≼ ψ) = ⊤  Notation 8.6, Proposition 8.7 □

Proposition 9.3 U ⋁ ⊣ ↓ in the sense that

ϕ : ΩX, F : ΩΩX ⊢ (τ. ⋁ εF ≼ ϕ) = (F ≼ ↓ ϕ) : Σ

Proof We may deduce in either direction as follows:

Γ  ⊢ (τ. ⋁ εF ≼ ϕ) = ⊤ : Σ
Γ, x  ⊢ ∃θ. (εF)θ ∧ (εθ)x ≤ (εϕ)x : Σ  Proposition 8.7
Γ, θ, x  ⊢ (εF)θ ∧ (εθ)x ≤ (εϕ)x : Σ  Definition 7.2
Γ, θ, (εF θ) = ⊤, x ⊢ (εθ)x ≤ (εϕ)x : Σ  Lemma 8.11
Γ, θ, (εF θ) = ⊤  ⊢ (θ ≼ ϕ) = ⊤ : Σ  Proposition 8.7
Γ, θ  ⊢ (εF θ) ≤ (θ ≼ ϕ) : Σ  Lemma 8.11
Γ  ⊢ (F ≼ ↓ ϕ) = ⊤ : Σ  Proposition 8.7

where ϕ, θ : ΩX ≡ UΣ^{X} and F : ΩΩX. The second and last lines use the definitions of ⋁ and ↓. □

Theorem 9.4 For each object X ∈ obS, ΩX carries the imposed structure of a complete Heyting algebra internally to the topos E. □

Notation 9.5 Let f : X → Y in S. Define

(a) the inverse image f^{∗} ≡ Ωf ≡ UΣ^{f} : ΩY → ΩX by

ψ : UΣ^{Y} ⊢ f^{∗}ψ ≡ τ. λx:X. (εψ)(fx) : UΣ^{X}

(b) and the direct image f_{∗} : ΩX → ΩY by

ϕ : UΣ^{X} ⊢ f_{∗}ϕ ≡ τ. λy:Y . ∃θ:UΣ^{Y} . (εθ)y ∧ (f^{∗}θ ≼ ϕ) : UΣ^{Y} .

Proposition 9.6 f^{∗} ⊣ f_{∗} in the sense of ≼. Proof To show (f^{∗}ψ ≼ ϕ) ≤ (ψ ≼ f_{∗}ϕ),

Γ  ⊢ (f^{∗}ψ ≼ ϕ) = ⊤ : Σ
Γ, y, (εψy) = ⊤ ⊢ (εψy) ∧ (f^{∗}ψ ≼ ϕ) = ⊤ : Σ  weakening
Γ, y, (εψy) = ⊤ ⊢ ∃θ. (εθy) ∧ (f^{∗}θ ≼ ϕ) = ⊤ : Σ  Definition 7.2
Γ, y  ⊢ (εψy) ≤ ∃θ. (εθy) ∧ (f^{∗}θ ≼ ϕ) : Σ  Lemma 8.11
Γ  ⊢ (ψ ≼ τ. λy. ∃θ:UΣ^{Y} . (εθy) ∧ (f^{∗}θ ≼ ϕ)) = ⊤  Prop. 8.7
Γ  ⊢ (ψ ≼ f_{∗}ϕ) = ⊤  def f_{∗}

where ϕ : UΣ^{X} and ψ, θ : UΣ^{Y}. Conversely, ψ ≼ f_{∗}ϕ means

Γ, y ⊢ εψy ≤ ε(f_{∗}ϕ)y : Σ  Proposition 8.7
Γ, x ⊢ (εψ)(fx) ≤ ε(f_{∗}ϕ)(fx) : Σ,  substitution

where x : X and y : Y, so we need

Γ, θ, (f^{∗}θ ≼ ϕ) = ⊤, x
⊢ ε(f^{∗}θ)x ≡ (εθ)(fx) ≤ εϕx : Σ  Proposition 8.7
Γ, θ, x ⊢ (f^{∗}θ ≼ ϕ) ∧ (εθ)(fx) ≤ εϕx : Σ  Lemma 8.11
Γ, x  ⊢ ε(f_{∗}ϕ)(fx) ≡ ∃θ. (f^{∗}θ ≼ ϕ) ∧ (εθ)(fx) ≤ εϕx  Def 7.2

Hence

Γ, x ⊢ (εψ)(fx) ≤ ε(f_{∗}ϕ)(fx) ≤ εϕx : Σ
Γ, x ⊢ (εψ)(fx) ≤ εϕx : Σ
Γ  ⊢ (f^{∗}ψ ≡ τ. λx. (εψ)(fx) ≼ ϕ) = ⊤ : Σ  Proposition 8.7 □

10 The topological case

Recall from Theorem 6.10 that we just have to identify the monad ΩΣ(−) on E in order to characterise the category L, so in this section we invoke the Scott principle to specialise to the topological case. (Actually, if we had the necessary dependent types, everything could still apply to ℵ-Loc, ℵ-LKLoc and CCD^{op}.)

We go on to give the traditional characterisations of primes, morphisms and bases. In this a theme emerges: where we use Σ-primes and general parameters in the minimal situation (for locally compact locales), we find Ω-primes and overt discrete parameters for L (sober spaces and locales). That is, the generalisation comes at a certain price.

The next section treats the minimal situation, i.e. those results that only apply to locally compact locales. The remainder of the paper after that considers the complete and exact situations, i.e. general locales and more complicated objects.

Frame homomorphisms (need only) preserve finite meets and arbitrary joins, but, to say this, we have to employ a more formal definition of finiteness than the fact that it is generated from 0 and 2.

Definition 10.1 For N ∈ obE, KN ∈ obE is the free semilattice on N in E.

This may be constructed in any elementary topos (in fact, without even the need for a natural numbers object) as the sub-⋎-semilattice of ΩN generated by the singletons [27, Appendix 2] [17, Theorem 9.16] [37, Proposition 6.6.11]. The semilattice structure, for which we write ⋎ and ≼, is imposed, not intrinsic.

Proposition 10.2 KN is overt discrete and is the free (imposed) semilattice on N in S. Proof It was defined as an open subobject of ΩN, so it is overt discrete.

If (S, 0, +) is a semilattice in S (imposed or intrinsic) then (US, U0, U+) is an imposed semilattice in E and ε : US → S is a semilattice homomorphism (cf. Notation 8.6).

Also, any f : N → S factors as ετ. f : N → US → S, which extends to a semilattice homomorphism KN → US → S. It is unique because if g : KN → S is a semilattice homomorphism then so is τ. g : KN → US, and this must agree with the extension of τ. f. □

The proof could have allowed f to have overt discrete parameters. However, the important cases are the following, of which powers exist even in the minimal situation, so in practice arbitrary parameters are allowed, via λ-abstraction.

Notation 10.3 For ℓ : KN, the expressions

λn. n ∈ ℓ : Σ^{N}, ξ : Σ^{N} ⊢ ∃n ∈ ℓ. ξn : Σ and ξ : Σ^{N} ⊢ ∀n ∈ ℓ. ξn : Σ

are defined to be the unique semilattice homomorphisms from KN to (Σ^{N}, ⊥, ∨), (Σ^{Σ^{N}} , ⊥, ∨) and (Σ^{Σ^{N}} , ⊤, ∧) that extend m ↦ λn. (n =_{N} m) and m ↦ λξ. ξm (twice). In particular,

(ℓ′ ≼ ℓ) = (∀n ∈ ℓ′. n ∈ ℓ).

Using this we can state the axiom that characterises the topological case.

Axiom 10.4 For N ∈ obE,

Φ : ΣΣN, ξ : ΣN ⊢ Φξ = ∃ℓ:KN . Φ(λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ξn

or, in dependent-type notation (Remark 8.9),

Φξ = ∃ℓ:{ℓ : KN | Φ(λn. n ∈ ℓ)}. ∀n ∈ ℓ. ξn.

This defines an effective basis [G, §4] on X ≡ Σ^{N},

ℓ : KN ⊢ B^{ℓ} ≡ λξ. ∀n ∈ ℓ. ξn : ΣΣN, A_{ℓ} ≡ λΦ. Φ(λn. n ∈ ℓ) : ΣΣΣN

such that x : X, ϕ : ΣX ⊢ ϕx = ∃ℓ. A_{ℓ}ϕ ∧ B^{ℓ}x.

Corollary 10.5 We have an adjoint retraction

\begin{matrix}ΣKN \\ ΣΣN & ^{[figure: P]⊣ \begin{matrix}Σ^{p} \\ \end{matrix}} \end{matrix}

where p(ℓ) ≡ λn. n ∈ ℓ and P (G) ≡ λξ. ∃ℓ:KN . Gℓ ∧ ∀n ∈ ℓ. ξn. Proof By Axiom 10.4,

Φ : ΣΣN ⊢ P (Σ^{p}Φ) = λξ. ∃ℓ. Φ(λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ξn = Φ,

whilst G : ΣKN ⊢ Σ^{p}(P G) = λℓ. ∃ℓ′. Gℓ′ ∧ ∀n ∈ ℓ′. n ∈ ℓ = λℓ. ∃ℓ′ ≼ ℓ. Gℓ′ ≥ G. □

To replace this ≥ with equality, G has to be monotone in the following sense.

Notation 10.6 For any overt discrete object S equipped with an imposed order relation ≼, we write Υ(S, ≼) ⊂ ΩS for the E-object of upper subsets, or the functions G : S → Ω that take ≼ to the intrinsic order ≤ on Σ.

Proposition 10.7 ΩΣN [figure: Φ ↦ τ. λℓ. εΦ(λn. n ∈ ℓ); ≅; τ. λξ. ∃ℓ:KN . εGℓ ∧ ∀n ∈ ℓ. ξn ← G] Υ(KN, ≼) ⊂ ΩKN.

Proof Υ(KN, ≼) ⊂ ΩKN is by definition the image of ΩΣN under U(Σ^{p}). □

Theorem 10.8 The Eilenberg–Moore category for the monad on E in Section 6 is the category Frm(E) of frames and their homomorphisms over E. Hence L is equivalent to a full subcategory of Loc(E), the category of locales over E. Proof The free frame on N is Υ(KN, ≼) [18, Theorem II 1.2]. □

Now we characterise Ω-primes, which correspond to “generalised points” of locales.

Lemma 10.9 x : X ⊢ ε̃x ≡ λψ:ΩX. εψx : ΣΩX preserves ⊤, ⋏ and ⋁. Proof Let n : N ⊢ α_{n} : Σ, ψ^{n} : ΩX, where N is overt discrete, and M ≡ {n : N | α_{n}} in the sense of Remark 8.9. Then

ε̃( ⋁_{n:M} ψ^{n}) ≡ ε̃(τ. ∃n:N . α_{n} ∧ εψ^{n})  Remark 8.10
= ετ. (∃n:N . α_{n} ∧ εψ^{n})x  def ε̃
= ∃n:N . α_{n} ∧ εψ^{n}x
= ∃n:N . α_{n} ∧ ε̃ψ^{n}
= ⋁_{n:M} ε̃ψ^{n}  Remark 8.8

Also ε̃(⊤) = (ε⊤)x = ⊤x = ⊤, and, using Notation 8.6,

ε̃(ϕ ⋏ ψ) = ε(ϕ ⋏ ψ)x = (εϕ ∧ εψ)x = (εϕ)x ∧ (εψ)x = ε̃ϕ ∧ ε̃ψ.  □

Proposition 10.10 Γ ⊢ Q : ΣΩX is Ω-prime, i.e.

Γ, G : ΩΣΩX ⊢ εGQ = Q(τ. λx:X. (εG)(λψ:ΩX. εψx))

iff it preserves ⊤, ⋏ and ⋁ in the sense of the previous result.

Proof Put N ≡ ΩX ∈ obE and expand εG : ΣΣΩX ≡ Σ^{Σ^{N}} using Axiom 10.4:

F : Σ^{N} ⊢ εGF = ∃ℓ. (εG)(λψ. ψ ∈ ℓ) ∧ ∀ψ ∈ ℓ. F ψ.

Then (εG)(λψ:ΩX. εψx) = ∃ℓ:KN . εG(λψ. ψ ∈ ℓ) ∧ ∀ψ ∈ ℓ. εψx

so with α_{ℓ} ≡ εG(λψ. ψ ∈ ℓ) : Σ and β^{ℓ} ≡ τ. λx. ∀ψ ∈ ℓ. εψx = ⋀_{ψ∈ℓ} ψ : ΩX

we have RHS = Q(τ. λx. ∃ℓ:KN . εG(λψ. ψ ∈ ℓ) ∧ ∀ψ ∈ ℓ. εψx)

= Q(τ. ∃ℓ. α_{ℓ} ∧ εβ^{ℓ})
= ∃ℓ. α_{ℓ} ∧ Qβ^{ℓ}  Q preserves joins
= ∃ℓ. α_{ℓ} ∧ Q( ⋀_{ψ∈ℓ} ψ)
= ∃ℓ. α_{ℓ} ∧ ∀ψ ∈ ℓ. Qψ  Q preserves meets
= ∃ℓ. εG(λψ. ψ ∈ ℓ) ∧ ∀ψ ∈ ℓ. Qψ
= εGQ = LHS  □

Corollary 10.11 H : ΩX → ΩΓ is a homomorphism (H = f^{∗} for f : Γ → X) iff it preserves ⊤, ⋏ and ⋁. □

Next we generalise the basis (B^{ℓ}, A_{ℓ}) provided by Axiom 10.4 from Σ^{N} to its Σ-split and regular subspaces.

Proposition 10.12 Any Σ-split subspace i : X ↣ Σ^{N} has an effective basis defined by

ℓ : KN ⊢ β^{ℓ} ≡ Σ^{i}B^{ℓ} ≡ λx. ∀n ∈ ℓ. ixn : ΣX,
ℓ : KN ⊢ A_{ℓ} ≡ Σ^{I}A_{ℓ} ≡ λϕ. (Iϕ)(λn. n ∈ ℓ) : ΣΣX

such that x : X, ϕ : ΣX ⊢ ϕx = ∃ℓ. A_{ℓ}ϕ ∧ β^{ℓ}x.

This is the ∧-basis generated by the N-indexed sub-basis β^{n} ≡ λx. ixn [G, §5]. □

Remark 10.13 Now let i : X ↣ Σ^{N} be a regular mono in L. Instead of I : ΣX → ΣΣN, we have to use i_{∗} : ΩX → ΩΣN.

x : X  ψ : ΩX  \overline{εΣX} ϕ : ΣX

ξ : ΣN [figure: i]  Ψ : ΩΣN [figure: i^{∗} ≡ Ωi]⊣ \begin{matrix}i_{∗} \\  \end{matrix}[figure: εΣΣN] Φ : ΣΣN^{Σi }

Lemma 10.14 For Γ ∈ E, any Γ ⊢ ϕ : ΣX is ϕ = εψ = Σ^{i}Φ = Σ^{i}(εΨ) = ε(i^{∗}Ψ) where ψ = τ. ϕ, Ψ = i_{∗}ψ and Φ = εΨ. □

Definition 10.15 The basis on a locale X is, as before,

ℓ : KN ⊢ β^{ℓ} ≡ Σ^{i}B^{ℓ} ≡ λx. ∀n ∈ ℓ. ixn : Σ^{X}.

But this is no longer effective in the sense of [G, §4]. Instead of the term A_{ℓ} : ΣΣX in Proposition 10.12 we have an operator on terms-in-context:

E ∋ Γ ⊢ ϕ : Σ^{X} ; Γ ⊢ A_{ℓ}. ϕ ≡ A_{ℓ}(εi_{∗}(τ. ϕ)) ≡ εi_{∗}(τ. ϕ)(λn. n ∈ ℓ) : Σ

i.e. the free variables of ϕ must all be of overt discrete type.

Lemma 10.16 For E ∋ Γ ⊢ ϕ : Σ^{X}, ℓ : KN,

Γ ⊢ β^{ℓ} ≤ ϕ : Σ^{X} = Γ ⊢ A_{ℓ}. ϕ = ⊤ : Σ

In other words, A_{ℓ}. ϕ says, as a Σ-predicate, that β^{ℓ} ≤ ϕ, as a judgement (cf. Remark 8.1), so long as the types of the free variables of ϕ are overt discrete. Proof Using Propositions 8.7 and 9.6 (i^{∗} ⊣ i_{∗}), the following are equivalent:

β^{ℓ} ≡ Σ^{i}B^{ℓ} ≡ Σ^{i}(λξ. ∀n ∈ ℓ. ξn) ≤ ϕ : Σ^{X}
(i^{∗}(τ. λξ. ∀n ∈ ℓ. ξn) ≼_{ΩX} (τ. ϕ)) = ⊤
((τ. λξ. ∀n ∈ ℓ. ξn) ≼_{ΩΣN} i_{∗}(τ. ϕ)) = ⊤
(λξ. ∀n ∈ ℓ. ξn) ≤ εi_{∗}(τ. ϕ) : ΣΣN
A_{ℓ}. ϕ ≡ (εi_{∗}(τ. ϕ))(λn. n ∈ ℓ) = ⊤ : ΣΣN

since (λξ. ∀n ∈ ℓ. ξn) ≤ Φ iff Φ(λn. n ∈ ℓ) = ⊤. □

Proposition 10.17 If E ∋ Γ ⊢ ϕ : Σ^{X} then Γ, x : X ⊢ ϕx = ∃ℓ. A_{ℓ}. ϕ ∧ β^{ℓ}x. □

Remark 10.18 Hence, as we would expect, any open subspace ϕ of a general locale X is the join of the basic open subspaces β^{ℓ} contained in ϕ. However, expressing things in a symbolic rather than set-theoretic language has shown up certain subtleties in this result:

(a) In a locally compact locale, ϕ may vary with arbitrary (“geometrical”) parameters;

(b) in a general locale, on the other hand, the parameters must have overt discrete type (“combinatorial”, cf. Remark 5.8).

(c) In a coherent or spectral locale, i.e. one that has a basis of compact open sets [18, §II.3], the inclusion β^{ℓ} ≤ ϕ is continuous in ϕ or computationally observable predicate, by means of a term A_{ℓ};

(d) in a general locale, the inclusion β^{ℓ} ≤ ϕ is no longer a continuous or observable predicate but a statement A_{ℓ}. ϕ, in which ϕ may again only have overt discrete parameters;

(e) in the intermediate case of a locally compact locale, there is a predicate A_{ℓ}ϕ, applicable to arbitrary terms ϕ : Σ^{X}. However, its lattice-theoretic meaning is not β^{ℓ} ≤ ϕ but β^{ℓ} ≪ ϕ, and it says that β^{ℓ} contributes to the join, as explained in [G, §4].

11 Locally compact locales

This section completes the investigation of the minimal topological situation by characterising the objects X ∈ obS as locally compact locales, or the (imposed) algebras ΩX as continuous distributive lattices. This is in effect another proof of the monadic property for LKLoc, two of which have already been published: [A, Theorem 5.12] and [B, Theorem 3.11]. Since much of the argument is the same as that in [G], we omit the proofs of the results that also appear there.

We begin by showing that we only need to consider the imposed structure on ΩX.

Lemma 11.1 ΣΣN has enough points.

[figure: ΩKN; εΣKN; ΣKN; KN; ⊂; ΩN]

[figure: ΥKN; UP; Ωp; = = = = =; ΩΣN; εΣΣN; ΣΣN; P; Σp; ΣN; p; εΣN; UΣN; ‖]

Proof By Corollary 10.5, p : KN ↠ ΣN is epi since Σ^{p} is mono (split by P). So εΣN is epi by cancellation in the diagram on the right, i.e. ΣN and likewise ΣKN have enough points. Both rectangles on the left commute, by naturality of ε with respect to P and Σ^{p}, so εΣΣN is also epi by cancellation. □

Proposition 11.2 ΣX has enough points.

X  ΩX  \overline{εΣX} ΣX

[figure: ΣN; i; ΩΣN; Ωi; UI; εΣΣN; ΣΣN; Σi; I]

Proof Since ε is natural with respect to Σi, which is epi, εΣX is epi by cancellation. We cannot extend this to X ∈ obL, because we have no handle on ΣΣX there. □

We shall need to use Scott continuity of maps between (imposed) lattices, i.e. preservation of directed joins. The next definition is discussed in [G, §2], and the four results following it are proved in §§6–7.

Definition 11.3 Γ, s : S ⊢ ϕ^{s} : Σ^{X} is called a directed diagram if S is overt discrete with an imposed semilattice structure (S, 0, +) with respect to which ϕ^{s} is covariant:

Γ, s, t : S ⊢ ϕ^{s} ≤ ϕ^{s+t} : Σ^{X}.

As in Remark 8.10, we need to consider, more generally,

∃s:{s : S | α_{s}}. ϕ^{s} ≡ ∃s:S. α_{s} ∧ ϕ^{s}

where α_{s} : Σ is contravariant. The subtype remains a semilattice so long as

α_{0} = ⊤ and α_{s+t} = α_{s} ∧ α_{t}.

We can turn the effective bases for ΣΣN and ΣX in the previous section into directed bases using the string of retractions

ΣΣX ◁ ΣΣΣN ◁ ΣΣKN ◁ ΣKKN.

Lemma 11.4 Σ^{N} has a directed basis expansion,

F : ΣΣΣN, Φ : ΣΣN ⊢ FΦ = ∃L:KKN . FA_{L} ∧ ∀ℓ ∈ L. Φβ^{ℓ},

where A_{L} ≡ λξ:Σ^{N} . ∃ℓ ∈ L. ∀n ∈ ℓ. ξn and β^{ℓ} ≡ λn. n ∈ ℓ. □

Proposition 11.5 Let i : X Σ^{N} with Σ-splitting I. Then X has a directed basis expansion

F : ΣΣX, ϕ : ΣX ⊢ F ϕ = ∃L:KKN . F γ^{L} ∧ D_{L}ϕ,

where γ^{L} ≡ λx. ∃ℓ ∈ L. ∀n ∈ ℓ. ixn and D_{L} ≡ λϕ. ∀ℓ ∈ L. Iϕ(λn. n ∈ ℓ). □

Corollary 11.6 All Γ ⊢ F : ΣΣX and F : Σ^{X} → Σ^{Y} in S preserve directed joins (in the intrinsic order). □

Corollary 11.7 Γ ⊢ P : ΣΣΩY is Σ-prime iff it preserves the finitary lattice operations. □

In the presence of the underlying set axiom, we can identify the role of Scott continuous functions between continuous lattices. Again this doesn’t extend to general locales, as we have no handle on ΣΣX in that case. (A further axiom, that ΣΣ(−) preserves certain equalisers, would probably rectify this situation.)

Theorem 11.8 Γ ⊢ G : ΣΩX is of the form G = λψ. F (εψ) for some Γ ⊢ F : ΣΣX iff G preserves directed joins in the imposed order. In this case, F is unique. Proof Using Remark 8.10 and Proposition 11.6, for Δ, s : S ⊢ θ^{s} : ΩY,

F ε ⋁ ; _{s:α_{s}} θ^{s} = F (ετ. ∃s. α_{s} ∧ εθ^{s}) = ∃s. α_{s} ∧ F (εθ^{s}) = ⋁ ; _{s:α_{s}} F ε(θ^{s}).

For the converse, we first use Proposition 11.5 to express ψ : ΩY as

ψ = ⋁ ; _{L:D_{L}(εψ)} τ. γ^{L}  or  εψx = ∃L. D_{L}(εψ) ∧ γ^{L}x.

Suppose that G preserves this directed join, and let

Γ ⊢ F ≡ λϕ:Σ^{Y} . ∃L. ε(G(τ. γ^{L})) ∧ D_{L}ϕ.

Then Gψ = ⋁ ; _{L:D_{L}(εψ)} G(τ. γ^{L}) = ∃L. D_{L}(εψ) ∧ ε(G(τ. γ^{L})x) = F (εψ).  □

Corollary 11.9 A function G : ΩY → ΩX in E is UF for some unique (“intrinsically Scottcontinuous”) morphism F : Σ^{Y} → Σ^{X} in S iff G is Scott-continuous (preserves directed joins) with respect to the imposed order. □

Corollary 11.10 A locally compact locale K is compact iff Σ^{!_{K}} has a right adjoint [C, Definition 7.7]. Proof For any locally compact locale K, the E-map !_{K}^{∗} ≡ Ω!_{K} ≡ UΣ^{!_{K}} : Ω → ΩK has a right adjoint !_{∗} with respect to the imposed order (Proposition 9.6). This preserves directed joins iff K is compact in the sense of locale theory [18, §III 1]. In this case, !_{∗} = UA for some unique A : Σ^{K} → Σ, so

id ≼ !^{∗} ·!_{∗} = U(Σ^{i} · A) and U(A · Σ^{i}) = !_{∗} ·!^{∗} ≼ id.

These imposed inequalities may be lifted to intrinsic ones as Σ^{K} has enough points (Proposition 11.2), so Σ^{i} ⊣ A in the intrinsic order. □

Remark 11.11 The proof of Theorem 11.8 is very delicate. Notation 7.4 allows us to write τ. γ^{L} because L : KKN ∈ obE is the only free variable in γ^{L}. On the other hand, F ≡ λϕ:Σ^{Y} . G(τ. ϕ) would not be well formed, because the type of the variable ϕ is not overt discrete. Similarly, the result cannot be extended to L using Remark 11.12, because we would want to form D_{L}. ϕ where ϕ : Σ^{X} is a variable.

Remark 11.12 There is also a directed basis expansion for X ∈ obL,

{E ∈ Γ ⊢ ϕ : Σ^{X} \atop Γ, F : ΣΣX ⊢ F ϕ = ∃L:KKN . F γ^{L} ∧ D_{L}. ϕ}

where D_{L}. ϕ is defined in a similar way to A_{ℓ}. ϕ in Definition 10.15, but it turns out not be very useful.

The remainder of this section completes the characterisation of the minimal topological situation as the category of locally compact locales.

Remark 11.13 Recall from Proposition 4.5 that an (imposed) complete lattice (A, ≼) in E is a continuous frame (the topology of a locally compact locale) iff there are functions

A[figure: J; \underline{H}] ΥKN

with N ∈ obE such that H · J = id_{A}, J preserves directed joins and H preserves finite meets and arbitrary joins.

Corollary 11.14 For any X ∈ obS in the minimal topological situation, the imposed structure on ΩX in E is that of a continuous frame. Proof Let i : X Σ^{N} with Σ-splitting I. Then H ≡ i^{∗} ≡ UΣ^{i} preserves finite meets and arbitrary joins (Proposition 10.9), whilst J ≡ UI preserves directed joins (Proposition 11.9). □

For the converse, we use the idempotent E = I · Σ^{i} : ΣΣN : ΣΣN or E′ = UE = J · H : ΩΣN → ΩΣN, for which the term nucleus was appropriated in [B, §2]. We have to show that the properties of H and J in Lemma 4.5 provide the hypotheses of Beck’s theorem characterising monads.

Lemma 11.15 Let H and J be monotone functions between semilattices such that H · J = id and H preserves ⋏. Then E ≡ J · H satisfies E(ϕ ⋏ ψ) = E(Eϕ ⋏ Eψ). □

Lemma 11.16 If E : Σ^{X} → Σ^{X} satisfies

ϕ_{1}, ϕ_{2} : Σ^{X} ⊢ E(ϕ_{1} ∧ ϕ_{2}) = E(Eϕ_{1} ∧ Eϕ_{2}) and E(ϕ_{1} ∨ ϕ_{2}) = E(Eϕ_{1} ∨ Eϕ_{2})

then it is a nucleus in the sense of [B, Definition 4.3], i.e.

F : ΣΣΣX ⊢ E(λx. F(λϕ. Eϕx)) = E(λx. F(λϕ. ϕx)).  □

Proposition 11.17 Every imposed distributive continuous lattice A arises as some ΩX. Proof By Lemma 4.5, A gives H and J and so E′ ≡ J · H : ΩΣA → ΩΣA. As this preserves directed joins, Corollary 11.9 with Y ≡ Σ^{A} gives E : ΣΣA → ΣΣA with E′ = UE.

[figure: ΣΣA; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{i}; Σ^{X}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; I; ΣΣA]

[figure: ΩΣA; εΣΣA; H; A; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; J; ΩΣA; εΣΣA]

Now E′, by construction, satisfies the equation in Lemma 11.15,

ψ_{1}, ψ_{2} : ΩΣA ⊢ E′(ψ_{1} ⋏ ψ_{2}) = E′(E′ψ_{1} ⋏ E′ψ_{2}) : ΩΣA

and a similar one with ⋎. Since ΣΣA has enough points by Lemma 11.1, we may apply the rule in Lemma 7.8, along with the relationship between ⋏ and ∧ in Notation 8.6, to deduce the analogous equations for E, namely

ϕ_{1}, ϕ_{2} : ΣΣA ⊢ E(ϕ_{1} ∧ ϕ_{2}) = E(Eϕ_{1} ∧ Eϕ_{2}) : ΣΣA

and similarly with ∨. By Lemma 11.16, E is then a nucleus, and so defines a Σ-split subspace

i : X  Σ^{N} such that A ≅ ΩX.  □

Theorem 11.18 In the minimal topological situation, S is equivalent to the category of locally compact locales over E. □

Remark 11.19 If the topos E satisfies the axiom of choice (for example in the form that all epis split, [17, §5.2]) then every object of S has enough points, so S is equivalent to the category of locally compact sober spaces [18, Theorem VII 4.3].

This result is peculiar to the topological case (ℵ = ℕ). In CCD^{op}, the real unit interval does not have enough points [10, Example 9] [B, Example 3.12], and this also provides a counterexample in the intermediate ℵ-case. □

12 Sober spaces and locales

Now we turn from the minimal to the complete situation, in which there are equalisers, and Σ is injective with respect to regular monos in L. We know from Sections 6 and 10 that

L ⊂ Loc(E) ≡ Frm^{op}(E),

where Frm(E) is the category of Eilenberg–Moore algebras for the monad ΣΩ(−) on E. (L is equivalent to a full subcategory of Loc(E), since L is intrinsic and Loc(E) imposed.)

The first task is to show that the category of sober topological spaces is embedded in S, or more precisely

L ∩ P ≃ Sob(E) ⊂ Sp(E).

Afterwards we show that L ≃ Loc(E) when a stronger notion of injectivity holds.

So let’s state the classical definition.

Definition 12.1 An (imposed, not necessarily T_{0}) topological space over E is an object N ∈ obE together with a subframe e^{∗} : A ⊂ ΩN, i.e. the square on the left commutes.

Recall that ΩN is the powerset (collection of all subsets) of N and A is the subcollection of open subsets. Like any frame homomorphism, e^{∗} has an (imposed) right adjoint e_{∗}, which yields the open interior of an arbitrary subset.

[figure: ΩΣA; ΩΣe^{∗}; ΩΣΩN; N_{1}; A_{1}; e_{1}^{∗}; ΩN_{1}]

[figure: A; α; e^{∗}; ΩN; ΩιN; N_{2}; f; A_{2}; H; e_{2}^{∗}; ΩN_{2}; Ωf ≡ f^{∗}]

A function f : N_{1} → N_{2} in E is continuous (in the imposed sense) if its inverse image map f^{∗} takes open subsets of (N_{2}, A_{2}) to open subsets of (N_{1}, A_{1}). This means that there is a map H that makes the right-hand square commute. Since e_{2}^{∗}, f^{∗} and e_{1}^{∗} are frame homomorphisms, so is H, and since e_{1}^{∗} is mono, H is unique. We write Sp(E) for this category.

Exercise 12.2 The forgetful functor Sp(E) → E by (N, A) ↦ N is faithful and has adjoints on both sides, as in Remark 2.1. □

This forgetful functor isn’t the same as our “underlying set” functor U : S → E, because their sources are different categories, but we shall connect them by functors in both directions.

Proposition 12.3 There is a functor S → Sp(E) that takes X ∈ obS to (UX, A), where the diagram in E on the left shows how the frame (A, α) is defined, and the morphism f : X_{1} → X_{2} to Uf : (UX_{1}, A_{1}) → (UX_{2}, A_{2}).

[figure: ΩΣΩX; ΩΣA; ΩΣΩUX; ΩX_{1}; A_{1}; ΩUX_{1}]

[figure: ΩX; ε̃_{X}^{∗}; A; α; . . . . . . . . . . . . . . . . .; ΩUX; ε̃_{UX}^{∗}; ΩX_{2}; f^{∗}; A_{2}; H; . . . . . . . . . . . . . . . .; ΩUX_{2}; (Uf)^{∗}]

\overline{ε_{X}^{∗}}

Proof The frame (A, α) is given by the image factorisation of ε_{X}^{∗} in Frm(E). In more detail, let A be the image as a set (object of the topos E). The adjunction ε^{∗} ⊣ ε_{∗} splits as a closure on ΩX and a coclosure on ΩUX, so the two parts are split. Hence ΩΣ(−) preserves the factorisation, from which the structure map α is defined, and satisfies the Eilenberg–Moore equations.

The function Uf is continuous (in the imposed sense) because, by a similar argument, there is a mediating homomorphism H : A_{2} → A_{1}. □

For this functor to be faithful we clearly need at least that ε_{X}^{∗} be mono (Lemma 7.8), whilst constructions involving Ω generally only tell us about L (Remark 6.13).

Proposition 12.4 There is a functor Sp(E) → L∩P ⊂ S that takes the topological space (N_{1}, A_{1}) to the equaliser E_{1} in S in the top line, where i_{1}·p_{1} : N_{1} → Σ^{A_{1}} is the double exponential transpose of A_{1} ↣ ΩN_{1} ↠ Σ^{N_{1}}. Moreover (A_{1}, α_{1}) ≅ (ΩE_{1}, Ωε̃E_{1}).

[figure: N_{1}; A_{1}; e_{1}^{∗}; ΩN_{1}; N_{1}; p_{1}; E_{1}; i_{1}; ΣA_{1}; Σα_{1}; ε̃ΣA_{1}; ΣΩΣA_{1}]

[figure: N_{2}; f; A_{2}; H; e_{2}^{∗}; ΩN_{2}; Ωf; N_{2}; f; p_{2}; E_{2}; . . . . . . . . . . . . . . . .; i_{2}; ΣA_{2}; ΣH; Σα_{2}; ε̃ΣA_{2}; ΣΩΣA_{2}; ΣΩΣH]

Similarly, the functor takes the continuous function f to the dotted map. Proof Since α is the structure map of an Eilenberg–Moore algebra, it is the coequaliser of the parallel pair in the following diagram, so there is a mediator u_{1} : A_{1} → ΩE_{1}.

ΩE_{1}
[figure: p_{1}^{∗}; i_{1}^{∗}]
ΩN_{1}  ΩΣA_{1} [figure: \underline{ΩΣα_{1}}; \underline{Ωε̃ΣA_{1}}] ΩΣΩN_{1}
[figure: e_{1}^{∗}; α_{1}]
A^{u_{1} . . . . . . . . . . . . . . . .}

Then u_{1} is split epi because i_{1}^{∗} is, by injectivity (Lemma 6.7), whilst u_{1} is split mono because e_{1}^{∗} is, by Definition 12.1, so u_{1} : A_{1} ≅ ΩE_{1} in Frm(E).

Since E_{1} is constructed as an equaliser, it is in L. Then we may use Corollary 6.12(b) and the fact that p_{1}^{∗} = e_{1}^{∗} · u_{1}^{−1} is split mono to deduce that p_{1} is epi and E_{1} ∈ obP.

The image of the morphism is the mediator to the second equaliser. □

Putting these constructions together, we have

Theorem 12.5 P ∩ L is equivalent to the full reflective subcategory of Sp(E) that consists of sober spaces in the traditional sense (i.e. not that of Axiom 3.3). Proof The composite L ∩ P ⊂ S → Sp(E) → L ∩ P takes

X ↦ (UX, ΩX ↣^{ε_{X}^{∗}} ΩUX) ↦ (X ↣^{i} ΣΩX ⇉ ΣΩΣΩX)

where ε_{X}^{∗} is mono because X ∈ obP and i is an equaliser because X ∈ obL. We leave it to the reader to show that our functors S ⇆ Sp(E) agree with the usual ones Loc ⇆ Sp [18, §II 1], whose fixed category is Sob(E). □

The two constructions are not themselves adjoint, but factor as two adjunctions S ⇆ L ⇄ Sp(E) in opposite senses. If we transfer the imposed notion of continuity from Sp(E) to our category S, we can see the separate (dual) roles of P and L in this result.

Definition 12.6 We say that a function (E-morphism) f : UX → UY between the underlying sets of X, Y ∈ obS is continuous (in the “imposed” sense) if there is a homomorphism H that makes the right hand square commute:

[figure: UX; f; UY; ΩUX; f^{∗}; ΩUY]

[figure: X; ε_{X}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; g; Y; ε_{Y}; ΩX; ε_{X}^{∗}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; H; ΩY; ε_{Y}^{∗}]

We obtain this situation if we are given an S-morphism (“intrinsically continuous function”) g : X → Y, when f = Ug and H = g^{∗}.

Theorem 12.7 Let X ∈ obP and Y ∈ obL. Then every continuous function f : UX → UY in the imposed sense arises in this way from a unique intrinsically continuous function g : X → Y in S. Proof Since ε_{X}^{∗}, ε_{Y}^{∗} and f^{∗} are Eilenberg–Moore homomorphisms for the monad on E, so too is H, since ε_{X}^{∗} is mono (because X has enough points). Then the transpose of H is an Ω-prime x : X ⊢ Q : ΣΩY, which arises from a unique Σ-prime since Y ∈ obL. This in turn corresponds to an S-morphism g : X → Y with f = Ug, P = λψ:ΣY . ψ(gx), Q = λψ:ΩY . εψ(gx) and H = g^{∗}. □

Now we consider the equivalence Loc(E) ≃ L ⊂ S. Since Sob(E) satisfies the conditions that we have so far imposed on L, in particular injectivity of the Sierpiński space, we have to assert another axiom.

Definition 12.8 The pair f, g : Σ^{N} ⇉ Σ^{M} in S is said to be Ω-contractible if there is some J : ΩΣN → ΩΣM in E such that

Ωf · J = id_{ΩΣN}  and  Ωg · J · Ωf = Ωg · J · Ωg.

The complete situation asserts the existence of the equaliser X ↣^{i} Σ^{N} ⇉ Σ^{M}, and that Ω take the regular mono i to a split epi. We now require that Ω take the equaliser diagram to a coequaliser diagram. In this case there is a unique map I : ΩX → ΩΣN such that

Ωi · I = id_{ΩX}  and  Ωg · J = I · Ωi.

We have already seen this happen for spatial locales in Proposition 12.4, but if it holds for all Ω-contractible pairs in L then we call Σ exactly injective.

Theorem 12.9 L ≃ Loc(E) iff Σ is exactly injective. Proof We already know that L ⊂ Loc(E) fully, so it only remains to show that every frame (Eilenberg–Moore algebra) is ΩX for some object X ∈ obL. We formulated the condition in exactly the way that we need for Beck’s theorem [37, Theorem 7.5.9]. □

Remark 12.10 Faced with a non-unique existence property, logicians and algebraists react in different ways. The logician’s answer is to ask for a canonical choice, which, in the case of injectivity, leads us to Σ-split monos.

The algebraist’s response is to classify the equivalence relation that is defined between the choices, and we chose the word “exact” to suggest the “image = kernel” idea of cohomological algebra.

ΩΣM  θ  θ′
[figure: Ωf; Ωg; Ωg; Ωf]
ΩΣN [figure: Ωf; J; Ωg]  ϕ = θ · f  θ · g = ϕ′′ = θ′ · g  θ′ · f = ϕ′
[figure: Ωi; Ωi]
[figure: ΩX; Ωi; I; ϕ · i = ψ = ϕ′ · i; Ωi]

Here, if ϕ, ϕ′ : Σ^{N} ⇉ Σ have the same restriction ϕ · i = ψ = ϕ′ · i : U → Σ, there are θ ≡ Jϕ, θ′ ≡ Jϕ′ : Σ^{M} ⇉ Σ and ϕ′′ ≡ Iψ : Σ^{N} → Σ making a zig-zag, which proves that ϕ · i = ϕ′ · i. □

Finally we summarise the many descriptions that we have of morphisms.

Theorem 12.11 The morphisms f : X → Y of L coincide with continuous functions as variously formulated in traditional topology, locale theory and abstract Stone duality, being in natural bijection with

(a) Eilenberg–Moore homomorphisms Σ^{f} : Σ^{Y} → Σ^{X} for the monad on S arising from the adjunction Σ^{(−)} ⊣ Σ^{(−)};

(b) Σ-primes x : X ⊢ λψ. ψ(fx) : ΣΣY;

(c) Eilenberg–Moore homomorphisms f^{∗} : ΩY → ΩX for the monad on E arising from the adjunction Σ ⊣ Ω;

(d) Ω-primes x : X ⊢ λψ. (εψ)(fx) : ΣΩY;

(e) adjoint pairs f^{∗} ⊣ f_{∗} where f^{∗} also preserves ⊤ and ⋏ in the imposed lattice structure;

(f) frame homomorphisms f^{∗}, where f^{∗} preserves ⊤, ⋏ and ⋁;

(g) x : X ⊢ Q ≡ λψ. (εψ)(fx) : ΣΩY preserving ⊤, ⋏ and ⋁;

(h) functions UX → UY for which the inverse image of any open subset of Y is open in X, if X has enough points;

(i) x : X ⊢ P ≡ λϕ. ϕ(fx) : ΣΣY preserving ⊤, ⊥, ∧ and ∨, if Y is locally compact;

(j) lattice homomorphisms H : Σ^{Y} → Σ^{X}, if Y is locally compact. □

13 The reflection and function-spaces in L

The known cartesian closed supercategories of spaces (filter spaces and equilogical spaces) admit reflections onto the traditional category of topological spaces. Moreover, when topological function spaces exist, they are also the exponentials in the supercategory.

In this section we shall see why this happens, using a little abstract category theory: it is (once again) essentially the comparison between the composite adjunction in Section 6 and the monad for frames. We also see the abstract explanation of some of the topologies that have been defined on the set of continuous functions but which are not categorical exponentials.

Theorem 13.1 The inclusion L ⊂ S has a left adjoint, \overline{(−)} , given by the equaliser:

[figure: X; \overline{X}; ΣΩX; ΣΩΣΩX]

in which X ↠ \overline{X} is epi.

Proposition 13.2 (ΣΩ(−), ε̃, μ, σ) is a strong monad on S, where

μX ≡ ΣιΩX : ΣΩΣΩX → ΣΩX  and  σ : ΣΩX × Y → ΣΩ(X × Y)

are defined by

G : ΣΩΣΩX  ⊢ μG ≡ λψ. G(τ. λG. Gψ)
G : ΣΩX, y : Y ⊢ σ(G, y) ≡ λθ:Ω(X × Y). G(τ. λx. εθ(x, y)) : Σ.

Proof The strength σ is related to the unit ε̃ by the equation

σ_{X,Y} · (ε̃X × Y) = ε̃(X × Y),

which, in symbolic form, is

σ(ε̃x, y) = λθ. (λψ. εψx)(τ. λx′. εθ(x′, y))
= λθ. (ετ. λx′. εθ(x′, y))x
= λθ. εθ(x, y) = ε̃(x, y)

We shall not need the other equation,

T σ_{X,Y} · σ_{T X,Y} · (μ_{X} × Y) = μ_{X×Y} · σ_{X,Y} ,

so we leave it as an exercise. □

Lemma 13.3 Let 𝕋 ≡ (T, ε̃, μ, σ) be a strong monad on a category S with finite limits. Let L ⊂ S be the Lambek–Rattray fixed category [21] of 𝕋, with reflection \overline{(−)} . Let X ∈ obS and Y, Z ∈ obL. Then there are two unique lifting properties

X × Y \overline{ρ_{X×Y}} \overline{X × Y}

[figure: f]

[figure: \overline{X} × Y; ρ_{X} × Y; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Z; . . . . . . . . . . . . . . . . .]

Proof In the following diagram, the three triangles and the trapezium with shapes

[figure: ε̃T X × Y; T ε̃X × Y]
[figure]
[figure: and]
[figure]
[figure: ε̃T (X × Y)]

are respectively instances of the law that relates the strength σ to the unit ε̃ for the strong monad 𝕋, and naturality of σ with respect to η. The other trapezium, the two lower right squares squares and the forks from X × Y are instances of naturality of ε̃.

[figure: \overline{X} × Y; T X × Y; ε̃T X × Y; T ε̃X × Y; T T X × Y]

[figure: ....................; ρ_{X} × Y; ε̃X × Y; ε̃(T X × Y)]

X × Y  T (T X × Y) \begin{matrix}σ_{T X,Y} \\  \end{matrix}

[figure: f; ^{........}; ρ_{X×Y}; _{........}; ε̃(X × Y); T (ε̃X × Y)]

[figure: \overline{X × Y}; . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .; T (X × Y); σ_{X,Y}; ε̃T (X × Y); T ε̃(X × Y); T T (X × Y); T σ_{X,Y}]

[figure: Z; . . . . . . . . . . . . . . . . .; ε̃Z; T Z; T f; ε̃T Z; T ε̃Z; T T Z; T T f]

Hence all composites from X × Y to each of the four objects in the column on the right are equal. But \overline{X} × Y, \overline{X × Y} and Z are the equalisers of their rows, so there are unique dotted mediators as shown. □

Corollary 13.4 \overline{X} × Y ≅ \overline{X × Y} . Proof Put each of them for Z. □

Remark 13.5 In general, \overline{X × Y} is not isomorphic to \overline{X} × \overline{Y} for X, Y ∈ obS. If it were, an argument similar to the following would make L cartesian closed [8], given that S is, but Sob(E) ⊂ L ⊂ Loc(E) cannot be cartesian closed. □

The exponential Z^{Y} exists in L when Y ∈ obL and Z is locally compact, as we may deduce easily from Theorem 3.22. I don’t know whether there are other (“sporadic”) examples of exponentials in Loc, but if there are then they’re all good in S:

Theorem 13.6 The inclusion L ⊂ S preserves exponentials. Proof Let Y, Z, F ∈ obL such that F ∈ obL has the universal property of Z^{Y}, i.e.

\overline{X} × Y → Z ; = ; \overline{X} → F

for any object \overline{X} ∈ obL. Then the same correspondence holds in S for any X ∈ obS. □

Remark 13.7 Applying Remark 1.14, two ways of forming pseudo-exponentials in Sp are known:

(a) (S(Y, Z) → \overline{Z^{Y}} ) ∈ obE ↓ S is Isbell’s natural topology, cf. Theorem 3.22, and

(b) (S(Y, Z) → Z^{UY} ) ∈ obE ↓ S is the topology of pointwise convergence. □

Question 13.8 Defining the type (Y → Z) as \overline{Z^{Y}} in L, we have a model of the λβ-calculus (not η). But it is much better than this: we usually use the η-rule to prove that composition of functions in the λ-calculus, namely

g · f ≡ λx. g(fx),

is associative with identities, but this follows directly from the fact that L is a category.

What, then, are the rules of the non-η λ-calculus of which we have a model? So far as I can gather, nobody has formulated them, as the problem falls amongst three stools: λ-calculus, category theory and topology.

One approach would be to add the rules for categories with products to the λβ-calculus, since we have to deal with multiple variables. But arguably the λ-calculus handles variables far more tidily than does the theory of categories with products, so why not re-introduce variables as place-holders? Where, then, is the restriction — is it on abstraction or application?

14 Injectivity and a new recursive calculus

The whole of this investigation has depended on the “underlying set” functor Δ ⊣ U, which only exists in a Set- or topos-based version of the theory, and not in a recursive one. On the other hand, the ASD literature has shown that many topological ideas can be expressed in the λ-calculus without U — its role in this paper has largely been to force conformity with the traditional theory.

In order to state the injectivity and exact injectivity axioms, however, we did pre-suppose one of the functors U or Ω. As we have claimed that injectivity of the Sierpiński space is a characteristic feature of topology and of computation, we must find another way of stating this property.

We have been careful only to say that Σ is injective with respect to regular monos in L (Definition 3.23), because it cannot be in S.

Lemma 14.1 Let i : U → X in a category with finite products and powers of Σ (Axiom 1.5). Then the following three non-unique lifting properties are equivalent (by exponential transposition) for each object Γ.

(a) Σ is injective with respect to i × Γ : U × Γ → X × Γ;

(b) Σ^{Γ} is injective with respect to i : U → X;

(c) Σ^{i} is surjective with respect to Γ.

[figure: U × Γ; i × Γ; X × Γ; U; i; X; Σ^{U}; Σ^{i}; Σ^{X}]
[figure: σ; ............; τ; ϕ; ............; ψ; ϕ̃; ............; ψ̃]
Σ  Σ^{Γ}  Γ

Moreover, in the case Γ ≡ Σ^{U}, they imply that

(d) there is some morphism I : Σ^{U} → Σ^{X} such that Σ^{i} · I = id_{Σ^{U}} (Definition 3.4), which conversely implies (a–c) for all Γ. □

Example 14.2 The inclusion ℕ^{ℕ} ↣ ℕ_{⊥}^{ℕ} is Σ-regular mono but not Σ-split in Sp, Loc and the complete topological situation.

[figure: ℕ^{ℕ}; i; ℕ_{⊥}^{ℕ}; ⊤; ↓; Σ^{ℕ}]

Proof In the diagram, ↓ is the definedness or termination predicate on partial functions with open support: f ↦ λn. (fn)↓ in recursion-theoretic notation, or (ℕ ↩ U → ℕ) ↦ ϕ where ϕ classifies U topologically. The total functions constitute the equaliser of this with ⊤, so i is regular mono.

The object ℕ_{⊥}^{ℕ} is the closed subspace of Σ^{ℕ×ℕ} co-classified by λϕψ. ∃n. ϕn ∧ ψn, so it and Σ^{ℕ} are locally compact.

Therefore if i were Σ-split, ℕ^{ℕ} would also be locally compact, but it is not. (I have a proof of this within ASD, but it wouldn’t fit in this marginal note.) □

Corollary 14.3 Σ cannot be injective with respect to all regular monos in S, because this class is closed under (−) × Γ. □

Remark 14.4 Therefore we must weaken the sense in which Σ^{i} is to be “onto”: whenever i is regular mono maybe Σ^{i} should be regular epi, rather than surjective. For exact injectivity (Definition 12.8), if i is the equaliser of f, g : X ⇉ Y, perhaps Σ^{i} should be the coequaliser of Σ^{f}, Σ^{g} : Σ^{Y} ⇉ Σ^{X}. On the other hand, Σ^{(−)} always takes coequalisers to equalisers, so the basic idea is that

Σ^{2}(−) preserves equalisers.

However, this still isn’t quite right.

Example 14.5 Since the category has stable disjoint sums, the diagram

[figure: 0; 2; id; swap; 2,]

is an equaliser (where swap interchanges the elements of 2), but Σ^{(−)} takes it to

[figure: 1; Σ^{Σ}; Σ × Σ; \underline{id}; \underline{swap}; Σ × Σ,]

where swap interchanges the components of the product. □

Definition 14.6 In a coreflexive equaliser diagram, as shown on the left, i is the equaliser of f and g, and r · f = id_{X} = r · g.

U[figure: i] X

[figure: U; i; X; f; .; .; .; .; .; .; .; r.........; g; Y]

[figure: X; i; g; Y; f]

In this case the square on the right is a pullback (intersection). Whereas Σ-split equalisers and monos are special, every Σ-regular mono can be expressed as a coreflexive equaliser, simply by replacing Y with X × Y.

The proposal for the exact injectivity axiom for a cartesian closed category of recursive spaces is this:

Axiom 14.7 The functor ΣΣ(−) should preserve coreflexive equaliser diagrams.

We put this in symbolic form before explaining how it implies both monadicity (Axiom 3.5) and that Σ is injective in L but not in S. It is the additional argument x to θ in the Σ^{{}}E and Σ^{{}}β rules that captures coreflexivity.

Notation 14.8 We introduce the equaliser of f, g : X ⇉ Y by the type-forming rule

X type  Y type  x : X ⊢ fx, gx : Y
{x : X | fx = gx : Y } type {}F

in which the variable x is bound (as for comprehension in set theory), although we shall often omit it and the type Y. As we don’t want to introduce dependent types at present, fx and gx must not contain any free variables besides x : X.

Remark 14.9 We need finite products in the restricted λ-calculus to make much sense of this in practice. Alternatively, since products and equalisers are both forms of categorical limit, we could combine them into a single notation, with several typed bound variables on the left of the divider. (In programming languages, these are called fields of a record.)

Since the type Y may also be a product, the conjunction of several equations is allowed on the right.

Definition 14.10 The rules of the subspace calculus are those of the sober λ-calculus [A, §8] plus

Γ ⊢ a : X Γ ⊢ fa = ga : Y

Γ ⊢ admit a : {X | f = g} {}I

u : {X | f = g} ⊢ iu : X  {}E_{0}
u : {X | f = g} ⊢ f(iu) = g(iu) : Y  {}E_{1}

Γ ⊢ a : X Γ ⊢ fa = ga : Y

Γ ⊢ i(admit a) = a : X {}β

u : {X | f = g} ⊢ admit(iu) = u : {X | f = g}  {}η
ϕ : Σ^{X} ⊢ Σ^{i}ϕ ≡ (λu. ϕ(iu)) : Σ^{{X|f=g}}  Σ^{{}}I

Γ ⊢ F : Σ^{2}X Γ, θ : Σ^{X×Y} ⊢ F (λx. θ(x, fx)) = F (λx. θ(x, gx))

Γ, ψ : Σ^{{X|f=g}} ⊢ Admit F ψ : Σ

Σ^{{}}E

Γ ⊢ F : Σ^{2}X Γ, θ : Σ^{X×Y} ⊢ F (λx. θ(x, fx)) = F (λx. θ(x, gx))
Γ, ϕ : Σ^{X} ⊢ Admit F (Σ^{i}ϕ) ≡ Admit F (λu. ϕ(iu)) = F ϕ

Σ^{{}}β

G : Σ^{2}{X | f = g} ⊢ Admit(Σ^{2}iG) ≡ Admit (λϕ. G(λu. ϕ(iu))) = G  Σ^{{}}η

Associated with the function-symbol i and the operators admit and Admit are further rules stating that they preserve equality, just as application, λ-abstraction and focus do.

For topology, of course, we add ℕ with recursion, the lattice structure of Σ and the Scott principle (Axiom 10.4), though the last may need to be generalised.

Exercise 14.11 The expressions

Admit(Σ^{2}iG) : Σ^{2}{X | f = g} and admit(Σ^{2}iG) : {Σ^{2}X | Σ^{2}(id, f) = Σ^{2}(id, g)}

are well formed (this is Σ^{{}}I_{1}) and, according to either of the last two rules,

Admit(Σ^{2}iG)(Σ^{i}ϕ) = (Σ^{2}iG)ϕ = G(Σ^{i}ϕ).  □

Exercise 14.12 Any nucleus E on X in the sense of [B] corresponds to a Σ-split equaliser. The function-symbol I in [B, §8] and the new operator Admit for this equaliser are mutually defined by

Iθ ≡ λx. Admit(λϕ. Eϕx)θ and Admit F ≡ λθ. F (Iθ),

and their β- and η-rules are inter-provable. □

Exercise 14.13 The translation

[[x]] ≡ x  [[λx. p]] ≡ admit (λxψ. ψ[[p]])  [[fa]] ≡ focus (i[[f]][[a]])

embeds the (full) simply typed λ-calculus, where admit and i arise from the equaliser displayed in Theorem 3.22. Here x or a is the argument of the function X → Y and ψ : Σ^{Y} is the continuation after it. □

Remark 14.14 Where the operator admit asserts the universal property of the equaliser for “first class” maps Γ → X, its companion Admit says that this is still valid of “second class” maps F̂ : Γ −× X, i.e. arbitrary F : Σ^{X} → Σ^{Γ}.

Such maps have been used to study “control effects” in imperative programming languages. An important feature of their categorical structure is that the product × on S extends to singlevariable functors X×(−) and (−)×Y applicable to F̂ but not to a two-variable monoidal structure. (See the work cited in [A] for this.)

Coreflexive equalisers, on the other hand, do extend. Identifying equalisers with subspaces and therefore with predicates in a Floyd–Hoare logic, this may be related to the fact that such logics are valid for reasoning about imperative as well as functional programs. □

Whereas the previous three results may be interpreted in any category satisfying Axiom 14.7, the solution to the injectivity problem seems to proof-theoretic, relying on either syntax or the free model. What follows is therefore conjecture.

The monadic calculus has a normalisation theorem, in which i and admit (but not I) may essentially be erased [B, §§9–10], leaving terms of the underlying sober λ-calculus.

Definition 14.15 In the analogous result for the new subspace calculus, we first need to define the rank of a type (the depth of alternation of exponentials and equalisers), and so of the sub-terms of a term. By the erasure of a term Γ ⊢ a : X we then mean the same term, but erasing all occurrences of i, admit and Admit whose types are of higher rank than X or the types in Γ.

Lemma 14.16 Let U ≡ {X | f = g} ↣ X be an equaliser type, and

Γ, u : U, ψ : Σ^{U} ⊢ Sψu : Σ

a (raw) term that has no free variable or sub-term of higher rank than Σ^{U}. Then there is a term

Γ, x : X, ϕ : Σ^{X} ⊢ T ϕx : Σ such that Γ, u : U, ϕ : Σ^{X} ⊢ S(ϕ · i)u = T ϕ(iu) : Σ

and S and T have the same erasure, cf. Lemma 7.10. Proof Syntactic manipulation of a logically elementary kind, together with weak normalisation for the simply typed λ-calculus. Note, however, that Admit is used in the process of defining T. □

Theorem 14.17 Every term is provably equal to its erasure. □

This means that we can do mathematics (topology, analysis) in the category S, which has many of the properties of the category of sets, possibly using a proof-editor for verification, and then do computation simply by erasing the type information.

Corollary 14.18 Σ is injective in L. □

Corollary 14.19 If we add the “underlying set” axiom to the subspace calculus then Sob(E) ⊂ S as in Section 12. □

Remark 14.20 Exact injectivity — and, more importantly, consistency — of the calculus are much more difficult. The potential threat comes from the equality rule for Admit:

Γ, θ : Σ^{X×Y} ⊢ F (λx. θ(x, fx)) = F (λx. θ(x, gx)) Γ, x : X, fx = gx : Y ⊢ ϕx = ϕ′x
Γ ⊢ F ϕ = Admit F (Σ^{i}ϕ) = Admit F (Σ^{i}ϕ′) = F ϕ′ : Σ

A proof-theoretic attack on this (maybe similar to [7]) would seek to extract, from the proof of Γ, x : X, fx = gx : Y ⊢ ϕx = ϕ′x, a sequence of terms θ_{1}, …, θ_{2n} : Σ^{X×Y} that makes a “zig-zag” as shown:

Σ^{Y}  θ_{1}  θ_{2}  θ_{3}  ⋯  θ_{2n}

[figure: Σ^{f}; Σ^{g}; Σ^{g}; Σ^{f}; Σ^{f}; Σ^{g}; Σ^{g}; Σ^{f}]

Σ^{X} [figure: Σ^{f}; Σ^{g}] ϕ = Σ^{f}θ_{1}  Σ^{g}θ_{1} = Σ^{g}θ_{2} Σ^{f}θ_{2} = Σ^{f}θ_{3}  ⋯  Σ^{f}θ_{2n} = ϕ′

[figure: Σ^{i}; Σ^{i}; Σ^{i}; Σ^{i}]

[figure: Σ^{U}; Σ^{i}; ψ; Σ^{i}]

(Axiom 10.4 may require us instead to find an “infinite” family of θs, i.e. one parametrised by an “ordinal” or a “fixed point object”.)

Then there is already a proof of F ϕ = F ϕ′ without using Admit, which is therefore conservative. □

Corollary 14.21 If we add the “underlying set” axiom to the subspace calculus then L ≃ Loc(E) as in Section 12. □

References

[1] Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, editors. Séminaire de Géometrie Algébrique, IV: Théorie des Topos, number 269–270 in Lecture Notes in Mathematics. Springer-Verlag, 1964. Second edition, 1972.

[2] Michael Barr and Charles Wells. Toposes, Triples, and Theories. Number 278 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985.

[3] Andrej Bauer, Lars Birkedal, and Dana Scott. Equilogical spaces. Theoretical Computer Science, 315:35–59, 2004.

[4] Nicolas Bourbaki. Eléments de Mathématique XXII: Théories des Ensembles, Livre I, Structures. Number 1258 in Actualités scientifiques et industrielles. Hermann, 1957. English translation, “Theory of Sets,” 1968.

[5] Nicolas Bourbaki. Topologie Générale. Hermann, 1966. Chapter I, “Structures Topologiques”. English translation, “General Topology”, distrubuted by Springer-Verlag, 1989.

[6] Ronald Brown. Topology: a Geometric Account of General Topology, Homotopy Types and the Fundamental Groupoid. Mathematics and its Applications. Ellis Horwood, 1988. First edition “Elements of modern topology,” 1968.

[7] Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type checking in f_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[8] Brian Day. A reflection theorem for closed categories. Journal of Pure and Applied Algebra, 2:1–1, 1972.

[9] Brian Day and Max Kelly. On topological quotient maps preserved by pullbacks or products. Mathematical Proceedings of the Cambridge Philosophical Society, 67:553–8, 1970.

[10] Barry Fawcett and Richard Wood. Completely distributive lattices I. Mathematical Proceedings of the Cambridge Philosophical Society, 107:81–9, 1990.

[11] Ralph Fox. On topologies for function-spaces. Bulletin of the American Mathematical Society, 51:429– 32, 1945.

[12] Gerhard Gierz, Karl Heinrich Hoffmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, and Dana Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980. Second edition, Continuous Lattices and Domains, published by Cambridge University Press, 2003.

[13] Martin Hyland. Filter spaces and continuous functionals. Annals of Mathematical Logic, 16:101–143, 1979.

[14] Martin Hyland. Function spaces in the category of locales. In Bernhard Banachewski and Rudolf-Eberhard Hoffman, editors, Continuous Lattices, number 871 in LNM, pages 264–281. Springer-Verlag, 1981.

[15] John Isbell. Meet-continuous lattices. Symposia Math, 16:41–54, 1975.

[16] John Isbell. General function spaces, products and continuous lattices. Mathematical Proceedings of the Cambridge Philosophical Society, 100:193–205, 1986.

[17] Peter Johnstone. Topos Theory. Number 10 in London Mathematical Society Monographs. Academic Press, 1977.

[18] Peter Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[19] André Joyal and Ieke Moerdijk. Algebraic Set Theory. Number 220 in London Mathematical Society Lecture Notes in Mathematics. Cambridge University Press, 1995.

[20] André Joyal and Myles Tierney. An Extension of the Galois Theory of Grothendieck, volume 309 of Memoirs. American Mathematical Society, 1984.

[21] Joachim Lambek and Basil Rattray. Localizations and sheaf reflectors. Transactions of the American Mathematical Society, 210:279–293, 1975.

[22] Bill Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences of the United States of America, 52:1506–1511, 1964.

[23] Bill Lawvere. Quantifiers and sheaves. In Actes du Congrès International des Mathématiciens, volume 1, pages 329–334. Gauthier-Villars, 1971.

[24] Bill Lawvere. Comments on the development of topos theory. In Jean-Paul Pier, editor, Development of Mathematics, 1950–2000. Birkhäuser, 2000.

[25] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.

[26] Francisco Marmolejo, Robert Rosebrugh, and Richard Wood. A basic distributive law. Journal of Pure and Applied Algebra, 168:209–226, 2002.

[27] Christian Mikkelsen. Lattice-theoretic and Logical Aspects of Elementary Topoi. PhD thesis, Århus Universitet, 1976. Various publications, number 25.

[28] Susan Niefield. Cartesianness: Topological spaces, uniform spaces and affine varieties. Journal of Pure and Applied Algebra, 23:147–167, 1982.

[29] Robert Paré. Colimits in topoi. Bulletin of the American Mathematical Society, 80(3):556–561, May 1974.

[30] Giuseppe Rosolini. Continuity and Effectiveness in Topoi. D. Phil. thesis, University of Oxford, 1986.

[31] Giuseppe Rosolini. Equilogical spaces and filter spaces. Rend. Circ. Mat. Palermo Suppl., 64:157–175, 2000.

[32] Dana Scott. More on the axiom of extensionality. In Yehoshua Bar-Hillel, E. I. J. Poznanski, M. O. Rabin, and Abraham Robinson, editors, Essays of the Foundations of Mathematics, pages 115–139. Magnes Press, Hebrew University, 1966. Distributed by Oxford University Press.

[33] Dana Scott. Continuous lattices. In Bill Lawvere, editor, Toposes, Algebraic Geometry and Logic, number 274 in Lecture Notes in Mathematics, pages 97–137. Springer-Verlag, 1972.

[34] J. Arthur Seebach and Lynn Arthur Steen. Counterexamples in Topology. Holt, Rinehart and Winston, 1970. Republished by Springer-Verlag, 1978 and by Dover, 1995.

[35] Norman Steenrod. A convenient category of topological spaces. Michigan Mathematics Journal, 14:133–152, 1967.

[36] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[37] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[38] Steven Vickers. Topology Via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1988.

The papers on abstract Stone duality may be obtained from

                                 www.cs.man.ac.uk/∼pt/ASD

[A] Paul Taylor, Sober spaces and continuations. Theory and Applications of Categories, 10(12):248–299, 2002.

[B] Paul Taylor, Subspaces in abstract Stone duality. Theory and Applications of Categories, 10(13):300– 366, 2002.

[C] Paul Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284–338, 2000.

[D] Paul Taylor, Non-Artin gluing in recursion theory and lifting in abstract Stone duality. 2000.

[E] Paul Taylor, Inside every model of Abstract Stone Duality lies an Arithmetic Universe. Electronic Notes in Theoretical Computer Science 416, Elsevier, 2005.

[F] Paul Taylor, Scott domains in abstract Stone duality. March 2002. [G–] Paul Taylor, Local compactness and the Baire category theorem in abstract Stone duality. Electronic

Notes in Theoretical Computer Science 69, Elsevier, 2003.

[G] Paul Taylor, Computably based locally compact spaces. Logical Methods in Computer Science, 2005, to appear.

[H-] Paul Taylor, An elementary theory of the category of locally compact locales. APPSEM Workshop,

Nottingham, March 2003.

[I] Andrej Bauer and Paul Taylor, The Dedekind reals in abstract Stone duality. May 2005.

[J] Paul Taylor, A λ-calculus for real analysis. May 2005.

This research is currently supported by UK EPSRC project GR/S58522 (2003–6).

However, this funding was obtained in part on the basis of the earlier version of this paper [H-], which dealt with the minimal (locally compact) situation. This appeared in the proceedings of the APPSEM workshop in Nottingham on 26–28 March 2003.

The extension to sober spaces and locales was discovered between September and November 2004.

The original work was carried out in January to March 2003, during a period of unemployment, when I was supported entirely from my own savings. However, I would have been unable to do this without the companionship and emotional support of my partner, Richard Symes.