Geometric and Higher Order Logic in terms of Abstract Stone Duality

Paul Taylor

Abstract

The contravariant powerset and its generalisations Σ^{X} to the lattices of open subsets of a locally compact topological space and of recursively enumerable subsets of numbers satisfy the Euclidean principle that σ ∧ F (σ) ⇔ σ ∧ F (⊤).

Conversely, when the adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic, this equation implies that Σ classifies some class of monos and the Frobenius law ∃x.(ϕ(x) ∧ ψ) ⇔ (∃x.ϕ(x)) ∧ ψ for the existential quantifier.

In topology, the lattice duals of these equations also hold, and are related to the Phoa principle in synthetic domain theory.

The natural definitions of discrete and Hausdorff spaces correspond to equality and inequality, whilst the quantifiers considered as adjoints characterise open (or, as we call them, overt) and compact spaces. Our treatment of overt discrete spaces and open maps is precisely dual to that of compact Hausdorff spaces and proper maps.

The category of overt discrete spaces forms a pretopos. The paper concludes with a converse of Paré’s theorem (that the contravariant powerset functor is monadic) that characterises elementary toposes by means of the monadic and Euclidean properties together with all quantifiers, making no reference to subsets.

Contents  6 Discrete and Hausdorff objects  21
1 Introduction  1  7 Overt and compact objects  27
2 Support classifiers  4  8 The quantifiers  31
3 The Euclidean principle  9  9 Unions and coproducts  35
4 The origins of the Euclidean principle 15  10 Open discrete equivalence relations 37
5 The Phoa Principle  18  11 Monadicity for elementary toposes 42

Theory and Applications of Categories 7(15), 284–338, December 2000.

[11 April 2011: This was chronologically the first paper in the Abstract Stone Duality programme, which has this evolved quite considerably in the intervening years. This version therefore contains numerous annotations that explain how the ideas developed, or didn’t develop. The notation has been made to conform to that adopted in later work and minor corrections have been made without comment. However, significant comments and modifications are indicated by square brackets.]

1 Introduction

The powerset construction was the force behind set theory as Ernst Zermelo formulated it in 1908, but higher order logic became the poor relation of foundational studies owing to the emphasis on the completeness theorem in model theory. In this paper the powerset plays the leading role, and we derive the first order connectives from it in a novel way. The collection of all subsets is also treated in the same way as the collections of open and recursively enumerable subsets in topology and recursion theory. The underlying formulation in which we do this is a category with a “truth values” object Σ for which the adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic. Robert Paré proved in 1974 that any elementary topos has this property, whilst the category LKLoc of locally compact locales has it too (§O 5.10 and Theorem B 3.11^{1}). [B] explains how this is an abstraction of Stone duality.

Gerhard Gentzen’s natural deduction was the first principled treatment of the logical connectives, and Per Martin-Löf used the Curry–Howard isomorphism to extend it in a principled way to type constructors [ML84]. However, the natural conclusion of such an approach is to say that the existential quantifier is the same as the dependent sum, i.e. that a proof of ∃x. ϕ(x) must always provide a witness: a particular a for which ϕ(a) holds.

This conflicts with geometrical usage, in which we may say that the Möbius band has two edges, or a complex number two square roots, locally but not globally, i.e. there exists an isomorphism between 2 ≡ 1 + 1 and the set of edges or roots on some open subspace [Tay99, §2.4]. Similarly, interprovable propositions are, for Martin-Löf’s followers, isomorphic types, not equal ones, and their account of the powerset is a bureaucratic one: a structure within which to record the histories of formation and proof of the proposition–types [op. cit., §9.5].

The way in which category theory defines the powerset is not, perhaps, based so firmly on a logical creed as is Martin-Löf type theory, in that it describes provability rather than proof, but it was at least designed for the intuitions of geometry and symmetry. This notion — the subobject classifier in an elementary topos, which is readily generalised to the classifier Σ for open subsets (the Sierpiński space) and recursively enumerable ones — then obeys the curious equation

σ ∧ F (σ) ⇔ σ ∧ F (⊤) for all σ ∈ Σ and F : Σ → Σ,

which we call the Euclidean principle. The Frobenius law, which is part of the categorical formulation of the (geometrical) existential quantifier and was so called by Bill Lawvere, is an automatic corollary of the Euclidean principle. From this we develop the connectives of first order categorical logic, in particular stable effective quotients of equivalence relations.

Whilst set theory and topology have common historical roots [Hau14], the motivation for a common treatment of the kind that we envisage is Marshall Stone’s dictum that we should “always topologize” mathematical objects, even though they may have been introduced entirely in terms of discrete ideas [Joh82, Introduction]. For example, the automorphisms of the algebraic closure of ℚ form, not an infinite discrete (Galois) group, but a compact topological group. Similarly, the powerset of even a discrete set is not itself a discrete set, but a non-Hausdorff topological lattice. (Steven Vickers has taken the same motivation in a different direction [Vic98].)

The types in our logic are therefore to be spaces. The topological structure is an indissoluble part of what it is to be a space: it is not a set of points together with a topology, any more than chipboard (which is made of sawdust and glue) is wood.

When we bring (not necessarily Martin-Löf) type theory together with categorical logic [Tay99], logical notions such as the quantifiers acquire meanings in categories other than Set. In particular, with the internal lattice Σ^{X} in place of the powerset of X, the internal adjunctions ∃_{X} ⊣ Σ^{!} ⊣ ∀_{X}, where they exist, suggest interpretations of the quantifiers. We shall find that they obey the usual logical rules, but in the topological setting they also say that the space X is respectively overt (a word that we propose to replace one of the meanings of open) or compact.

It is well known that the recursively enumerable subsets of ℕ almost form a topology, since we may form finite intersections and certain infinitary unions of “open” subsets. However, the unification of topology with recursion theory, i.e. making precise Dana Scott’s thesis that continuity approximates the notion of computability, involves a revolutionary change, because the classical axiomatisation of (the frame of open subsets of) a topological space demands that we may form arbitrary unions.

1The letters denote the other papers in the ASD programme.

The usual procedure for turning a base (something, like this “topology” on ℕ, that partially satisfies the axioms for a topological space) into a topology would make every subset of ℕ open, losing all recursive information. In particular, in topology an open subspace is glued to its closed complement by means of a comma square construction that is due to Michael Artin, but this doesn’t work for recursively enumerable subsets and their complements [D, Section 4].

Although they are in many respects more constructive, the modern re-axiomatisations of topology in terms of open subsets — the theory of frames or locales [Joh82] that came out of topos theory [Joh77], and Giovanni Sambin’s formal topology [Sam87] motivated by Martin-Löf type theory — have exactly the same fault as Bourbaki’s [Bou66].

The finite meets and joins in the theory of frames present no problem, so what we need is a new way of handling the “purely infinitary” directed joins. Here we use an idea to which Scott’s name has become firmly attached (though it goes back to the Rice–Shapiro and Myhill–Shepherdson theorems of 1955), that directed joins define a topology. However, we turn this idea on its head: by treating frames, not as infinitary algebras over Set, but as finitary ones over Sp (i.e. as topological lattices, cf. topological groups) we can use topology in place of the troublesome directed joins, whenever they are genuinely needed. (Nevertheless, substantial re-working of general topology is needed to eliminate the use of interiors, Heyting implication, direct images, nuclei and injectivity.)

We do this by postulating that, for the category C of spaces, the adjunction

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

be monadic, i.e. C^{op} is equivalent to the category of Eilenberg–Moore algebras and homomorphisms over C. In practice, this is used in the form of Jon Beck’s theorem about U-split coequalisers. The way in which this expresses both Stone duality and the axiom of comprehension is explored in Sections B 1 and B 8. The concrete topological model of this situation is the category of locally compact spaces (or locales) and continuous maps.

But this category does not have all equalisers, pullbacks and coequalisers. The impact of this on logic is that we must also reconsider the notions of equality and inequality, which we define by saying that the diagonal subspace is respectively open or closed, i.e. that the space is discrete or Hausdorff .

[It will emerge later in the ASD programme that we cannot, after all, do without equalisers and pullbacks, especially when we consider recursion in [E, Section 2].]

Computational considerations also urge such a point of view. Two data structures may represent the same thing in some ethereal mathematical sense, for example in that they encode functions that produce the same result for every possible input value. However, as we are unable to test them against every input, such an equality may be outside our mortal grasp. A similar argument applies to inequality or distinguishing between the two data structures, in particular real numbers. Equality and inequality, therefore, are additional structure that a space may or may not possess.

Now that equality is no longer to be taken for granted as has traditionally been done in pure mathematics, there are repercussions for category theory. Specifically, Peter Freyd’s unification of products, kernels and projective limits into the single notion of limit in a category [Fre66b] breaks down, because the non-discrete types of diagram depend on equality. This entails a rootand-branch revision of categorical logic, which has traditionally relied very heavily on the universal availability of pullbacks. In fact, most of this work has already been done in categorical type theory [Tay99, Chapters VIII and IX].

The duality between equality and inequality (which also relates conjunction to disjunction and universal to existential quantification) is the characteristic feature of classical logic: for all its other merits, intuitionistic logic loses it. However, we find that it reappears in topology and recursion: for everything that we have to say in this paper about conjunction, equality, existential quantification, open subsets and overt spaces, we find exactly analogous results for disjunction, inequality, universal quantification, closed sets and compact spaces.

This symmetry is a constructive theorem (for LKLoc): as a result of Scott continuity, the Euclidean principle implies its lattice dual. Together with monotonicity (the finitary part of Scott continuity), the two Euclidean principles amount to the Phoa^{2} principle that has arisen in synthetic domain theory [Pho90a, Hyl91, Tay91]. These are also theorems in the free model of the other axioms. In view of their novelty and unusual form, connections to the Markov principle and several other things have deliberately been left as loose ends.

Whilst Scott continuity is obviously an important motivating principle, the Phoa principle alone has been enough to develop quite a lot of general topology, keeping the open–closed symmetry a precise one so far.

In particular we have a completely symmetrical treatment of open and proper maps, including the dual Frobenius law identified by Japie Vermeulen. Currently it only deals with inclusions and product projections, but the analogue and lattice dual of André Joyal and Myles Tierney’s “linear algebra” for locales [JT84] will be developed in future work.

The topics in general topology that we discuss in the body of the paper converge on a treatment of overt discrete spaces (classically, these are sets with the discrete topology), showing that they form a pretopos. That is, they admit cartesian products, disjoint unions, quotients of equivalence relations and relational algebra. [Assuming Scott continuity, they also admit free monoids and so form an arithmetic universe [E].]

The whole of the paper therefore concerns the logic of the category of sets, even though much of it is written in topological language: what we say about the subcategory of overt discrete spaces is immediately applicable to the whole category when this is Set or an elementary topos. In this sense, we have a new account of some of the early work on elementary toposes, in particular that they satisfy Jean Giraud’s axioms, i.e. that any topos is also what we now call a pretopos.

The distinction between topology and set theory turns out, therefore, to be measured by the strength of the quantifiers that they admit. The paper concludes with a new characterisation of elementary toposes that is based, like Paré’s theorem, on monadicity of the contravariant powerset, but which makes no reference whatever to subsets.

2 Support classifiers

We begin with the way in which powersets are defined in topos theory, i.e. using the subobject classifier (Section 11) and exponentials, but expressed in a slightly more flexible way. We may arrive at the same definitions from type-theoretic considerations [Tay99, §9.5]. But, whereas the uniqueness of the characteristic map ϕ is a moot point in that discipline, it is essential to this paper.

The subobject classifier was originally defined by Bill Lawvere in 1969, and the basic theory of elementary toposes was developed in collaboration with Myles Tierney during the following year [Law71, Law00]. Giuseppe Rosolini generalised the definition to classes of supports [Ros86] and developed a theory of partial maps, but the Frobenius law (Propositions 3.11, 8.2 and 10.13) is also required for relational algebra.

2This is an aspirated p, not an f. Wes Phoa told me that his name should be pronounced like the French word poire, i.e. pwahr, though maybe this is only helpful to the southern English and his fellow Australians as there is no final r.

Definition 2.1 A class M of morphisms (written ↪) of any category C, such that

(a) all isomorphisms are in M,

(b) all M-maps are mono, so i ∈ M must satisfy i ∘ a = i ∘ b ⇒ a = b,

(c) if i : X ↪ Y and j : Y ↪ Z are in M then so is j ∘ i, and

[figure: V; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; U; Y; f^{∗}i; \begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}; f; X; i; ∩]

(d) if i : U ↪ X is in M and f : Y → X is any map in C then the pullback f^{∗}i : V ↪ Y exists in C and belongs to M,

is called a class of supports or a dominion.

Definition 2.2 An M-map ⊤ : 1 → Σ is called a support classifier or a dominance (for M) if for every M-map i : U ↪ X there is a unique characteristic map ϕ : X → Σ making the square a pullback:

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

Set-theoretically, U is obtained from ϕ as {x : X | ϕ[x]} by the axiom of comprehension (separation or subset-selection), though we shall find the abbreviation [ϕ] ↪ X convenient here. Because of the topological intuition we call i : U ↪ X (the inclusion of) an open subset. (We shall write ⊏ for closed subsets and ↣ for Σ-split ones.)

Notice that this pullback is also an equaliser

[figure: U; ⊂; i; X; ⊤; ϕ; Σ.]

The relationship between the axiom of comprehension and the monadic ideas of this paper is explored in Section B 8, which also sets out the λ-calculus that we need in a more explicitly symbolic fashion.

Remark 2.3 This classification property deals only with a single subobject of (or predicate on) X, but in practice we need to consider Γ-indexed families of subobjects, or predicates containing parameters z⃗ whose types form the context Γ. These may equivalently be seen as binary relations Γ ↽ ⇀ X or as subobjects of Γ × X, which are classified by maps Γ × X → Σ. We would like these to be given by maps from Γ, i.e. by generalised elements of the internal object of maps X → Σ. Hence we want to use the exponential Σ^{X}. In Set, this is the same as the powerset P(X). To summarise, there is a correspondence amongst

iz⃗ : Uz⃗ ↪ X,  ϕz⃗[x],  ϕ : Γ × X → Σ  and  ϕ̃: Γ → Σ^{X} ≡ P(X)

where ϕ̃(z⃗) is the subset Uz⃗ for (z⃗) ∈ Γ.

Remark 2.4 We do not intend C to be cartesian closed, because this does not follow from our axioms and we want to use the category of locally compact spaces as an example. Recall that to say that the exponential Y^{X} exists in a category C (as a property of these objects individually) means that the functor C(− × X, Y) : C^{op} → Set is representable, i.e. it is naturally isomorphic to C(−, Z) for some object Z, which we rename Z ≡ Y^{X}. For this to be meaningful, all binary products Γ × X must first exist in C.

Notice that we ask for exponentials of the form Y^{X} for all X and fixed Y, whereas the word exponenti\underline{abilit}y refers to a property of a particular object X for arbitrary Y. Peter Freyd [FS90] has used the word baseable for the property that we require of Σ, but recognising the meaning of that word out of context depends on already knowing its association with exponents, whereas exponenti\underline{atin} g suggests its own meaning more readily. (The word exponent seems to have come from the French exposant [Bar88].)

Remark 2.5 We shall make use of the λ-calculus to define morphisms to and from exponentials such as these. However, since we are only assuming the existence of Σ^{X}, and not cartesian closure, the body of any λ-expression that we use must be of type Σ, or some other provably exponentiating object, such as a retract of Σ^{Y}. The range, i.e. the type of the bound variable, is arbitrary (cf. Definition 7.7).

[The restricted λ-calculus that we require, i.e. with just Σ^{Y} instead of general exponentials, is sketched in Section A 2.]

We leave it to the reader, making use of some account of λ-calculus and cartesian closed categories such as [Tay99, §4.7], to rewrite juxtapositions like ϕ(fy) categorically in terms of evaluation (ev : Σ^{X} × X → Σ), and λ-abstractions as adjoint transpositions. When we write x ∈ X, ϕ ∈ Σ^{X} etc., we mean generalised elements, i.e. C-morphisms x : Γ → X and ϕ : Γ → Σ^{X}, or expressions of type X or Σ^{X} involving parameters whose types form an unspecified context Γ; to make Γ explicit in our categorical expressions often involves forming products of various objects with Γ. On the other hand, when we write f : X → Y, it is sufficient for our purposes to regard this as a particular C-morphism, i.e. a global element of its hom-set, though in most cases parametrisation is possible by reading f as a morphism Γ × X → Y. At first we need to make the parametrising object explicit (calling it X), as we are considering a new logical principle, but from Section 6 it will slip into the background.

Symbolically, our λ-calculus is peculiar only in that there is a restriction on the applicability of the (→)-formation rule; such a calculus has been set out by Henk Barendregt [Bar92, §5.2], although this is vastly more complicated than we actually need here. We shall instead adopt a much simpler notational convention: lower case Greek letters, capital italics, Σ^{(−)} ≡ (−)^{∗} and the logical connectives and quantifiers denote terms of exponentiating type (predicates), whilst lower case italics denote terms of non-exponentiating type (individuals and functions). The capital italics could be thought of as “generalised quantifiers”.

The objects, unlike the morphisms, are never parametric in this paper (except in Proposition 5.4).

[We also refer to an equation between λ-terms as a statement.]

Remark 2.6 As exponentials are defined by a universal property, the assignment X ↦ Σ^{X} extends to a contravariant endofunctor, Σ^{(−)} : C → C^{op}. It takes f : Y → X to

Σ^{f} : Σ^{X} → Σ^{Y} by Σ^{f}(ϕ) ≡ ϕ ∘ f ≡ f ; ϕ ≡ λy. ϕ(fy).

The effect of Σ^{f} is to form the pullback or inverse image along f:

[figure: V; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; U; 1; Y; \begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}; f; X; ∩; ϕ; Σ; ⊤]

Remark 2.7 Returning to the powerset, we write Sub_{M}(X) for the collection of isomorphism classes of M-maps into X ∈ obC. Then Definition 2.2 says that the contravariant functor Sub_{M} : C^{op} → Set is representable, i.e. that it is naturally isomorphic to C(−, Σ) for some object Σ. As a special case of the conditions on M, the pullback (intersection) of any two M-maps into X exists, and the composite across the pullback square is in M, so Sub_{M}(X) is a semilattice. In fact, Sub_{M}(−) is a presheaf of semilattices on the category C, so C(−, Σ) is an internal semilattice in the topos of presheaves [Fre66a]. Since the Yoneda embedding is full and faithful and preserves products, Σ was already an internal semilattice in C.

It is well known that this argument makes unnecessary use of the category of sets, which it is the whole point of this paper to avoid (there are also size conditions on C), although we may suppose instead that C is an internal category in some pretopos. However, it is not difficult to disentangle this result from the sheaf theory and prove it directly instead. (The details of this proof would be a useful exercise in diagram-chasing for new students of category theory.)

Proposition 2.8 Any dominance Σ carries a ∧-semilattice structure, and pullback along {⊤} ↪ Σ induces an external semilattice isomorphism [ ] : C(X, Σ) → Sub_{M}(X).

[figure: Σ × Σ × Σ; id × ∧; Σ × Σ; Σ × Σ; tw; Σ × Σ]
[figure: ∧; ∧]
[figure: Σ × Σ; ∧ × id; ∧; Σ; ∧; Σ]
Σ × Σ  Σ
[figure: (⊤, id); (id, ⊤); Δ; id]
[figure: Σ; id; Σ; ∧; id; Σ; Σ × Σ; ∧; Σ]

Moreover, each Σ^{X} is an internal ∧-semilattice and each Σ^{f} is a semilattice homomorphism. (We shall consider the existence and preservation of joins in Section 9.)

[figure: 1; 1; 1; Σ; ⊤; ∩; Σ; ⊤; π_{1}; Σ × Σ; id × ⊤; ∩; ∧; Σ; ⊤; U ∩ V; ⊂; U; 1; 1; ∩; Σ; ψ; V; ∩; \underline{⊂}; X; ...........; .; .; .; .; .; .; .; .; .; .; ϕ ∧ ψ; Σ; ϕ; ∧; Σ; Σ × Σ]

Proof The fifth diagram defines ∧ as sequential and in terms of composition in M; manipulation of the pullbacks in the sixth establishes the relationship with intersection. By construing the monos {⟨⊤, ⊤⟩} ↪ Σ × Σ and {⟨⊤, ⊤, ⊤⟩} ↪ Σ × Σ × Σ as pullbacks in various ways, the semilattice laws follow from the uniqueness of their characteristic maps. These laws are expressed by the four commutative diagrams above involving products, i.e. Σ is an internal semilattice. Moreover, Σ^{X} is also an internal semilattice because the functor (−)^{X} (that is defined for powers of Σ and all maps between them) preserves products and these commutative diagrams. Similarly, Σ^{f} is a homomorphism because (−)^{f} is a natural transformation. □

Remark 2.9 In the next section we give a new characterisation of support classifiers as semilattices satisfying a further equation (the Euclidean principle), rather than by means of a class of supports. This characterisation depends on another hypothesis, that the adjunction

Σ^{(−)} ⊣ Σ^{(−)}

(which is defined for any exponentiating object Σ) be monadic. The way in which this hypothesis is an abstract form of Stone duality is explored in Examples B 1. In many cases the category C that first comes to mind does not have the monadic property, but [B] constructs the monadic completion \overline{C} of any category C with an exponentiating object Σ. In fact \overline{C} is the opposite of the category Alg of Eilenberg–Moore algebras for the monad.

Ultimately our interest is in developing some mathematics according to a new system of axioms, i.e. in the free model (Remark 3.8, Theorem 4.2), but first we introduce the concrete situations on which the intuitions are based. They and Example 4.5 also provide examples and counterexamples to gauge the force of the Euclidean and monadic principles. Even when C is not monadic, its properties are usually close enough to our requirements to throw light on the concepts, without shifting attention to the more complicated \overline{C}.

[In fact most of the results of this paper can be developed in the similar but alternative framework of equideductive logic, without the monadic principle [DD].]

Examples 2.10

(a) Let C be Set or any elementary topos, and Σ ≡ Ω its subobject classifier, which is an internal Heyting algebra; classically, it is the two-element set. So Σ^{X} ≡ P(X) is the powerset of X and M consists of all monos: 1–1 functions or (up to isomorphism) subset inclusions. All objects are compact, overt and discrete in the sense of Sections 6–8. Section 11 proves Paré’s theorem, that the adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic.

(b) Let C be any topos and Σ ≡ Ω_{j} be defined by some Lawvere–Tierney topology j, so M consists of the j-closed monos [LR75] [Joh77, Chapter 3] [BW85, §6.1]. The full subcategory E_{j} of j-sheaves is reflective in E, and the sheaves are the replete objects [BR98]. Restricted to E_{j}, the adjunction is monadic, and E_{j} is the monadic completion of E.

Examples 2.11

(a) Let Σ be the Sierpiński space, which, classically, has one open and one closed point; the open point classifies the class M of open inclusions. Then the lattice of open subsets of any topological space X, itself equipped with the Scott topology, has the universal property of the exponential Σ^{X} so long as we restrict attention to the category C of locally compact sober spaces (LKSp) or locales (LKLoc) and continuous maps [Joh82, §VII 4.7ff]. In this case the topology is a continuous lattice [GHK^{+}80]. A function between such lattices is a morphism in the category, i.e. it is continuous with respect to this (Scott) topology, iff it preserves directed joins [Joh82, Proposition II 1.10].

With excluded middle, all objects are overt, but (unlike Set) LKSp and LKLoc are not cartesian closed, complete or cocomplete. For LKLoc, the adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic (§O 5.10 and Theorem B 3.11), as it is for LKSp, assuming the axiom of choice.

(b) Let C be the category Cont of continuous lattices and functions that preserve directed joins, and Σ be the Sierpiński space; then Σ^{X} is the lattice of Scott-open subsets of X. In this case Σ^{(−)} is not monadic, but LKLoc is its monadic completion (\overline{C}). As Cont is cartesian closed but LKLoc is not, this shows that the construction of \overline{C} from C in Section B 4 does not preserve cartesian closure. For trivial reasons, all objects of Cont are overt and compact.

(c) In these examples we may instead take M to be the class of inclusions of closed subsets, except that now the closed point ⊥ of the Sierpiński space performs the role of ⊤ in Definition 2.2 (Corollary 5.5ff).

It is by regarding (locally compact) frames as finitary algebras over the category of spaces (in which directed joins are “part of the wallpaper”), rather than as infinitary ones over the category of sets, that we achieve complete open–closed duality for the ideas discussed in this paper.

Examples 2.12

(a) Let C be Pos and Σ ≡ Υ ≡ Ω be the subobject classifier (regarded classically as the poset ⊥ ⩽ ⊤), so Υ^{X} is the lattice of upper sets, cf. the notation for the Alexandroff topology in [Joh82, §II 1.8]. The category C is cartesian closed and has equalisers and coequalisers. Although C → \overline{C} is (classically) full and faithful, the real unit interval [0, 1] is an algebra that is not the lattice of upper sets of any poset [FW90, Example 9], see also Example B 3.12.

(b) The algebras for the monad are completely distributive lattices, but the intuitionistic definition of the latter is itself a research issue [FW90], so we assume excluded middle in our discussion of this example. Nevertheless, Francisco Marmolejo, Robert Rosebrugh and Richard Wood have shown that the opposite of the category of constructively completely distributive lattices is monadic [MRW02]. Classically, this category is equivalent to the category of continuous dcpos and essential Scott-continuous maps, i.e. those for which the inverse image preserves arbitrary meets as well as joins [Joh82, §VII.2]. All objects are overt and compact, whilst Set is embedded as the full subcategory of discrete objects (Example 6.14).

In any given category, there may be many classes M of supports, each class possibly being classified by some object Σ_{M}.

Remark 2.13 Many of the ideas in this paper evolved from synthetic domain theory, a model of which is a topos (with a classifier Ω for all monos) that also has a classifier Σ for recursively enumerable subsets [Ros86, Pho90a, Pho90b, Hyl91, Tay91, FR97, BR98]. In this case, Σ is a subsemilattice of Ω. Such models exist wherein the full subcategory of replete objects satisfies the monadicity property discussed in this paper for Σ [Theorem I 15.10], in addition to that for the whole category for Ω [RT98].

3 The Euclidean principle

We now give a new characterisation of dominances in terms of the object Σ (and its powers) alone, without any reference to subsets. These are supplied by the monadic assumption, which therefore somehow plays the role of the axiom of comprehension. [This role is formalised in Section B 8.]

Proposition 3.1 In any dominance Σ, the Euclidean principle

ϕ(x) ∧ F (x, ϕ(x)) ⟺ ϕ(x) ∧ F (x, ⊤)

holds for all ϕ : X → Σ and F : X × Σ → Σ.

[figure: [ϕ] ∩ [F ⊤]; ⊂; [F ⊤]; 1]

[figure: [ϕ]; ∩; ⊂; X; ∩; (id, ⊤); (id, ϕ); X × Σ; F; Σ; ⊤; ∩]

[figure: ≅; [ϕ] ∩ [F ϕ]; ∪; ⊂; [F ϕ]; ∪; 1; ⊤_{∪}]

Proof The composites [ϕ] ↪ X ⇉ X × Σ → Σ are equal by the construction of [ϕ] ↪ X, so their pullbacks [ϕ]∩[F ⊤] and [ϕ]∩[F ϕ] along ⊤ are isomorphic, i.e. equal as subobjects of [ϕ], and so of X. Since [ ] : C(X, Σ) → Sub_{M}(X) preserves ∩, these subobjects are [ϕ ∧ F ⊤] and [ϕ ∧ F ϕ] respectively. But then, by the uniqueness of the characteristic map, the equation holds. □

Another construction that we can do with a dominance will turn out to be the existential quantifier. [For this reason the letter E was used for it in the published version of this section, but this has been changed to I here because of the convention that was adopted later in the ASD programme of using E for a nucleus.]

Lemma 3.2 Using Definition 2.2, let i : U ↪ X be the mono classified by ϕ : X → Σ. Then the idempotent (−) ∧ ϕ on Σ^{X} splits into a homomorphism Σ^{i} and another map I : Σ^{U} ↣ Σ^{X} with Σ^{i} · I = id_{Σ^{U}} and I · Σ^{i} = (−) ∧ ϕ : Σ^{X} → Σ^{X}.

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

[figure: U × Σ^{X}; ∩; id × Σ^{i}; U × Σ^{U}; ∩; ev_{U}; Σ; ⊤]

[figure: id]

[figure: X × Σ^{X}; i × id; ∩; id × Σ^{i}; X × Σ^{U}; i × id; ∩; Ĩ; Σ; ⊤]

Proof Let V and W be the middle and left pullbacks in the top row, and let Ĩ be the classifying map for V ↪ X × Σ^{U}, so the big square is also a pullback.

Now consider how V ↪ U × Σ^{U} is classified by maps targeted at the lower right corner. One classifier is id ∘ ev_{U}. However, whilst V was defined as the pullback of Ĩ against ⊤, it is also the pullback of the composite Ĩ ∘ (i × id) against ⊤, where the relevant triangle commutes because i × id is mono. Hence Ĩ∘ (i × id) also classifies V. By uniqueness, the trapezium commutes, and the exponential transposes are Σ^{i} · I = id.

The composite along the bottom is the transpose of I · Σ^{i}. The lower left square is a pullback, so the whole diagram is a pullback and W is {(x, ψ) ∈ X × Σ^{X} | I(Σ^{i}ψ)(x)}. However, using the smaller pullback rectangle, it is {(x, ψ) | x ∈ U ∧ ψ(x)}, where (x ∈ U) means ϕ(x). Again by uniqueness of (pullbacks and) the classifier, these are equal, so I · Σ^{i} = (−) ∧ ϕ. □

The significance of the Euclidean principle and the map I is that they provide an example of the condition in the theorem of Jon Beck that characterises up to equivalence the adjunction between the free algebra and underlying set functors for the category of algebras of a monad [Mac71, §IV 7] [BW85, §3.3] [Tay99, §7.5]. Although the public objective of the theory of monads is as a way of handling infinitary algebra, this condition will turn out to be more important in Abstract Stone Duality than the notion of algebra.

Lemma 3.3 Let Σ be an exponentiating semilattice that satisfies the Euclidean principle (i.e. the conclusion of Proposition 3.1). Then the parallel pair (u, v) in the middle of that diagram,

[figure: U ≡ [ϕ]; ⊂; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; i; X; ⊂; u : x ↦ ⟨x, ⊤⟩; v : x ↦ ⟨x, ϕ(x)⟩; X × Σ; Σ^{U}; .; .; .; .; .; .; .; .; .; .; .; ^{Σ^{i} ...............}; ⊤; .; .; .; .; .; .; .; .; .; .; .; .; .; .; I; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{X}; J : ψ ↦ λxσ. σ ∧ ψx; Σ^{X×Σ}]

is Σ-split in the sense that there is a map J as shown such that

(Jψ)(ux) ⇔ ψ(x)  and  J(F ∘ u)(vx) ⇔ J(F ∘ v)(vx)

for all x ∈ X, ψ ∈ Σ^{X} and F ∈ Σ^{X×Σ}. (We just mark u with a hook as a reminder that these equations are not symmetrical in u and v.) Proof For ψ ∈ Σ^{X}, we have (Jψ)(ux) ⇔ ⊤ ∧ ψ(x) ⇔ ψ(x) and (Jψ)(vx) ⇔ ϕ(x) ∧ ψ(x). Hence J(F ∘ u)(vx) ⇔ ϕ(x) ∧ F (x, ⊤) and J(F ∘ v)(vx) ⇔ ϕ(x) ∧ F (x, ϕ(x)), which are equal by the Euclidean principle. □

Remark 3.4 The map I defined in Lemma 3.2 is the fifth one needed (together with Σ^{u} and Σ^{v}) to make the lower diagram in Lemma 3.3 a split coequaliser.

id_{Σ^{U}} = Σ^{i} · I I · Σ^{i} = (−) ∧ ϕ = Σ^{v} · J.

[The term E ≡ I · Σ^{i} ≡ λψ. ψ ∧ ϕ is a nucleus (Definition B 4.3 and §O 8.3):

E(λx. F(λψ. ψx)) = λx. ϕx ∧ F(λψ. ψx)
= λx. ϕx ∧ F(λψ. ψx ∧ ϕx)
= E(λx. F(λψ. ψx))

using the Euclidean principle with σ ≡ ϕx. Then

U ≡ {X | E}  and  x ∈ U ⊣⊢ ϕx ⇔ ⊤ ⊣⊢ ∀ψ. Eψx ⇔ ψx

in the notation of Section B 8.] □

Remark 3.5 Since Σ is a semilattice, it carries an internal order relation. Some morphisms are monotone with respect to this order, but others may not be. The order also extends pointwise to an order on morphisms between (retracts of) powers of Σ. We shall discuss monotonicity, and some other ways of defining order relations, in Section 5.

The order also allows us to talk of such morphisms as being adjoint, L ⊣ R.

When the definition of adjunction is formulated as the solution of a universal property, the adjoint is automatically a functor. However, the definition that is most useful to us is the one that uses the internal order relation and the structure of the category directly, namely

id ⩽ R · L L · R ⩽ id,

which does not itself force L and R to be monotone. So we say so, even though we have no intention of considering non-monotone adjunctions. This point is significant in Lemma 3.7 in particular. To repeat Proposition 2.8,

Lemma 3.6 For any object Z, the functor (−)^{Z} (defined on the full subcategory of retracts of powers of an exponentiating semilattice Σ) preserves the semilattice structure, and hence the order (i.e. it is monotone or order-enriched) and adjointness (L^{Z} ⊣ R^{Z}). □

Lemma 3.7 Let P : A → S be a homomorphism between internal semilattices and I : S → A another morphism such that id_{S} = P · I. Then the following are equivalent:

(a) I · P = (−) ∧ ϕ for some ϕ : 1 → A;

(b) I is monotone and satisfies the Frobenius law,

I(θ) ∧ ψ = I(θ ∧ P ψ) for all θ ∈ S, ψ ∈ A;

(c) [P and I define an isomorphism A ≅ S ↓ ϕ ≡ {ψ : S | ψ ⩽ ϕ}.] In this case, I preserves binary ∧, so it is monotone, and I ⊣ P. Since the [order relation ⩽ derived from a semilattice structure is] antisymmetric [i.e. ϕ ⩽ ψ, ψ ⩽ ϕ ⊢ ϕ = ψ], adjoints are unique, so each of P, I and ϕ uniquely determines the other two. (See Definition 10.4 for when I preserves ⊤.) Proof [a⇒b] I(θ) ∧ ψ = I · P · I(θ) ∧ ψ = (Iθ ∧ ϕ) ∧ ψ, whilst

I(θ ∧ P ψ) = I(P · I(θ) ∧ P ψ) = I · P (I(θ) ∧ ψ) = (Iθ ∧ ψ) ∧ ϕ

since P preserves ∧.

[a⇐b] I · P (ψ) = I(⊤ ∧ P ψ) = I(⊤) ∧ ψ, so ϕ = I(⊤).

In particular, I(θ_{1}) ∧ I(θ_{2}) = I(θ_{1} ∧ P · I(θ_{2})) = I(θ_{1} ∧ θ_{2}). Finally, I ⊣ P because id_{S} ⩽ P · I and I · P ⩽ id_{A}. □

Now we apply the monadic property to logic for the first time.

Remark 3.8 Instead of taking the class M of monos as fundamental, from now on we shall assume that

(a) the category C has finite products and splittings of idempotents;

(b) Σ is an exponentiating object;

(c) the adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic;

(d) (Σ, ⊤, ∧) is an internal semilattice and

(e) it satisfies the Euclidean principle.

Lemma 3.9 With the assumptions in Remark 3.8, let ϕ : X → Σ in C. Then

(a) the pullback i : U ↪ X of ⊤ : 1 → Σ against ϕ exists in C;

(b) there is a map I : Σ^{U} → Σ^{X} such that id_{Σ^{U}} = Σ^{i} · I and I · Σ^{i} = (−) ∧ ϕ : Σ^{X} → Σ^{X};

(c) the classifying map ϕ : X → Σ is uniquely determined by i;

(d) if j : V ↪ U is also open then so is the composite V ↪ U ↪ X.

So we have a class M of monos with an exponentiating classifier Σ, as in Section 2.

V  \overline{}1

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

.............. I(ψ)

[figure: Σ; ⊤; ∩; ϕ; X; ∩]

Proof The pullback is given by an equaliser; Lemma 3.3 shows that this pair is Σ-split, using the Euclidean principle, so the equaliser exists by Beck’s theorem, and the contravariant functor Σ^{(−)} takes it to the (split) coequaliser. Thus the idempotent (−)∧ϕ on Σ^{X} splits into a homomorphism Σ^{i} : Σ^{X} ↠ Σ^{U} and a map I, satisfying the equations above. By Lemma 3.7, I ⊣ Σ^{i} and the characteristic map ϕ ≡ I(⊤) is unique. Finally, if V is classified by ψ : U → Σ then the composite i ∘ j is classified by I(ψ). [See §O 8.4 for a more detailed proof of (d).] □

Theorem 3.10 Let (C, Σ) satisfy the first four axioms in Remark 3.8. Then

(a) ⊤ : 1 → Σ is a dominance (where M is the class of pullbacks of this map and ∧ is given by Proposition 2.8) iff

(b) (Σ, ⊤, ∧) satisfies the Euclidean principle. In this case, a mono i is classified (open) iff there is some map I that satisfies id = Σ^{i} · I and the Frobenius law. Proof [More explanation of how the Euclidean principle entails uniqueness of classifiers is needed. This is trivial in the case of ⊤ since the square

[figure: V; 1; U; ≅; ∩; ψ; Σ; ⊤]

is only a pullback (indeed, commutes) when ψ = ⊤. More generally, if ϕ, ψ : X ⇉ Σ have the same pullback U then so does ϕ ∧ ψ (cf. Proposition 2.8), so without loss of generality ψ ⩽ ϕ. Using the foregoing argument, this situation transfers from X to U. The role of the Euclidean principle, or more precisely the Frobenius law, is to make Σ^{U} ≅ Σ^{X} ↓ ϕ (Lemma 3.7). The external form of this relationship is the top row of the diagram

[figure: C(U, Σ); ≅; \underline{(−) · i}; C(X, Σ) ↓ ϕ; \underline{(−) ∧ ϕ}; C(X, Σ)]

[figure: Sub(U); pullback; = = = = = = = = =; \{V ∈ Sub(X) | V ⊂ U\}; pullback; \underline{(−) ∩ U}; Sub(X); pullback]

in which the bottom row says the same thing for (open) subspaces, using the fact that open inclusions compose (Lemma 3.9(d)). We also know that the diagram commutes in the obvious ways. Hence if ψ ⩽ ϕ : X ⇉ Σ both classify U then ψ factors through U → Σ and as such it classifies the same open subspace of U as ⊤ does, namely U itself, so ψ = ⊤ : U ⇉ Σ, Since C(U, Σ) ≅ C(X, Σ) ↓ ϕ we have ψ = ϕ : X ⇉ Σ.] □

This result partly answers a criticism of [Tay91], that it did not ask for a dominance, since the Euclidean principle is a part of the Phoa principle (Proposition 5.7), although monadicity was not considered there.

It does not seem to be possible, in general, to deduce id = Σ^{i} · I from the simpler condition that i be mono (with I ⊣ Σ^{i}), but see Corollary 10.3 when the objects are overt and discrete.

The next result justifies the name ∃_{i} for I [Tay99, §9.3], although it only allows quantification along an open inclusion: we consider the more usual quantifier ranging over a type in Sections 7–8.

Proposition 3.11 For i : U ↪ X open, Σ^{i} and ∃_{i} satisfy

(a) the Frobenius law

∃_{i}(θ) ∧ ψ = ∃_{i}(θ ∧ Σ^{i}ψ)

for any θ ∈ Σ^{U} and ψ ∈ Σ^{X}, and

(b) the Beck–Chevalley condition

[figure: V; g; U; 1; Σ^{V}; Σ^{g}; Σ^{U}∋ θ]

?

[figure: Y; j; ∩; f; X; i; ∩; ϕ; Σ; ⊤; Σ^{Y}; ∃_{j}; Σ^{f}; Σ^{X}; ∃_{i}]

for any map f : Y → X in C, i.e. that if the square consisting of g, i, f and j is a pullback then that on the right commutes.

Proof [a] Lemma 3.7. [b] Put ω ≡ ∃_{i}(θ), so θ = Σ^{i}(ω) and ω = ∃_{i}Σ^{i}ω = ω ∧ ϕ. Then ∃_{j}Σ^{g}θ = ∃_{j}Σ^{g}Σ^{i}ω = ∃_{j}Σ^{j}(Σ^{f}ω) = Σ^{f}ω ∧ (ϕ ∘ f) = Σ^{f}(ω ∧ ϕ) = Σ^{f}ω = Σ^{f}∃_{i}θ since ϕ ∘ f classifies j : V ↪ Y. □

Remark 3.12 Consider the pullback (intersection) U ∩ V ⊂ X of two open subsets.

X  Σ^{X}
[figure]
U  V  Σ^{U}  Σ^{V}
[figure]
U ∩ V  Σ^{U∩V}

In the diagram on the right, the monos are existential quantifiers and the epis are inverse images, which are adjoint and split. The Beck–Chevalley condition for this pullback says that the squares from Σ^{U} to Σ^{V} and vice versa commute. These equations make the square of existential quantifiers an absolute pullback, i.e. it remains a pullback when any functor is applied to it, and similarly the square of inverse image maps an absolute pushout [Tay99, Exercise 5.3]. □

Remark 3.13 The Euclidean equation can be resolved into inequalities

σ ∧ F (ψ) ⟹ F (σ ∧ ψ) σ ∧ F (σ ∧ ψ) ⟹ F (ψ)

for all σ ∈ Σ, F : Σ^{Y} → Σ^{X} and ψ ∈ Σ^{Y}. The first says that F is strong, and the second is a similar property for order-reversing functions. At the categorical level, the contravariant functor Σ^{(−)} also has such a co-strength, X × Σ^{X×Y} → Σ^{Y}, given by (x, ω) ↦ λy. ω(x, y). □

4 The origins of the Euclidean principle

This characterisation of the powerset offers us a radically new attitude to the foundations of set theory: the notion of subset is a phenomenon in the macroscopic world that is a consequence of a purely algebraic (“microscopic”) principle, and is made manifest to us via the monadic assumption. Taking this point of view, where does the Euclidean principle itself come from?

Remark 4.1 The name was chosen to be provocative. The reason for it is not the geometry but the number theory in Euclid’s Elements, Book VII: with f, n ∈ Σ ≡ ℕ, ⊤ ≡ 0 and ∧ ≡ hcf, we have a single step of the Euclidean algorithm,

hcf(n, (f + n)) = hcf(n, (f + 0)).

In fact, hcf(F (n), n) = hcf(F (0), n) for any polynomial F : ℕ → ℕ, since F (n) − F (0) = n × G(n) for some polynomial G. I do not know what connection, if any, this means that there is between higher order logic and number theory; the generalisation is not direct because ring homomorphisms need not preserve hcf, whereas lattice homomorphisms do preserve meets.

The way in which the Euclidean principle (and the Phoa principle in the next section) express F (σ) in terms of F (⊥) and F (⊤) is like a polynomial or power series (Taylor) expansion, except that it only has terms of degree 0 and 1 in σ, ∧ being idempotent. These principles may perhaps have a further generalisation, of which the Kock–Lawvere axiom in synthetic differential geometry [Koc81] would be another example. Of course, if ∧ is replaced by a non-idempotent multiplication in Σ^{X} then the connection to the powerset is lost.

The Euclidean algorithm may be stated for any commutative ring, but it is by no means true of them all. But it is a theorem for the free (polynomial) ring in one variable, and we have similar results in logic, where Σ^{Σ} is the free algebra (for the monad) on one generator. [See also the discussion in §O 7.7.]

Post-Publication Note. The following is only valid for terms whose free variables are of type ℕ or Σ^{ℕ}. In particular, F cannot be a free variable.

Theorem 4.2 The Euclidean principle holds in the free model of the other axioms in Remark 3.8. Proof There is a standard way of expressing the free category with certain structure (including finite products) as a λ-calculus (with cut and weakening), in which the objects of the category are contexts, rather than types [Tay99, Chapter IV]. In our case, C has an exponentiating internal semilattice, and the calculus is the simply typed λ-calculus restricted as in Remark 2.5, together with the semilattice equations. The calculus gives the free category because the interpretation or denotation functor ⟦−⟧ : C → D is the unique structure-preserving functor to any other category of the same kind.

The free category \overline{C} in which the adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic will be constructed (and given its own λ-calculus) in Section B 4, from which (for the present purposes) we only need to know that C(−, Σ^{Σ}) ≅ \overline{C}(−, Σ^{Σ}).

So we just have to show that ϕ ∧ F (ϕ ∧ ψ) ⇔ ϕ ∧ F (ψ) for all ϕ, ψ ∈ Σ, by structural induction on F ∈ Σ^{Σ} in the appropriate λ-calculus, considering the cases where F (σ) is

(a) ⊤ or another variable τ: trivial;

(b) σ itself: by associativity and idempotence of ∧;

(c) Gσ ∧ Hσ: by associativity, commutativity and the induction hypothesis;

(d) λx. G(σ, x): using ϕ ∧ λx. G(x, σ) = λx. (ϕ ∧ G(x, σ)) and the induction hypothesis;

(e) G(H(σ), σ): put ψ′ ≡ Hψ and ψ′′ ≡ H(ϕ ∧ ψ), so

ϕ ∧ ψ′ ≡ ϕ ∧ Hψ ⇔ ϕ ∧ H(ϕ ∧ ψ) ≡ ϕ ∧ ψ′′

by the induction hypothesis for H, and

ϕ ∧ G(Hψ, ψ) ≡ ϕ ∧ G(ψ′, ψ)
⇔ ϕ ∧ G(ϕ ∧ ψ′, ϕ ∧ ψ)
⇔ ϕ ∧ G(ϕ ∧ ψ′′, ϕ ∧ ψ)
⇔ ϕ ∧ G(ψ′′, ϕ ∧ ψ)
≡ ϕ ∧ G(H(ϕ ∧ ψ), ϕ ∧ ψ)

by the induction hypothesis for (each argument of) G. □

Remark 4.3 The result remains true for further logical structure, because of generalised distributivity laws:

(a) ∨ and ⊥, assuming the (ordinary) distributive law;

(b) ⇒, by an easy exercise in natural deduction;

(c) ∃, assuming the Frobenius law;

(d) ∀, since it commutes with ϕ ∧ (−);

(e) ℕ, since ϕ ∧ rec(n, G(n), λmτ. H(n, m, τ)) ⇔ rec(n, ϕ ∧ G(n), λmτ. ϕ ∧ H(n, m, τ));

(f) =_{ℕ} and ≠_{ℕ}, since these are independent of the logical variable;

(g) Scott continuity, as this is just an extra equation (Remark 7.11) on the free structure, but Corollary 5.5 proves the dual Euclidean principle more directly in this case. □

Remark 4.4 Todd Wilson identified similar equations to the Euclidean principle in his study of the universal algebra of frames [Wil94, Chapter 3], in particular his Proposition 9.6(b) and Remark 9.24, although the fact that frames are also Heyting algebras is essential to his treatment.

[Some other similar results are also known about maps F : Ω → Ω:

(a) Denis Higgs, quoted in [Joh77, Exercise I.33], showed that if F is mono (but need not preserve order) then F^{2} = id_{Ω};

(b) Jean Bénabou, quoted in [Woo04, §4.1], showed that if F ⩽ id then F σ ⇔ σ ∧ F ⊤. See also the discussion in §O 7.7. Besides these, Anna Bucalo, Carsten Fürhmann and Alex Simpson [BFS03] investigated an equation similar to the Euclidean principle that is obeyed by the lifting monad (−)_{⊥}.]

Example 4.5 So-called stable domains (not to be confused with the stability of properties under pullback that we shall discuss later) provide an example of a dominance that is instructive because many of the properties of Set and LKSp fail. Although the link and specialisation orders (Definition 5.9) coincide with the concrete one, they are sparser than the semilattice order. All maps Σ → Σ are monotone with respect to the semilattice order, but not all those Σ^{Σ} → Σ. The object Σ is not an internal lattice, so there is no Phoa or dual Euclidean principle.

The characteristic feature of stable domains is that they have (and stable functions preserve) pullbacks, i.e. meets of pairs that are bounded above. Pullbacks arise in products of domains from any pair of instances of the order relation, for example

(⊥, ⊤) ⩽ (⊤, ⊤)  (f′, x) ⩽ (f, x)
∨/  ∨/  ∨/  ∨/
(⊥, ⊥) ⩽ (⊤, ⊥)  (f′, x′) ⩽ (f, x′)

in Σ × Σ and in Y^{X} × X for any f′ ⩽ f in Y^{X} and x′ ⩽ x in X. The first example says that there is no stable function Σ × Σ → Σ that restricts to the truth table for ∨. The second means that, for the evaluation map ev : Y^{X} × X → Y to be stable,

f′ ⩽ f implies ∀x′, x. x′ ⩽ x ⇒ f′(x′) = f′(x) ∧ f(x′).

In fact f′ ⩽ f is given exactly by this formula, which is known as the Berry order, since (using the universal property that defines Y^{X}) the function {⊥ ⩽ ⊤} × X → Y defined by (⊥, x) ↦ f′x and (⊤, x) ↦ fx is stable iff the formula holds.

Stable domains were introduced by Gérard Berry [Ber78], as a first attempt to capture sequential algorithms denotationally: parallel or, with por(t, ⊥) ≡ por(⊥, t) ≡ t and por(f, f) ≡ f, is not interpretable, as it is in Dcpo. Notice that the Berry order is sparser than the pointwise order on the function-space; it bears some resemblance to the Euclidean principle, but I cannot see what the formal connection might be here, or with Berry’s domains that carry two different order relations.

In order that they may be used like Scott domains for recursion, stable domains must have, and their functions preserve, directed joins with respect to the Berry order. Some models also require infinitary (wide) pullbacks [Tay90], i.e. binary ones and codirected meets. The literature is ambiguous on this point (some, such as [FR97], require only the binary form), because there are also models satisfying Berry’s “I” condition, that there be only finitely many elements below any compact element, so there are no non-trivial codirected meets to preserve. Berry and other authors also required distributivity of binary meets over binary joins (the “d” condition, hence dI-domains) in order to ensure that function-spaces have ordinary joins of bounded sets, rather than multijoins.

From the point of view of illustrating dominances, it is useful to assume that stable functions do preserve infinitary pullbacks, and therefore meets of all connected subsets. Then if U ⊂ X is connected and classified by ϕ : X → Σ, we may form u ≡ ⋀ U ∈ X, and, by stability of ϕ, u belongs to U, so U is the principal upper set ↑ u. Removing the connectedness requirement, Achim Jung and I picturesquely called the classified subsets (disjoint unions of principal upper subsets) icicles.

The exponential Σ^{Σ} is a V-shape in the Berry order. The identity and λx. ⊤ are incomparable: if there were a link Σ → Σ^{Σ} between them, its exponential transpose would be ∨ : Σ × Σ → Σ.

[figure: id ≡ λx. x; λx. ⊤]
[figure]
F^{−1}(⊤)

⊥ ≡ λx. ⊥

On the other hand, there is a morphism F : Σ^{Σ} → Σ for which F (λx. ⊤) ≡ ⊥ and F (id) ≡ ⊤, shown as the icicle F^{−1}(⊤) above. This control operator detects whether ϕ ∈ Σ^{Σ} reads its argument; in a generalised form, it is called catch, by analogy with the handling of exceptions, which are thrown. When ϕ is processed sequentially, there must be a first thing that it does: it either reads its input, or outputs a value irrespectively of the input.

Nevertheless, Σ^{Σ} is still an internal semilattice, carrying the pointwise semilattice order, for which id ⩽ (λx. ⊤) and F is not monotone. I have not worked out the monadic completion \overline{C} of the category of stable domains, but it would be interesting to know what this looks like. We consider the stable example again in Remark 9.3.

5 The Phoa Principle

Remark 5.1 Consider the lattice dual of the Euclidean principle,

σ ∨ F (σ) ⟺ σ ∨ F (⊥),

where we suppress the parameter x ∈ X to σ ∈ Σ^{X} and F ∈ Σ^{X×Σ}. Taking F to be ¬¬ in Set or Pos, this yields excluded middle (¬¬σ ⇔ σ). Observe that the Euclidean principle and its dual are trivial for σ ≡ ⊤ and σ ≡ ⊥, and therefore for the classical case Σ ≡ {⊥, ⊤}. □

In topology and recursion, C-morphisms of the form F : Σ^{Y} → Σ^{X} preserve directed joins with respect to the semilattice order: they are said to be Scott-continuous (cf. Examples 2.11).

This completely changes the constructive status of the dual Euclidean principle.

The results about open subsets and maps and overt objects that we present later in the paper then have closed, proper or compact mirror images. Note that Scott-continuity of ¬¬ would imply excluded middle.

More basically, any F : Σ^{Y} → Σ^{X} is monotone (Remark 3.5) in Pos as well as in topology and recursion, but not in Set. Even though we intend to consider (locally compact) topological spaces X in general, we need only use lattice or domain theory to study Σ^{X}, since this is just the lattice of open subsets of X, equipped with a topology that is entirely determined by the (inclusion) order.

Lemma 5.2 For any exponentiating semilattice Σ, the functor Σ^{(−)} is order-enriched iff all functions Σ^{Y} → Σ^{X} are monotone, but then it is contravariant with respect to the order: if F ⩽ G then Σ^{G} ⩽ Σ^{F}, and if L ⊣ R then Σ^{R} ⊣ Σ^{L}. □

Remark 5.3 In recursion theory, Σ^{X} consists of the recursively enumerable subsets of X. By the Rice–Shapiro theorem [Ric56, Ros86], recursive functions F : Σ^{Y} → Σ^{X} again preserve directed unions. The following result has an easier proof in this situation, where σ ∈ Σ measures whether a program ever terminates: then σ ⇔ ⋁_{n} σ_{n}, where σ_{n} decides whether has finished within n steps or is still running.

Proposition 5.4 Suppose that C has stable disjoint coproducts and a dominance Σ that is a distributive lattice. Then for every element σ ∈ Σ, there is some directed diagram d : I → {⊥, ⊤} ⊂ Σ, only taking values ⊥ and ⊤, and with I an overt object (Section 7), of which σ is the join. Proof Intuitively, σ is ⊤ just on the part U ≡ [σ] of the world that it classifies, so σ is the smallest global element that is above the partial element ⊤ : U → Σ. Since U is classified, it is open. Also, as it is a subsingleton, it satisfies the binary part of the directedness property. We achieve the full property by using d ≡ [⊥, ⊤] : I ≡ 1 + U → Σ.

In more orthodox^{3} categorical terms, σ : Γ → Σ is a generalised element and classifies i : U ↪ Γ; then we put I ≡ Γ + U and d ≡ [⊥, ⊤]. Stable disjoint sums in C (Section 9) are needed to show that d : I → Σ is directed and I → Γ is an open map (Section 7). In fact there a semilattice structure

[figure: I ×_{Γ} I ≅ Γ + U + U + U; ∨; Γ + U ≡ I; ⊥; Γ,]

where U ×_{Γ} U ≅ U since U ↪ Γ. An element τ ∈ Σ is an upper bound for the diagram d : I → Σ iff its restriction to U is ⊤, as is the case for σ.

U
[figure: I ≡ Γ + U; [id, i]; Γ; i; ..............]

⩽  V  \overline{}1

[figure: Γ + Γ; id + i; ∩; [⊥, ⊤]; Σ; σ; τ]

[figure: Γ; τ; Σ; ⊤]

If τ classifies V ↪ Γ and is a bound then there is a commutative kite, so U ⊂ V using the pullback. However, to deduce ϕ ⩽ ψ, we need uniqueness of the characteristic maps to Σ, or equivalently the Euclidean principle. □

The synthetic form of this argument uses the left adjoint ∃_{d} : Σ^{Γ} × Σ^{U} ≅ Σ^{Γ+U} → Σ^{Γ} of Σ^{d}, for which ∃_{d}(⊥, ⊤) ≡ ϕ. Corollary 8.4 discusses I-indexed joins.

[More simply, if we formulate the Scott principle, cf. [E], as

ξ : Σ^{N}, F : Σ^{Σ^{N}} ⊢ F ξ ⟺ ∃ℓ:KN . F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ξn

then the Phoa principle is the special case N ≡ 1.]

Corollary 5.5 The dual of the Euclidean principle is therefore also valid in LKLoc. By Theorem 3.10, this says that ⊥ ∈ Σ classifies closed subsets. Proof By Scott continuity and Remark 5.1 for {⊥, ⊤}. □

Classically, this is trivial, but we are making a substantive claim here about how the Sierpiński space ought to be defined intuitionistically. This claim is amply justified by the open–closed symmetry that we shall see in this paper and [D]. Indeed Japie Vermeulen has identified the dual Frobenius law for proper maps of locales [Ver94], although he used the opposite of the usual order on a frame, so that ϕ ⩽ ψ would correspond to inclusion of the closed subsets that they classify. André Joyal and Myles Tierney defined the Sierpiński space by means of the free frame on one generator [JT84, §IV 3], and gave a construction in terms of the poset {⊥ ⩽ ⊤} that amounts to saying that Σ^{Σ} ≅ Σ^{⩽}.

3Orthodox though it may be, I regard parametric objects like this as unsatisfactory without first defining a system of dependent types by means of a class of display maps [Tay99, Chapter VIII]. The object Γ + U is used for a different purpose in [D, Section 7].

[There is a much simpler proof of the dual Euclidean and Phoa principles for locales in §O 7.5.]

Corollary 5.6 By the lattice dual of the results of Section 3, there is a right adjoint Σ^{i} ⊣ ∀_{i} of the inverse image map for the inclusion of a closed subset i : C ^{⊏} X in LKLoc. This satisfies the dual of the Frobenius law,

∀_{i}(θ) ∨ ψ = ∀_{i}(θ ∨ Σ^{i}ψ)

for any θ ∈ Σ^{C} and ψ ∈ Σ^{X}, together with Beck–Chevalley again. □

The same principle is also valid in (parallel) recursion theory, where Martin Hyland stressed [Hyl91, Assumption 4] that ⊥ should classify co-RE subsets, as well as ⊤ classifying RE subsets. He also stated the following idea as his Assumption 6, although it was only after writing that paper that he attached his former student’s name to it.

Proposition 5.7 Let Σ be an exponentiating object with global elements ⊥ ⩽ ⊤ in an internal preorder. Then the conjunction of

(a) Σ is a distributive lattice,

(b) the Euclidean principle, σ ∧ F (σ) ⇔ σ ∧ F (⊤),

(c) its lattice dual, σ ∨ F (σ) ⇔ σ ∨ F (⊥), and

(d) monotonicity of F with respect to the semilattice order, for all F : X × Σ → Σ and σ ∈ Σ, is the Phoa principle that

any such F is monotone in this sense, and conversely for each pair of maps ϕ, ψ : X ⇉ Σ with ϕ ⩽ ψ pointwise, there is a unique map F : X × Σ → Σ with F (x, ⊥) ≡ ϕ(x) and F (x, ⊤) ≡ ψ(x).

In this case, F is obtained from ϕ and ψ by “linear interpolation”: F σ ≡ F ⊥ ∨ (σ ∧ F ⊤).

Another way of stating the Phoa principle is that ⟨ev_{⊥}, ev_{⊤}⟩ : Σ^{Σ} → Σ × Σ is mono and is the order relation on Σ, indeed that for which ∧ is the meet and ∨ the join. Proof [⇒] F must be given by this formula (and so Σ^{Σ} → Σ × Σ is mono) because

F σ ⇔ (F σ ∨ σ) ∧ F σ ⇔ (F ⊥ ∨ σ) ∧ F σ ⇔ (F ⊥ ∧ F σ) ∨ (σ ∧ F σ) ⇔ F ⊥ ∨ (σ ∧ F ⊤).

[⇐] Any function F given by this formula is monotone in σ. With X ≡ Σ, we obtain F ≡ ∧ from ϕ ≡ λx. ⊥ and ψ ≡ id, and F ≡ ∨ from ϕ ≡ id and ψ ≡ λx. ⊤. Now consider the laws for a distributive lattice in increasing order of the number k of variables involved. For k ≡ 0 we have the familiar truth tables. Each equation of arity k ≥ 1 is provable from the ones before when the kth variable is set to ⊥ or ⊤, so let ϕ ⩽ ψ : X ≡ Σ^{k−1} → Σ be the common values; then the two sides of the equation both restrict to ϕ and ψ, so they are equal for general values of the kth variable by uniqueness of F : Σ^{k} → Σ. Finally, σ ∧ F σ ⇔ σ ∧ (F ⊥ ∨ (σ ∧ F ⊤)) ⇔ (σ ∧ F ⊥) ∨ (σ ∧ σ ∧ F ⊤) ⇔ σ ∧ (F ⊥ ∨ F ⊤) ⇔ σ ∧ F ⊤, and similarly for the dual. □

Remark 5.8 Theorem 4.2 and Remarks 4.3(a,c,e,f) can easily be adapted to show that the Phoa principle holds in the free model in which Σ is a distributive lattice, either as the lattice dual result together with a separate proof of monotonicity, or by expanding polynomials. For the latter method, the case of application (4.2(e)) is again the most complicated, the induction hypothesis being F ⊥ ⇒ F σ ⇔ (F ⊥ ∨ σ ∧ F ⊤) ⇒ F ⊤. [This suffers from the same error as Theorem 4.2.] □ Definition 5.9 When all maps F : Γ × Σ → Σ preserve the semilattice order there are two ways of extending this order to binary relations on any other object X of the category (not just the retracts of powers of Σ as in Remark 3.5). They both agree with the concrete order in Cont and (assuming excluded middle) Pos.

(a) The Σ-order, defined by

x ⊑_{Σ} y if ∀ϕ ∈ Σ^{X}. ϕx ⇒ ϕy,

is reflexive and transitive but not necessarily antisymmetric. This is the relation inherited by X via η_{X} from the semilattice order on Σ^{Σ^{X}}. For topological spaces, it is known as the specialisation order [Joh82, §II 1.8], but in Set, it is discrete (x ⊑_{Σ} y iff x = y).

(b) The link relation is

x ⊑_{L} y if ∃ℓ:Σ → X. ℓ(⊥) = x ∧ ℓ(⊤) = y,

i.e. a path from x to y indexed by Σ, rather than by the real unit interval as in traditional homotopy theory. For categories in general, this relation need not be transitive or antisymmetric: for example it is indiscriminate in Set, i.e. x ⊑_{L} y always holds [assuming excluded middle].

Wesley Phoa formulated his principle and introduced the link order to show that the order relation on a limit in his category of domains is given in the expected way [Pho90a, §2.3]. For this to work, ℓ must be unique.

Remarks 5.10

(a) All morphisms f : X → Y are monotone with respect to both of the relations that we have just defined (so, when we talk about monotone maps, we mean with respect to the semilattice order).

(b) The link relation is contained in the Σ-order iff all F : Γ × Σ → Σ are monotone.

(c) In the poset {⊥ ⩽ ⊤}, these two points are in the link relation iff excluded middle holds, since we need to find a map ℓ : Σ → {⊥ ⩽ ⊤}.

(d) The Σ-order on Σ^{X} coincides with the semilattice order iff η_{Σ^{X}} is monotone.

(e) If Σ is a lattice, then the semilattice order on Σ^{X} is contained in the link relation, but the Phoa principle makes ℓ unique.

(f) Any replete object X inherits the link relation via η_{X} : X ⟶ Σ^{Σ^{X}}, so this always happens when the adjunction Σ^{(−)} ⊣ Σ^{(−)} is monadic.

(g) When the Phoa principle holds, all maps Σ^{Y} → Σ^{X} are monotone (cf. Example 4.5).

(h) As given, these definitions are not internal to the category C: they are for generalised elements (Remark 2.5), i.e. in an enclosing topos such as the presheaf topos Set^{C^{op}} or a model of synthetic domain theory. One way of translating the definition of ⊑_{Σ} into an internal one is as the inverse image along η_{X} of the semilattice order on Σ^{Σ^{X}}, if the appropriate pullback exists. Similarly, ⊑_{L} (with ℓ unique) can be defined internally as X^{Σ}, if this exists.

Important though they are in domain theory, these order relations will only be mentioned in this paper in the trivial situation of the following section.

6 Discrete and Hausdorff objects

Now we can begin to develop some general topology and logic in terms of the Euclidean and Phoa principles and monadicity.

For the remainder of the paper (apart from the last section), we shall work in a model (C, Σ) of the axioms in Remark 3.8, i.e. Σ is a Euclidean semilattice and the adjunction is monadic. The category could be Set, LKLoc, CDLat^{op}, an elementary topos or a free category as considered in Theorem 4.2 and Remark 4.3. We shall also assume the dual Euclidean principle when discussing the dual concepts: closed subspaces, compact Hausdorff spaces and proper maps.

By Theorem 3.10, Σ classifies some class M of supports, which we call open inclusions. So far, M has been entirely abstract: the only maps that are obliged to belong to it are the isomorphisms. The diagonal map Δ : X → X × X is always a split mono, so what happens if this is open or closed?

In accordance with our convention about Greek and italic letters (Remark 2.5), we use p_{0} : X × Y → X and p_{1} : X × Y → Y instead of the more usual π for product projections, though we keep Δ for the diagonal.

Definition 6.1 An object X ∈ obC is said to be discrete if the diagonal X ↪ X × X is open.

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

The characteristic map (=_{X}) : X × X → Σ and its transpose { }_{X} : X → Σ^{X} are known as the equality predicate and singleton map respectively. We shall often write the subscript on this extensional (but internal) notion of equality, to distinguish it from the intensional (but external) equality of morphisms in the category C.

[Symbolically, the equality predicate =_{X} is related to equality of morphisms by the rule

a = b : X = (a =_{X} ) ⟺ ⊤

in which a = b : X is called a statement in Definition I 4.4.]

Lemma 6.2 If X is discrete in this sense then it is T_{1}, i.e. the Σ-order (Definition 5.9(a)) on X is discrete. If all functions Σ → Σ are monotone then the link order is also discrete. Proof If x ⊑_{Σ} y then {x} ⊑_{Σ} {y} in Σ^{X} by Remark 5.10(a), so, by putting ϕ ≡ ev_{x} in the definition of ⊑_{Σ}, by reflexivity we have ⊤ ⇔ {x}(x) ⩽ {y}(x) ≡ (x =_{X} y).

If all F : Σ → Σ are monotone then x ⊑_{L} y ⊢ x ⊑_{Σ} y. But for a direct argument (on the same hypothesis) consider F ≡ λσ. (ℓσ =_{X} ℓ⊥). Then F ⊥ ⇔ ⊤, so F ⊤ ⇔ ⊤ by monotonicity, but this says that x =_{X} y. □

Examples 6.3

(a) Every set is discrete.

(b) For a poset to be discrete in this sense, the diagonal {(x, y) | x =_{X} y} must be an upper subset of X × X. This means that if x ⩽ y then (x, x) ⩽ (x, y) must also lie in this subset, so x = y. Hence discreteness agrees with standard usage. (This is the same argument as in the Lemma.)

(c) For a topological space to be discrete, the diagonal subset must be open. Each singleton {x} is open, so if we may form arbitrary unions of open subsets, all subsets are open.

(d) In recursion theory, ℕ is discrete in the sense of Definition 6.1 and singletons in ℕ are recursively enumerable, but arbitrary subsets are not. This is explored in [D]. Intuitionistically, even 1 has co-RE subspaces that are not RE, so there is nothing to be gained from introducing a notion of strong discreteness.

(e) A presheaf is discrete with respect to Σ ≡ Ω_{j} (Example 2.10(b)) iff it is j-separated [Joh77, Proposition 3.29] [BW85, §6.2].

(f) A recursive datatype X is discrete iff there is a program δ(x, y) that terminates iff its arguments are intensionally equal; for example if X is defined by reduction rules or by generators and relations then δ has to search for an equational proof. Following the usage of decidable (yes or no) and semi-decidable (yes or wait), semi-discrete would perhaps be a clearer term.

Definition 6.4 Dually, we say that an object is Hausdorff if the diagonal is closed (classified by ⊥) [Bou66, §8]. We write (≠_{X}) or (#_{X}) : X × X → Σ for the characteristic function, which is sometimes called apartness. Again, it follows that singletons are closed (the T_{1} separation property in point-set topology), but not arbitrary subsets.

The symbolic rule is

a = b : X = (a ≠_{X} ) ⟺ ⊥

Exercise 6.5 To check that you understand how ≠_{X} is defined, adapt Lemma 6.2 to show that if x ⊑_{Σ} y in a Hausdorff space X then (x ≠_{X} y) ⇔ ⊥, and explain how it follows from this that X is T_{1} in the order-theoretic sense. □

Examples 6.6

(a) For locales, this property is called strong Hausdorffness [Joh82, §III 1.3], but this is because localic and spatial products are not the same unless we require local compactness, as indeed we do in this paper.

(b) An object of a topos is Hausdorff in our sense iff it is ¬¬-separated, and in particular this always happens for classical sets. Similarly, any discrete poset or space whose underlying set is ¬¬-separable is also Hausdorff, the converse also being true for posets. Hausdorffness is therefore not a very interesting property for sets and posets, and it is better to avoid this term altogether unless the dual Euclidean and Frobenius principles hold.

(c) Following the analogy between open and recursively enumerable subsets, a recursive datatype X is Hausdorff iff there is a program δ(x, y) that terminates iff its arguments are unequal (distinguishable). For example, the real line ℝ is Hausdorff, but not discrete [Theorem I 9.3]. Of course, we know this topologically: the point is that this is the case computationally, as Brouwer tried to remind us, in contradiction to the pathological analysis that led to Cantor’s set theory, and “floating point” arithmetic in Fortran and other programming languages, which purport to make equality decidable.

(d) In traditional point-set topology and locale theory, any T_{0} group is Hausdorff, as is any discrete space, but these results depend on being able to form arbitrary unions of open subsets, and are therefore not true recursively. For example, we would otherwise be able to solve the word problem for groups, i.e. detect that a group is non-trivial. In particular, even the singleton subgroup need not be closed.

To sum up, discreteness and Hausdorffness are quite different properties.

Lemma 6.7 Let X be discrete and ϕ ∈ Σ^{X}. Then

∃_{Δ}(ϕ) ≡ (λxy. (x =_{X} y) ∧ ϕx) ≡ (λxy. (x =_{X} y) ∧ ϕy).

Proof We use the Frobenius law ∃_{Δ}(θ∧Σ^{Δ}ψ) ≡ (∃_{Δ}θ)∧ψ, with θ ≡ ⊤, so (∃_{Δ}θ) = (λxy. x =_{X} y). Putting either ψ ≡ Σ^{p_{0}}ϕ or Σ^{p_{1}}ϕ, so ψ = λxy. ϕ(x) or λxy. ϕ(y), we recover ϕ = Σ^{Δ}ψ, so the left hand side of the Frobenius law is ∃_{Δ}(ϕ) and the right hand side is one of the other two expressions.

[figure: [x =_{X} y] ∩ [ϕx]; ⊂; [ϕx] × X; ⊂; [ϕx]; 1]

[figure: Γ × [x =_{X} y]; ∩; ⊂; Δ; Γ × X × X; ∩; p_{01}; p_{02}; Γ × X; ∩; ϕ; Σ; ⊤]

[figure: [x =_{X} y] ∩ [ϕy]; ∪; ⊂; X × [ϕy]; ∪; ⊂; [ϕy]; ∪; 1; ⊤]

Theorem 3.10 gives an alternative proof using open subsets: [(x =_{X} y)∧ϕx] is the same subobject of Γ × X as [(x =_{X} y) ∧ ϕy] since the composites X → X × X ⇉ X are equal; hence they are the also same subobject of Γ × X × X, so the characteristic maps are equal. □

Corollary 6.8 (=_{X}) is reflexive, symmetric and transitive. Proof Consider ϕ ≡ λu. (y =_{X} u) and ϕ ≡ λu. (u =_{X} z). □

This is the algebraic characterisation of the equality predicate, which we consider in Section 10.

Corollary 6.9 (λn. ϕ(n)) a ≡ ∃n. (n =_{ℕ} a) ∧ ϕ(n).

Here “∃n” is as in Definition 7.7. So, instead of β-reducing the application of a predicate to an argument of type ℕ, i.e. substituting the term a for the variable n throughout the formula ϕ, we can make a local change to the expression-tree and rely on unification to carry out the effect of the substitution [Section A 11]. □

[Lemma J 5.9 proves the properties of equality symbolically from the Euclidean principle.]

Remark 6.10 The analogous property for ∀ in intuitionistic logic is that

∀_{Δ}(ϕ)(x, y) ≡ (x =_{X} y) ⇒ ϕx ≡ (x =_{X} y) ⇒ ϕy.

We need the dual Euclidean and Frobenius principles (Corollary 5.6) to make this equivalent to the lattice dual of the Lemma, namely

∀_{Δ}(ϕ)(x, y) ≡ (x ≠_{X} y ∨ ϕx) ≡ (x ≠_{X} y ∨ ϕy),

for Hausdorff spaces. In this case, an object that is both discrete and Hausdorff is called decidable, cf. Proposition 9.6.

Proposition 6.11

(a) 1 is discrete.

(b) If Σ has ⊥ then 1 is also Hausdorff.

(c) If X and Y are both discrete then so is X × Y.

(d) Similarly if they are both Hausdorff, assuming that Σ is a distributive lattice.

(e) If U ⊂ X is any subset of (i.e. any mono into) a discrete or Hausdorff object then U is also discrete or Hausdorff.

Proof [a,b] (=_{1}) ≡ ⊤ : 1 × 1 → Σ and (≠_{1}) ≡ ⊥. [c,d] (=_{X×Y}) ≡ (=_{X}) ∧ (=_{Y}) and (≠_{X×Y}) ≡ (≠_{X}) ∨ (≠_{Y}).

[figure: U; X; 1; U × U; X × X; ∩; Σ]

[e] U → X is mono iff the square on the left is a pullback. □

The next result will be used to prove Theorem 11.3, so instead of monadicity we assume only that Σ is exponentiating, but still read the existence of the pullback in Definition 6.1 as the definition of discreteness.

Lemma 6.12 If X is discrete then the maps { }_{X} : X → Σ^{X} and η_{X} : X → Σ^{Σ^{X}} are mono.

[figure: Γ; b; a; X; { }_{X}; Σ^{X}]

Σ^{X} × X

[figure: { }_{X} × id_{X}]

[figure: Γ; ⟨b, a⟩; ⟨a, a⟩; X × X; =_{X}; Σ; ev]

.................................. a

[figure: X; Δ_{∪}; 1; ⊤]

Proof If { }_{X} ∘ a = { }_{X} ∘ b then the composites Γ → Σ are equal, but one of them factors through the pullback, so the other does too.

Naturality of η with respect to { }_{X} gives a commutative square

X  \overline{^{\{ \}_{X}}} Σ^{X}

[figure: Σ^{Σ^{X}}; η_{X}; ΣΣ^{^{^{{} ^{}}}^{X}}; ΣΣ^{Σ^{X}}; η_{Σ^{X}}; Σ^{η_{X}}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .]

The map on the right is split mono, so by the first part and cancellation, η_{X} is mono. □

Remark 6.13 The Lemma helps to explain why there are two ways of defining j-separated presheaves (namely being T_{0} or discrete with respect to Ω_{j}) and the fact that Hausdorffness implies sobriety for spaces [Joh82, Lemma II 1.6(ii)]. See also [Joh77, Definition 1.24], [BW85, §2.3, Proposition 6] and [Mik76, p. 3] concerning the singleton map { }_{X} in an elementary topos.

We shall find at the end of the paper that CDLat^{op} satisfies most of our characterisation of elementary toposes, apart from the fact that all sets are discrete. Let’s briefly explore this analogy.

Example 6.14 Assuming excluded middle, the subcategory Set ⊂ Pos ⊂ CDLat^{op} consists of the discrete (equivalently, Hausdorff) objects.

Set components ⊥

discrete

⊥ underlying set

Pos

Ω Υ

Set is the reflective subcategory of the Ω-replete objects in Pos, just as the sheaf subtopos E_{j} consists of the Ω_{j}-replete objects in E [BR98].

The object Ω (the dominance in Set) is the underlying set of Υ (that in Pos), i.e. its image under the right adjoint of the inclusion Set ⊂ Pos. The product-preserving left adjoint (components) to the inclusion of categories is the replete reflection.

By contrast, Ω_{j} is the result of applying the left adjoint, sheafification, to Ω. Also, we have Ω ↞ Υ instead of Ω_{j} ⊂ Ω. □

Remarks 6.15 In the same way we may ask whether adjoints exist to the inclusions of the full subcategories Set and KHaus of (overt) discrete and compact Hausdorff spaces in LKLoc instead of Pos.

[figure: Set; ↼  \underline{(b)}; ⊥; ⊥; \underline{(a)}; LKLoc; (d); ⊥; ⊥; \overline{_{(e) ⇀}}; KHaus]

[figure: Ω; (a,c); Σ; (e,f); 2]

(a) The right adjoint Set ← LKLoc is the set of points functor.

(b) Unfortunately, the left adjoint Set ← LKLoc, which is the components functor, is only defined for locally connected locales [BP80, Tay90], but it does preserve products.

(c) The underlying set of the Sierpiński space Σ is the subobject classifier Ω, and the objects of the smaller category are replete, overt and discrete with respect to both Σ and Ω.

(d) The left adjoint LKLoc → KHaus is the Stone–Čech compactification [Joh82, Theorem IV 2.1], but it does not preserve finite products.

(e) Martín Escardó has shown that the patch topology provides the right adjoint, but only to the inclusion into the category of stably locally compact locales and perfect maps [Esc99].

(f) The patch topology on the Sierpiński space is 2, but 2-replete objects are Stone spaces (totally disconnected compact Hausdorff spaces), and these do not form a pretopos.

The lack of open–closed symmetry between these results makes it very unlikely that they have a unifying formulation in our axiomatisation.

[The overt discrete objects play the role of sets in ASD. If we assume, motivated by (a) above, that the inclusion of the full subcategory of them has a right adjoint U, then this subcategory is a topos with Ω ≡ UΣ and the whole category is equivalent to that of locally compact locales over this topos, [H].]

Discreteness and Hausdorffness are binary properties, relating X to X × X: we now turn to the corresponding nullary ones, involving 1 = X^{0}.

7 Overt and compact objects

[The best introduction to compact and overt subspaces in ASD is that in Sections J 8 and J 11. See also [G, Section 5].]

The characterisation of open maps in terms of the adjunction ∃_{f} ⊣ Σ^{f} in Section 3 (and of closed maps using Σ^{f} ⊣ ∀_{f} in Corollary 5.6) can be generalised to remove the mono requirement.

Unfortunately, as our category need not have all pullbacks, we cannot discuss the Beck– Chevalley condition in the generality that we would like. (We do have it sufficiently often for the purposes of this paper, namely to study the full subcategory of overt discrete objects in Section 10.) For this reason we abstain from giving a generally applicable definition of open map, but, as there is no such problem with Frobenius, we do make the

Definition 7.1 Any map f : Y → X, not necessarily mono, is called pre-open if Σ^{f} : Σ^{X} → Σ^{Y} has a monotone left adjoint ∃_{f} satisfying the Frobenius law

∃_{f}(ψ) ∧ ϕ = ∃_{f}(ψ ∧ Σ^{f}ϕ) for all ϕ ∈ Σ^{X} and ψ ∈ Σ^{Y} ,

where ϕ and ψ are generalised elements, cf. Remark 2.5 and Proposition 8.2.

The origin of the name open is that (for topological spaces) Σ^{f} has a left adjoint satisfying

Frobenius iff, for every open subobject i : U ↪ X, the image of U ↪^{i} X →^{f} Y is open; indeed the characteristic map of this image is ∃_{f}ϕ, where ϕ classifies U. However, this argument does not have any meaning for us, as we do not yet have any notion of direct image, and the one that we shall obtain in Section 10 relies on the present discussion. See [Bou66, §5] for an account of open maps of spaces and [JT84, Chapter V] for the localic version.

Lemma 7.2

(a) All isomorphisms are pre-open maps.

(b) Inclusions of open subsets are pre-open maps (Theorem 3.10).

(c) The composite of two pre-open maps is pre-open.

(d) If e : X ↠ Y is Σ-epi (i.e. Σ^{e} is mono) and f ∘ e is a pre-open map then f : Y → Z is also pre-open.

(e) If m : Y → Z and Σ^{Σ^{m}} are mono, and m ∘ f is pre-open then f : X → Y is also pre-open. Proof [a–c] are obvious. [d] ∃_{f} ≡ ∃_{g} · Σ^{e} where g ≡ f ∘ e. [e] Let E ≡ Σ^{m} · ∃_{g} where g ≡ m ∘ f [the letter E is used to suggest the existential quantifier here, it does not denote a nucleus]. Then we easily have ϕ ⩽ Σ^{g} · ∃_{g}ϕ = Σ^{f} · Σ^{m} · ∃_{g}ϕ = Σ^{f} · Eϕ. Using the hypothesis that Σ^{m} is Σ-epi, for the other two properties, it suffices to consider ψ = Σ^{m}θ. Then

E · Σ^{f} · Σ^{m}θ = E · Σ^{g}θ = Σ^{m} · ∃_{g} · Σ^{g}θ ⩽ Σ^{m}θ

and E(ϕ ∧ Σ^{f} · Σ^{m}θ) = Σ^{m} · ∃_{g}(ϕ ∧ Σ^{g}θ) = Σ^{m}(∃_{g}ϕ ∧ θ) = Eϕ ∧ Σ^{m}θ.  □

Definition 7.3 Similarly, any map f, not necessarily mono, for which Σ^{f} ⊣ ∀_{f} exists and satisfies the dual Frobenius law is called pre-proper. Again, a continuous function between spaces or locales is pre-proper iff the image of every closed subset of X is closed in Y. See [Bou66, §§5, 10] for the theory of proper maps of spaces and [Ver94] for locales, and the dual Frobenius law in particular.

Closed subsets, proper and pre-proper maps satisfy the analogue of Lemma 7.2.

Remark 7.4 The Beck–Chevalley condition (Propositions 3.11 and 8.1) is automatic for (pre-) open maps of spaces and locales, but not for pre-proper maps. In view of the strict duality between them in our theory, this difference in the traditional ones means that we cannot get the Beck– Chevalley condition for free in either case. In keeping with this duality, it seems inappropriate to employ the usual name closed for pre-proper maps.

Remark 7.5 André Joyal and Myles Tierney do construct pullbacks of open maps of locales against arbitrary maps, and prove the Beck–Chevalley condition [JT84, Proposition V 4.1]. But they do this with the benefit of a development of “linear algebra” for sup-lattices, which are to Abelian groups as frames (locales, as they call them) are to commutative rings [op.cit., Chapter I]. In particular, the required pullback of spaces is a pushout of frames and is constructed as a tensor product of sup-lattices, which is obtained as a coequaliser. Our categories do not have arbitrary coequalisers, though it seems plausible that the one that is needed could be constructed. Clearly we are currently even less equipped to undertake an analysis of descent parallel to theirs.

We shall concentrate on the question of whether product projections are open or proper, and on open maps between overt discrete spaces in Section 10.

Remark 7.6 The open–proper symmetry brings us to the question of why we have three words closed, proper and compact (not to mention perfect) in one case and only open in the other. Without them, of course, there would ambiguity over closed but non-compact subsets of noncompact spaces (Proposition 8.3). But open sets are equally ambiguous. [Indeed, we find that overt subspace in real analysis are often also closed, cf. Definition J 11.1.]

Hence the introduction of the word^{4} overt for objects, keeping open for the subsets and maps.

Definition 7.7 An object X ∈ obC is said to be overt if Σ^{!} has a monotone left adjoint ∃_{X} : Σ^{X} → Σ, and compact if there is a monotone right adjoint, ∀_{X}. The Frobenius laws are automatic (Proposition 8.2).

We write ∃x. ϕ(x) and ∀x. ϕ(x) for ∃_{X}(ϕ) and ∀_{X}(ϕ), where ϕ ∈ Σ^{X}. Extending the notational convention in Remark 2.5, the range (X) of such a quantifier must be an overt or compact object respectively, whilst the type of the body, ϕ, like that of a λ-abstraction, must be a power of Σ or the carrier of an algebra.

Examples 7.8

(a) Every set, presheaf or poset is both overt and compact.

(b) Classically, every domain, topological space or locale is overt.

(c) In recursion, ℕ is overt, as are all recursively enumerable datatypes.

(d) See [JT84, §V 3] and [Pho90a, §6.5] for some discussion of overt objects, in particular the partial-function space [ℕ ⇀ X].

(e) If every function Σ^{Y} → Σ^{X} is monotone then ∃_{X} ≡ ev_{⊤} ⊣ Σ^{!} ⊣ ∀_{X} ≡ ev_{⊥} for any object X that has ⊤ and ⊥, by Lemma 5.2, because ⊥ ⊣ ! ⊣ ⊤.

(f) In particular, every domain (with ⊥) is compact.

(g) Similarly, all stable domains are compact, since the only icicle to which ⊥ belongs is the whole domain (Example 4.5).

4Unfortunately this distinction cannot be translated into (for example) French, but whilst overt obviously came from French, it has been recorded in English at least since 1330: it means public or up-front. This seems to be appropriate for a concept that’s related to having a definite distinction between termination and divergence, or between habitation and emptiness. The etymology also parallels our open–closed symmetry, in that the change from aperīre to ^{∗}ōperīre in regional Vulgar Latin was influenced by ^{∗}cōperīre, from which we get cover and covert [Bar88].

But there are also other compact predomains, i.e. not necessarily having ⊥. This intriguing possibility is thrown up by our unification of topology and recursion: future work will uncover their significance.

[Since the publication of this paper, Martín Escardó [Esc04] has written extensively on the computational significance of this notion of compactness.]

Remark 7.9 The usual definition of compactness for topological spaces, that every cover by open subsets has a finite subcover, can be reformulated in terms of directed joins, cf. [Joh82, §III 1] for locales. Our notion of compactness (in the diagram on the right below) is equivalent to the usual one for LKSp and LKLoc because ∀_{X} must be a map in the category, and is therefore Scott-continuous (Examples 2.11, Remark 7.11).

Proposition 7.10 If the quantifiers and ⊥ exist then they must form pullbacks as shown.

[figure: 1; 1; 1; 1; Σ^{X}; ⊥; ∃_{X}; Σ; ⊥; Σ^{X}; ⊤; ∀_{X}; Σ; ⊤]

Conversely, if ⊤ : 1 → Σ^{X} is open then its classifier is ∀_{X}.

Likewise, assuming the dual Euclidean principle, if ⊥ : 1 → Σ^{X} is closed then its classifier is ∃_{X}. Proof ∃_{X}ϕ ⇔ ⊥ iff ϕ = λx. ⊥, and ∀_{X}ϕ ⇔ ⊤ iff ϕ = λx. ⊤.

Conversely, if {⊤} ⊂ Σ^{X} is classified by (some map that we call) ∀_{X} then we need to show that ∀_{X} is monotone, id ⩽ ∀_{X} · Σ^{!} and Σ^{!} · ∀_{X} ⩽ id.

U
[figure: i_{U}; ..............]
[figure: V; 1; 1]

[figure: Γ; i_{V}; ψ; ∨/; ϕ; Σ^{X}; ⊤; ∀_{X}; Σ; ⊤]

Given ϕ, ψ ∈ Σ^{X} with ϕ ⩽ ψ, let U, V ⊂ Γ be their pullbacks against ⊤ : 1 → Σ^{X}, which exist because ∀_{X}ϕ and ∀_{X}ψ classify them. Then ψ ∘ i_{U} ⩾ ϕ ∘ i_{U} = ⊤, whence U ⊂ V, so ∀_{X}ϕ ⩽ ∀_{X}ψ by uniqueness of classifiers.

[figure: 1; 1; Σ; ⊤; ∀_{X} · Σ^{!}; id; Σ; ⊤]

Both of these squares commute, but the one with id is a pullback, so comparing the other with the pullback that it contains we have

1 ≡ [id] ⊂ [∀_{X} · Σ^{!}],

and so the required inequality follows by uniqueness of classifiers.

[figure: X; X; 1; {(ϕ, x) | ϕ[x]}; 1]

⊂

[figure: Σ^{X} × X; (⊤, id); ∩; ∀_{X} × id; Σ × X; (⊤, id); ∩; π_{0}; Σ; ⊤; Σ^{X} × X; ∩; ev; Σ; ⊤]

The two lower composites are the exponential transposes of Σ^{!} · ∀_{X} and id respectively, and both diagrams are pullbacks. So to obtain the required inequality (again using uniqueness of classifiers) we only need to check that one subset is contained in the other, but clearly ϕ[x] = ⊤ when ϕ = λx. ⊤. (We have equality when X is inhabited, but not when it’s empty.)

The analogous result for ∃_{X} depends on the dual Euclidean principle, since we rely on uniqueness of classifiers using ⊥. □

Remark 7.11 The simplest way of imposing Scott-continuity is the equation

F (λx:ℕ. ⊤) ⟺ ∃n:ℕ. F (λx:ℕ. x < n) for all F ∈ Σ^{Σ^{ℕ}}

which was called the Scott Principle in [Tay91]. In this situation, ℕ cannot be compact, because F = ∀_{ℕ} would satisfy

∀_{ℕ}(λx. ⊤) ≡ (∀x:ℕ. ⊤) ⇔ ⊤ ∀_{ℕ}(λx. x < n) ≡ (∀x:ℕ. x < n) ⇔ ⊥,

making the two sides of the Scott principle ⊤ and (∃n. ⊥) ⇔ ⊥. □

Whilst Scott continuity pervades the motivations of Abstract Stone Duality, it is remarkable how many theorems we can prove before we need to invoke it as an axiom. In particular, the search or minimalisation operator μ : (2_{⊥})^{ℕ} → ℕ_{⊥} for general recursion can be constructed without using it [D], but we do need it for the function-space (ℕ_{⊥})^{ℕ} [F]. For all of the investigations that I have done so far in general topology, the Phoa principle and monadicity have been enough.

Proposition 7.12 If X is overt and discrete (in particular X ≡ ℕ) then { }_{X} : X ↣ Σ^{X} is a Σ-split mono, i.e. there is a map I : Σ^{X} ↣ Σ^{Σ^{X}} such that Σ^{^{{ }}^{X}} · I = id_{Σ^{X}}.

[figure: X; \{ \}_{X}; Σ^{X}; Σ^{X}; \underline{λx. F (λy. x =_{X} y) ← F}; ϕ ↦ λψ. ∃y. ϕy ∧ ψy; Σ^{Σ^{X}}]

This subspace is in general neither open nor closed, but ℕ ^{⊂} ℕ_{⊥} ^{⊏} Σ^{ℕ} assuming the Scott principle [D, F]. □

8 The quantifiers

Having used the symbols ∃ and ∀, we are obliged to justify them in terms of the rules of natural deduction, or at least their categorical interpretation [Tay99, §§9.3–4] as we don’t want to get too heavily involved in syntax. In particular, the ability to substitute under a quantifier is another consequence of insisting that the adjunctions be internal.

[The letter E is used in the following two results to suggest an existential quantifier, not a nucleus.]

Proposition 8.1 If Σ^{!} : Σ → Σ^{X} has a left (or right) adjoint then Σ^{p_{1}} : Σ^{Y} → Σ^{X×Y} also has one, and this automatically satisfies the Beck–Chevalley condition, the pullbacks in question being given by product projections as shown on the left below.

[figure: X × Z; X × f; X × Y; p_{0}; X; Σ^{X×Z}; Σ^{X×f}; Σ^{X×Y}; Σ^{p_{0}}; Σ^{X}]

Z \begin{aligned}p_{1} \\ &  \end{aligned}\overline{f} Y \begin{aligned}p_{1} \\ &  \end{aligned}\overline{}1{! \atop }  Σ^{Z} [figure: G; Σ^{p_{1}}]^{Σf} Σ^{Y} [figure: F; Σ^{p_{1}}]^{Σ!}  Σ^{\begin{aligned}E \\ &  \end{aligned}⊣ Σ^{!} }

Proof If E ⊣ Σ^{!} then F ≡ E^{Y} ⊣ Σ^{p_{1}} by Lemma 3.6.

Explicitly, for ω ∈ Σ^{X×Y}, put F (ω) ≡ λy. E(λx. ω(x, y)); then for ψ ∈ Σ^{Y},

F (Σ^{p_{1}}(ψ)) = λy. E(λx. ψy) = λy. EΣ^{!}(ψy) ⩽ λy. ψy = ψ,

whilst ω(x, y) ⇒ Σ^{!}E(λx′. ω(x′, y)) ⇔ F (Σ^{p_{1}}ω)(y).

The Beck–Chevalley condition is naturality of E^{(−)} : Σ^{X×(−)} → Σ^{(−)} with respect to f. Explicitly, ω ↦ λz. E(λx. ω(x, fz)) both ways round the square involving F and G ≡ E^{Z}. □

The preceding proof only required Σ to be exponentiating: the Euclidean principle comes into the next result.

Proposition 8.2 For X overt, every product projection p_{1} : X × Y → Y is pre-open, because (a) by the Euclidean principle, ! : X → 1 is pre-open, i.e. ∃_{X} : Σ^{X} → Σ obeys the Frobenius law

(cf. [JT84, Proposition V 3 1] for locales);

(b) for any pre-open map f : X → Z, the map f × Y : X × Y → Z × Y is also pre-open (cf. Bourbaki’s definition of proper maps, [Bou66, §10]).

Proof

(a) For σ ∈ Σ and ϕ ∈ Σ^{X}, let F (σ) ≡ E(ϕ ∧ Σ^{!}(σ)):

[figure: Γ × Σ; F; Σ; Σ^{X} × Σ^{X}; ϕ × Σ^{!}; ∧^{X}; Σ^{X}; E]

Definition 7.7 required E to be monotone, so F (σ) ⇒ E(Σ^{!}σ) ⇒ σ. Then

E(ϕ ∧ Σ^{!}σ) ⇔ F (σ) ⇔ F (σ) ∧ σ ⇔ F (⊤) ∧ σ ⇔ E(ϕ) ∧ σ

by the Euclidean principle.

(b) Let ϕ ∈ Σ^{X×Z} be a generalised element in the context Γ, so ϕ : Γ → Σ^{X×Z}; then ϕ′ ≡ λx. ϕ(x, z) is a generalised element in the context Γ × Z, and this is how Definition 7.1 must be read. From Proposition 8.1, ∃_{f×Z}ϕ = λz. ∃_{f}(λx. ϕ(x, z)). Then for ψ ∈ Σ^{Y ×Z},

∃_{f×Z}(ϕ ∧ Σ^{f×Z}ψ) = λz. ∃_{f}(λx. ϕ(x, z) ∧ ψ(fx, z))
= λz. (∃_{f}(λx. ϕ(x, z)) ∧ λy. ψ(fx, z))
= ∃_{f×Z}ϕ ∧ ψ □

Proposition 8.3 By analogy with Proposition 6.11,

(a) 1 is overt and compact.

(b) If X and Y are both overt or both compact then so is X × Y.

(c) If U ↪ X is an open subset of an overt object then U is itself an overt object.

(d) Similarly for closed subsets of compact objects. Proof [a] ∃_{1} ≡ ∀_{1} ≡ id_{Σ}. [b] ∃_{X×Y} ≡ ∃_{X} · ∃_{Y}^{X} ≡ ∃_{Y} · ∃_{X}^{Y}. [c,d] U ↪ X → 1 is a composite of open or proper maps. □

[Beware that the letter I in the following two results denotes an “indexing object” not a Σ-splitting.]

Corollary 8.4 If the object I is overt then every algebra (A ≡ Σ^{X}) has internal I-indexed joins, ∧ distributes over them and they are preserved by homomorphisms.

[figure: X × I; f × I; Y × I; A^{I} ≡ Σ^{X×I}; Σ^{f×I}; B^{I} ≡ Σ^{Y ×I}; X; p_{0}; f; Y; p_{0}; A ≡ Σ^{X}; ⋁I; Σ^{f}; B ≡ Σ^{Y}; ⋁I]

Dually, if I is compact then algebras have and homomorphisms preserve I-indexed meets. Proof These are re-statements of the Frobenius and Beck–Chevalley conditions. □

Corollary 8.5

(a) In classical topology, every object I is overt. Therefore algebras have all joins, and binary meet distributes over them, i.e. the algebras are frames, and the homomorphisms preserve joins. By the adjoint function theorem, Heyting implication exists in the algebras, and frame homomorphisms have (non-continuous) right adjoints.

(b) In recursion, ℕ is overt, but other objects need not be. The algebras are sometimes called σ-frames.

(c) ℕ is not compact, so ℕ-indexed meets need not be preserved.

(d) If 0 and 2 are overt then each algebra is an internal distributive lattice, which we shall consider in the next section. □

Now let’s think a bit about syntax, using [Tay99, §9.3].

Remark 8.6 Our category is a model of a fragment of predicate calculus in which each object names a (non-dependent) type, and contexts are products (cf. Theorem 4.2). Each open inclusion U ↪ X is a predicate x : X ⊢ ϕ(x) prop, though we prefer to regard ϕ(x) as a generalised element of Σ^{X}, rather than as a mono. Thus we interpret

Γ ⊢ ϕ prop  by ϕ ∈ Σ, i.e. ϕ : Γ → Σ, and
Γ, ϕ_{1}, ϕ_{2}, …, ϕ_{n} ⊢ θ by ϕ_{1} ∧ ϕ_{2} ∧ ⋯ ∧ ϕ_{n} ⇒ θ ∈ Σ.

The effect of pullback Σ^{p_{0}} ≡ p_{0}^{∗} along a product projection p_{0} : Γ × X → Γ is to add a variable x to the context (weakening, which is written x̂^{∗} in [Tay99]):

Γ ⊢ ϕ prop
Γ, x : X ⊢ ϕ prop

{Γ, ϕ ⊢ θ \atop Γ, x : X, ϕ ⊢ θ}

If X is overt then this map Σ^{p_{0}} has a left adjoint ∃_{X} : Σ^{X} → Σ or ∃_{p_{0}} : Σ^{Γ×X} → Σ^{Γ}, which interprets existential quantification:

Γ, x : X ⊢ ϕ(x) prop
Γ ⊢ ∃x. ϕ(x) prop

Γ ⊢ θ prop Γ, x : X, ϕ(x) ⊢ θ ; = ; Γ, ∃x. ϕ(x) ⊢ θ

The Beck–Chevalley condition is needed to ensure that, for any function f : Γ → Δ between types, the bijective correspondence on the right is preserved by Σ^{f} (substitution or cut along f), whilst the Frobenius law provides in a similar way for additional predicates that may be present in the context.

Remark 8.7 In Section 10 we shall encounter expressions of the forms

∃_{i} · Σ^{i} · Σ^{p_{0}}, ∃_{p_{1}} · ∃_{i} · Σ^{i} · Σ^{p_{1}} and ∃_{p_{1}} · ∃_{i} · Σ^{i} · Σ^{p_{0}}

where i : R ↪ X × Y is the inclusion of an open binary relation classified by ρ : X × Y → Σ. Recall from Section 3 that ∃_{i} · Σ^{i} ≡ ρ ∧ (−), so it takes

Γ, x : X, y : Y ⊢ ψ(x, y)  to  Γ, x : X, y : Y ⊢ ρ(x, y) ∧ ψ(x, y)

without changing the context. Hence the effect on Γ, x : X ⊢ ϕ(x) prop of

∃_{i} · Σ^{i} · Σ^{p_{0}}  is Γ, x : X, y : Y ⊢ ρ(x, y) ∧ ϕ(x) prop
∃_{p_{1}} · ∃_{i} · Σ^{i} · Σ^{p_{1}} is Γ, y : Y ⊢ ∃x:X. ρ(x, y) ∧ ϕ(y) prop
∃_{p_{1}} · ∃_{i} · Σ^{i} · Σ^{p_{0}} is Γ, y : Y ⊢ ∃x:X. ρ(x, y) ∧ ϕ(x) prop □

This brief discussion of the rules of natural deduction and Corollary 10.11 about the direct image show logicians and categorists respectively that we are using the existential quantifier in the usual way. However, the dual of the Euclidean principle implies the dual Frobenius law for ∀_{X}, which is something extra on top of the standard rules for the universal quantifier [Tay99, §9.4], namely that Σ^{!} ⊣ ∀_{X} with the Beck–Chevalley condition.

Remark 8.8 Let ϕ ∈ Σ^{X} be a decidable predicate on any overt compact object, so ∀x. (ϕ(x) ∨ ψ(x)), where ψ ≡ ¬ϕ ∈ Σ^{X}. Then we have ∀x. (ϕ(x) ∨ ∃y. ψ(y)), which is equivalent by the dual Frobenius law to (∀x. ϕ(x)) ∨ (∃y. ψ(y)).

For decidable predicates on ℕ, this property is well known in recursion theory as the Markov principle [Mar47] [Ros86, §5.1].

For us it is not legitimate to write “∀n:ℕ. ϕ(n)” because ℕ is not compact in topology or recursion (Remark 7.11). But consider its one-point compactification, ℕ_{∞}; both ℕ and ℕ_{∞} are (intended to be) overt, and the inclusion i : ℕ ↪ ℕ_{∞} is dense in the sense that (∃x:ℕ_{∞}. ψ(x)) ⇔ (∃n:ℕ. ψ(in)). Although ℕ is not compact, if ⊤ ⇔ ∀x:ℕ_{∞}. ϕ(x) ∈ Σ then Σ^{i}ϕ = ⊤ ∈ Σ^{ℕ}. Conversely, we may transfer Σ-predicates from ℕ to ℕ_{∞}, but we cannot, unfortunately, do the same with decidable ones without prejudging the question for the extra point ∞ ∈ X. □

We have a more encouraging result when we compare our universal quantifier for closed subsets with the standard one for all subsets in a topos. The following situation arises in synthetic domain theory (Remark 2.13), for the sheaves for a Lawvere–Tierney topology (Σ ≡ Ω_{j} in Example 2.10(b)), and also for Ω ↠ Υ in Example 6.14 since this map is actually also mono.

[Eduardo Dubuc and Jacques Penon [DP86] called an object K of a topos compact if its universal quantifier ∀_{K} satisfies the dual Frobenius law.]

Proposition 8.9 Suppose that Σ is an object that satisfies the Euclidean principle in a topos, so Σ classifies certain open subsets, whilst Ω classifies all subsets. If the object X is compact with respect to Σ then the interpretations of ∀_{X} with respect to Σ and Ω agree, in the sense that the bottom face of the cube commutes:

[figure: Γ; {X}; 1]
[figure: .......; ϕ̃; Γ × X; 1]
\{λx. ⊤\}  \overline{}1

[figure: Ω^{X}; ∀^{Ω}; Ω; ⊤]
[figure: ?; mono; Σ; ϕ; Ω; ⊤]
[figure: Σ^{X}; ∩; ∀^{Σ}; Σ; ⊤]

Proof To prove that the two routes Σ^{X} → Ω are equal, it is enough to show that they both classify the Ω-subobject {λx. ⊤} ⊂ Σ^{X}. The front and back faces of the cube are pullbacks by Proposition 7.10, as is the right face because Σ → Ω is mono by Remark 2.13. To show that the left face is also a pullback, consider any test Γ; the two routes Γ ⇉ Ω^{X} are equal iff the square on the right commutes, which it does iff ϕ̃ = λx. ⊤, as required. □

Remark 8.10 Of the other meanings that we might attribute to saying that the two notions of ∀ agree, one is trivially true in that Σ^{X} ≅ ΣX̄, where X̄ is the replete reflection of X, and another is trivially false in that every object is compact with respect to Ω, but not necessarily with respect to Σ.

Remark 8.11 It is not possible to adapt this argument to ∃ and ⊥ because, without excluded middle, characteristic maps with respect to ⊥ : 1 → Ω in a topos need not be unique. An analogous result can nevertheless be achieved by imposing the open cover Lawvere–Tierney topology on the topos, but discussion of this relies on sheaf-theoretic methods, which are inappropriate for this paper.

9 Unions and coproducts

By the monadicity property, our category has finite coproducts, indeed Σ^{X+Y} ≅ Σ^{X} × Σ^{Y}. In this section we consider the question of whether these coproducts are stable and disjoint, and investigate the consequences of assuming that particular objects are overt.

[Theorem B 11.8 constructs coproducts of general spaces in the category and shows that they are stable and disjoint, just assuming that Σ has a point.]

Proposition 9.1

(a) The initial object, 0, is overt iff Σ has a least element, ⊥. Similarly, the existence of ⊤ means that 0 is compact. The Frobenius laws say that σ ∧ ⊥ ⇔ ⊥ and σ ∨ ⊤ ⇔ ⊤, which always hold in a lattice.

(b) 2 is overt iff Σ has binary joins, ∨, and (the Frobenius law for ∃_{2} says that) ∧ distributes over them. Similarly, the existence of ∧ means that 2 is compact, distributivity again being the dual Frobenius law (for ∀_{2}).

(c) If 0 is strict then it is both discrete and Hausdorff because Δ : 0 ≅ 0 × 0 is classified with respect to both ⊤ and ⊥ by the unique map 0 × 0 → Σ.

(d) If + is disjoint and × distributes over it then 2 is discrete and Hausdorff. Proof [b] is Corollary 8.4. To see α ∧ (β ∨ γ) ⇔ (α ∧ β) ∨ (α ∧ γ) directly from the Euclidean principle, consider F (σ) ≡ (σ ∧ β) ∨ (σ ∧ γ). [d] is Proposition 9.5 below. □

So for this section we shall assume that Σ is a distributive lattice. We shall not use the dual Euclidean principle or monotonicity, so the results are applicable to elementary toposes. The main one says that, in the coproduct of spaces, the two components are embedded as complementary open subsets. The coproduct is therefore stable and disjoint, and the empty space is strict.

Theorem 9.2 The category C is extensive, i.e. it has stable disjoint coproducts [Coc93, CLW93] [Tay99, §5.5], cf. [JT84, Corollary to V 2 1] for locales.

[figure: X; Z; Y; 1; 2; s; 1]

Proof Given any commutative diagram in C as shown above, we must show that the top row is a coproduct of spaces (Z = X + Y) iff the squares are pullbacks (inverse images). We do this by considering the corresponding diagram of algebras, with A ≡ Σ^{X}, B ≡ Σ^{Y} and C ≡ Σ^{Z}.

First, let ϕ ≡ Σ^{s}(⊤, ⊥), ψ ≡ Σ^{s}(⊥, ⊤) ∈ C. Since Σ is a lattice and Σ^{s} is a homomorphism, ϕ ∧ ψ ⇔ ⊥ and ϕ ∨ ψ ⇔ ⊤ in C. The definition of ϕ makes the diagram

X  \overline{}Z

[figure: ϕ]

[figure: 1; ν_{0}; 2; s]
[figure: ⊤] [figure: (⊤, ⊥)]

Σ commute, in which the square rooted at 2 is a pullback iff that at Σ is one.

Now suppose that Z = X +Y, so C = A×B. Then ϕ ≡ (⊤, ⊥) ∈ A×B and C ↓ ϕ ≡ (A×B) ↓ (⊤, ⊥) ≅ A. This means that X ≅ [ϕ], i.e. the square rooted at Σ is a pullback, whence so is that at 2.

Conversely, suppose that the two squares are pullbacks, so X = [ϕ] and Y = [ψ]. Then

A × B ≅ (C ↓ ϕ) × (C ↓ ψ) ≅ \{(σ, τ) | σ ⩽ ϕ & τ ⩽ ψ\} [figure: σ, τ ↦ σ ∨ τ; \underline{θ ∧ ϕ, θ ∧ ψ ← θ}] C

is an isomorphism because, using distributivity,

(θ ∧ ϕ) ∨ (θ ∧ ψ) = θ ∧ (ϕ ∨ ψ) = θ ∧ ⊤ = θ
(σ ∨ τ) ∧ ϕ = (σ ∧ ϕ) ∨ (τ ∧ ϕ) = σ ∨ ⊥ = σ

since σ ⩽ ϕ and τ ∧ ϕ ⩽ ψ ∧ ϕ = ⊥. □

Remark 9.3 The category of stable predomains (i.e. of disjoint unions of stable domains, Example 4.5) is also extensive, because the forgetful functor to Set creates coproducts and pullbacks (in the category, not the domains). We may also see this by a version of the preceding argument, since it only depends on being able to define ϕ ∨ ψ when ϕ and ψ are disjoint (ϕ ∧ ψ = ⊥): in terms of the systems of icicles that they classify, to construct ϕ ∨ ψ, each ϕ-icicle must be either wholly contained in a single ψ-icicle, or wholly disjoint from them, and vice versa. Nevertheless, Σ is not an internal lattice — even classically, where it has only two points. □

Proposition 9.4 If X and Y are both overt or both compact then so is X + Y.

If f_{1} : X_{1} → Y_{1} and f_{2} : X_{2} → Y_{2} are both pre-open or both pre-proper maps, then so is f_{1} + f_{2} : X_{1} + X_{2} → Y_{1} + Y_{2}. Proof We define

∃_{X+Y} : Σ^{X+Y} ≅ Σ^{X} × Σ^{Y} → Σ × Σ → Σ by (ϕ, ψ) ↦ (∃x. ϕx) ∨ (∃y. ψy),

∀_{X+Y} by (∀x. ϕx) ∧ (∀y. ψy) and ∃_{f_{1}+f_{2}} by ∃_{f_{1}} × ∃_{f_{2}} : Σ^{X_{1}} × Σ^{X_{2}} → Σ^{Y_{1}} × Σ^{Y_{2}}. The adjunction and Frobenius laws hold componentwise. □

Proposition 9.5 If X and Y are both discrete or both Hausdorff then so is X + Y. Proof The decomposition in the diagram depends on distributivity, but to recover X +Y as the fourfold coproduct [=_{X}] + [⊥] + [⊥] + [=_{Y}] also requires that coproducts be stable and disjoint.

[figure: X + Y; 1; (X + Y) × (X + Y); ∩; ≅; X^{2} + X × Y + Y × X + Y^{2}; [(=_{X}), ⊥, ⊥, (=_{Y})]; Σ; ⊤]

Similarly (≠_{X+Y}) is given by [≠_{X}, ⊤, ⊤, ≠_{Y}]. □

Proposition 9.6 Assuming the dual Euclidean principle, any subset U that is both open and closed is a component of a disjoint union as in Theorem 9.2.

Proof Let U ≡ ϕ^{−1}(⊤) = ψ^{−1}(⊥) and put V ≡ ϕ^{−1}(⊥) and W ≡ ψ^{−1}(⊤), so

0 = U ∩ W = (ϕ ∧ ψ)^{−1}(⊤) 0 = V ∩ U = (ϕ ∨ ψ)^{−1}(⊥).

By uniqueness of characteristic maps of both kinds, ϕ ∧ ψ = ⊥ and ϕ ∨ ψ = ⊤, so we have the situation of Theorem 9.2, V ≡ W being the complement of U. □

In a non-Boolean topos, by contrast, a subset that is both open and closed in our sense need not be complemented, but merely ¬¬-closed.

10 Open discrete equivalence relations

From now on we concentrate on the full subcategory of overt discrete objects, showing that it is a pretopos. The notion of pretopos is the finitary part of Jean Giraud’s categorical characterisation of Grothendieck toposes [Joh77, Theorem 0.45]. These are the properties of the category of “sets” that we require in order to do algebra and symbolic logic in it, for accounts of which see [MR77], [FS90], [Tay99, Chapter V]. In particular we shall show how to construct quotients by equivalence relations using a Σ-split coequaliser.

For point-set topology, related results in both the open and proper cases are to be found in [Bou66, §5.2], except that there an open equivalence relation is by definition one for which q is an open map.

As we do not currently have pullbacks of general open maps (Remark 7.5), we cannot yet develop relative versions of these results for étale maps D → Z, which Joyal and Tierney define as open maps for which Δ : D → D ×_{Z} D is also open [JT84, §V 5].

Proposition 10.1 Pullbacks rooted at any discrete object D exist.

[figure: P; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; X; Y; g^{∗}f; . . . . . . . . . . . . . . . . .; g; D; f]

Proof

D  \overline{}1
[figure: f]
P .................... X

[figure: D × D; ∩; =_{D}; Σ; ⊤]
[figure: f × id]
[figure: X × Y; i; \begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}; id × g; X × D; (id, f); ∩]

[figure]

X

[figure: g^{∗}f; Y; p_{1}; g; D; p_{1}]

[figure]

1{! \atop } □

Lemma 10.2 If X is an overt object then f and g^{∗}f are pre-open maps, and the Beck–Chevalley condition holds. Proof (id, f) : X ↪ X ×D and p_{1} : X ×D → D are pre-open maps (Propositions 3.11 and 8.2), where, for ϕ ∈ Σ^{X}, ∃_{(id,f)}ϕ ≡ λxd. ϕ(x) ∧ (fx =_{D} d), so

∃_{f}ϕ = λd. ∃x. ϕ(x) ∧ (fx =_{D} d).  □

Corollary 10.3 If i : X → D is a mono between overt discrete objects then X is classified by some ϕ ∈ Σ^{D}.

[figure: X; id; X; Σ^{X}; id; Σ^{X}]

[figure: X; id; i; D; i; Σ^{X}; id; ∃_{i}; Σ^{D}; Σ^{i}]

Proof The square on the left is a pullback iff i is mono, and then the Beck–Chevalley condition (Propositions 3.11 and 8.1) makes the square on the right commute (Σ^{i} · ∃_{i} = id), which was the condition required in Theorem 3.10. [See §O 8.10 for a simpler symbolic proof.] □

Definition 10.4 A pre-open map f is surjective if id = ∃_{f} · Σ^{f}.

This is equivalent to (∃_{f}⊤) ⇔ ⊤ by the Frobenius law, cf. [JT84, §V 4].

Lemma 10.5 Let f be a pre-open surjective map [from an overt object to a discrete one]. Then g^{∗}f is also pre-open surjective. Proof By the proof of Lemma 10.2, surjectivity of f : X → D says that

λd. ⊤ = ∃_{f}Σ^{f}(λd. ⊤) = ∃_{f}(λx. ⊤) = λd. ∃x.(fx =_{D} d),

which means “∀d ∈ D. ∃x ∈ X. (fx =_{D} d)” externally, cf. Remark 8.8.

We require ∃_{X} · ∃_{i} · Σ^{i} · Σ^{p_{1}} = id, where the effect of ∃_{i} · Σ^{i} was described in Remark 8.7. This is the case for ψ ∈ Σ^{Y} because (∃x. ψy ∧ (fx =_{D} gy)) ⇔ (ψy ∧ ∃x. fx =_{D} gy) ⇔ ψy by Frobenius and surjectivity of f at d ≡ gy. □

Proposition 10.6 If X and Y are both overt or both discrete then so is P. Proof ∃_{P} ≡ ∃_{Y} · ∃_{g^{∗}f} and (=_{P}) ≡ (=_{X}) ∧ (=_{Y}), cf. Propositions 6.11 and 8.3. □

Proposition 10.7 For any morphism f : X → D from an overt object to a discrete one, the kernel pair K ⇉ X of f exists, and i : K ↪ X × X is an open equivalence relation (reflexive, symmetric and transitive). □

Lemma 10.8 Let X be an overt object and i : K ↪ X ×X an open equivalence relation classified by δ : X × X → Σ. Then the coequaliser K ⇉ X ↠ Q exists in C and X ↠ Q is a pre-open surjection. [See Example B 11.13 for a construction using a nucleus in the ASD λ-calculus. In fact, K can be also constructed as a subspace of Σ^{X}.]

\overline{Δ}

[figure: Q; q; X; \underline{p̄_{0}}; \underline{p̄_{1}}; K]

[figure: p_{0}; p_{1}; i]

X × X

Proof Write p̄_{0} ≡ p_{0} ∘ i and p̄_{1} ≡ p_{1} ∘ i.

Since the monadic property says that Σ^{(−)} : C ≃ Alg^{op}, we calculate the coequaliser q of p̄_{0}, p̄_{1} : K ⇉ X as the equaliser Σ^{q} of the homomorphisms Σp̄_{0} and Σp̄_{1} in Alg. As monadic forgetful functors create equalisers, it suffices to show that the carrier of this equaliser exists as an object of C when we just consider Σp̄_{0} and Σp̄_{1} as functions (C-morphisms). To do this we show that ∃p̄_{1} splits the equaliser, i.e. that Σ^{Q} is a retract of Σ^{X}, not just a subobject.

The equations to be verified are

∃p̄_{1} · Σp̄_{1} = id_{Σ^{X}}  and  Σp̄_{0} · ∃p̄_{1} · Σp̄_{0} = Σp̄_{1} · ∃p̄_{1} · Σp̄_{0}

cf. Lemma 3.3. They make Q a Σ-split coequaliser.

First, ∃p̄_{1} · Σp̄_{1} = ∃_{p_{1}} · ∃_{i} · Σ^{i} · Σ^{p_{1}} takes ϕ to (λy. ∃x. ϕ(y) ∧ δ(x, y)) = λy. ϕ(y) by Remark 8.7 and reflexivity.

[figure: U; Σ^{q}; \underline{∃_{q}}; Σ^{X}; Σp̄_{0}; Σp̄_{1}; \underline{∃p̄_{1}}; Σ^{K}]

[figure: Σ^{p_{0}}; Σ^{p_{1}}; ∃_{p_{1}}; ∃_{i}; Σ^{i}]

Σ^{X×X}

For the other equation, that the two composites Σp̄_{0/1} · ∃p̄_{1} · Σp̄_{0} (for 0 and 1) are equal, it suffices to post-compose the mono ∃_{i} and show that

∃_{i} · Σ^{i} · Σ^{p_{0/1}} · ∃_{p_{1}} · ∃_{i} · Σ^{i} · Σ^{p_{0}}

are equal. By Remark 8.7, these composites take ϕ ∈ Σ^{X} to

λxy. δ(x, y) ∧ ∃z. (δ(x, z) ∧ ϕ(z)) and λxy. δ(x, y) ∧ ∃z. (δ(y, z) ∧ ϕ(z))

respectively. These are indeed equal, by symmetry, transitivity and the Frobenius law.

Since U is defined to split the idempotent ∃p̄_{1} · Σ̄^{p_{0}}, we have ∃_{q} · Σ^{q} = id_{U}, and Σ^{q} is a homomorphism by Beck’s theorem. Hence

Σ^{q} · ∃_{q} = ∃p̄_{1} · Σ̄^{p_{0}} = ∃_{p_{1}} · ∃_{i} · Σ^{i} · Σ^{p_{0}},

which takes ϕ ∈ Σ^{X} to

λx. ∃y. δ(x, y) ∧ ϕ(y)

by Remark 8.7. Hence ϕ ⩽ Σ^{q}∃_{q}ϕ by reflexivity, so ∃_{q} ⊣ Σ^{q}.

For the Frobenius law, again it suffices to apply the mono Σ^{q}, which preserves ∧. Let ω ∈ Σ^{Q}, and put ψ ≡ Σ^{q}ω, so ω = ∃_{q}Σ^{q}ω = ∃_{q}ψ and ψ = Σ^{q}∃_{q}ψ. Then

Σ^{q}∃_{q}(ϕ ∧ Σ^{q}ω), which is λx. ∃y. δ(x, y) ∧ ϕ(y) ∧ ψ(y), and
Σ^{q}∃_{q}ϕ ∧ Σ^{q}ω, which is λx. ∃y. δ(x, y) ∧ ϕ(y) ∧ ψ(x),

are the same by symmetry and transitivity. □

Lemma 10.9 Q is discrete and effective.

K ^{_{⊂}  i} X × X
[figure: q × X; X × q]
X [figure: p̄_{0}; p̄_{1}]  Q × X  X × Q
[figure: q × Q; q × Q]
[figure: Q; q; Δ; Q × Q]

Proof The diagram commutes by manipulation of products and because q ∘p̄_{0} = q ∘p̄_{1}. We have just shown that q is pre-open, whence so are q × X etc. by Proposition 8.2, whilst i is pre-open by hypothesis. So the composite K → Q × Q is pre-open, but K ↠ Q is Σ-epi, so Δ is also pre-open by Lemma 7.2, i.e. ∃_{Δ} ⊣ Σ^{Δ} satisfies Frobenius. Hence the split mono Δ is the inclusion of an open subset by Theorem 3.10, i.e. Q is discrete. Using surjectivity of K ↠ Q,

∃_{Δ} · Σ^{Δ} = ∃_{Δ} · ∃_{q∘p_{0}} · Σ^{q∘p_{0}} · Σ^{Δ} = ∃_{q×q} · ∃_{i} · Σ^{i} · Σ^{q×q} = ∃_{q×q}(δ ∧ Σ^{q×q}(−)) = ∃_{q×q}(δ) ∧ (−)

by Frobenius for ∃_{q×q}, so the characteristic map of Δ is (=_{Q}) ≡ ∃_{q×q}(δ).

Then Σ^{q×q}(=_{Q}) ≡ δ since q × q is surjective, i.e. qx =_{Q} qy ⇔ δ(x, y), which says that the quotient is effective. □

Theorem 10.10 The full subcategory of overt discrete objects is effective regular, and is a pretopos if Σ is a distributive lattice. Proof

(a) Finite limits exist by Propositions 6.11, 8.3, 10.1 and 10.6;

(b) effective quotients of equivalence relations exist by Lemmas 10.8 and 10.9;

(c) they are stable under pullback by Lemma 10.5;

(d) coproducts are stable and disjoint, and the initial object is strict, by Theorem 9.2. □

Corollary 10.11 Every map between overt discrete objects factorises as an open surjection followed by an open inclusion. This factorisation is unique up to unique isomorphism and stable under pullback along arbitrary C-maps. Proof Given f : X → Y, form the quotient q : X ↠ Q of the kernel pair K ⇉ X of f. Then the mediator i : Q → Y is mono [Tay99, §5.8], and open by Corollary 10.3. □

Remark 10.12 Although Σ^{X} isn’t discrete (except in a topos), Q is also the image factorisation of δ̃: X → Σ^{X}:

[figure: X; q; Q; { }_{Q}; Σ^{Q}; Σ^{q}; Σ^{X},]

where we check that the composite takes x to λy. (qx =_{Q} qy), which is λy. δ(x, y) by effectiveness. The surjection is Σ-split, as are the inclusions, by Proposition 7.12. □

This is the traditional construction of the quotient as the set of equivalence classes: an element of Q can be represented either by any element of X that is in the equivalence class or by the characteristic function of this class. The quotient is also constructed using this image factorisation in [Joh77, Proposition 1.23]; see also [BW85, §2.3 Theorem 7].

Peter Freyd and Andre Scedrov [FS90] have shown how to capture the notions of effective regular category and pretopos in terms of relations instead of functions. This approach also transfers attention away from objects and on to the morphisms, so it is possible for there to be “too few” objects for the logic: their condition of tabulation says that all of the objects that the logic describes are actually present. Tabulation plays an analogous role in their theory to the monadicity property in ours, and to the axiom of comprehension in set theory.

See [CW87] for another categorical account of relations.

Proposition 10.13 Assuming only the Euclidean law and not monadicity, the overt discrete objects of C carry the structure of a (C-enriched) allegory. Proof The hom-set Rel(X, Y) is Σ^{X×Y}, which is an internal semilattice. The identity on the discrete object X is (=_{X}) and the composition Σ^{X×Y} × Σ^{Y ×Z} → Σ^{X×Z} at the overt object Y is defined by

σ ∘ ρ = λxz. ∃y. ρ(x, y) ∧ σ(y, z).

The unit law is that σ(x, z) ⇔ ∃y. (x =_{X} y) ∧ σ(y, z) and associativity follows as usual from the Frobenius law, which itself comes from the Euclidean principle (Theorem 3.10). For the other two Freyd–Scedrov axioms, we have

(σ ∧ τ) ∘ ρ  = λxz. ∃y. ρ(x, y) ∧ (σ(y, z) ∧ τ(y, z))
⩽ (σ ∘ ρ ∧ τ ∘ ρ) = λxz. (∃y. ρ(x, y) ∧ σ(y, z)) ∧ (∃y′. ρ(x, y′) ∧ τ(y′, z))
(σ ∘ ρ ∧ τ)  = λxz. (∃y. ρ(x, y) ∧ σ(y, z)) ∧ τ(x, z)
⩽ σ ∘ (ρ ∧ σ^{op} ∘ τ) = λxz. ∃y. ρ(x, y) ∧ (∃z′. τ(x, z′) ∧ σ(y, z′)) ∧ σ(y, z)

which follow from the Frobenius law and the adjunction ∃_{Y} ⊣ Σ^{!} by putting y′ ≡ y and z′ ≡ z. □

Proposition 10.14 If the monadic property also holds then this allegory is tabular, and is therefore equivalent to the category of relations of a regular category. Proof Given a relation ρ : X ×Y → Σ, we must find the corresponding open subset U ⊂ X ×Y. Lemma 3.9 did this. □

Remark 10.15 As usual, similar results for compact Hausdorff spaces follow from the dual Euclidean principle; in particular they too form a pretopos.

The root of the distinction between the properties of overt discrete and compact Hausdorff spaces is that ℕ is overt, discrete and Hausdorff, but not compact (Remark 7.11). From Corollary 8.4, it follows that all homomorphisms preserve ℕ-indexed joins (but not necessarily meets), whilst ∃_{f} and ∀_{f}, where they exist, preserve joins and meets respectively by virtue of being adjoints.

Remark 10.16 This opens the way to applying the limit–colimit coincidence from domain theory [Tay87] to the construction of infinitary colimits of overt discrete spaces and limits of compact Hausdorff ones. The following remarks are only intended to sketch the argument, as the questions of the existence of the relevant limits of algebras in C and the internal language needed to invoke them are outside the scope of this paper.

A (filtered) colimit diagram of overt discrete spaces is given by a limit of the corresponding algebras and maps of the form Σ^{f}, but this is accompanied by the diagram of the left adjoints ∃_{f}. As all of these maps preserve ℕ-indexed joins, the limit and colimit coincide. Then the limiting cone and colimiting cocone consist respectively of the inverse images and quantifiers for the colimit of the original diagram of overt discrete spaces. In particular, the colimit is overt and discrete. The subcategory also admits initial algebras [E], so it is an arithmetic universe as defined by André Joyal.

Similarly, a (cofiltered) limit diagram of compact Hausdorff spaces gives rise to a filtered colimit of inverse image maps that coincides with the limit of their universal quantifiers. This subcategory also admits final coalgebras.

11 Monadicity for elementary toposes

This section characterises the case where E is an elementary topos and Ω its subobject classifier [Joh77, Chapter 1] [BW85, Chapter 2]. We change the notation from (C, Σ) to (E, Ω) to emphasise that this is the only section of the paper in which we either assume directly that E is a topos (and Ω classifies all monos) or make other assumptions that turn out to be equivalent to this.

In the earlier parts of this paper we have tried to generalise as much as possible of the basic theory of elementary toposes from higher order to geometric logic, i.e. from Set and toposes to LKLoc and abstract Stone duality. We begin this section with a proof of Paré’s theorem. The reason for doing this is to show what (little) remains that is peculiar to the topos case, and apparently cannot be generalised. [Equideductive topology also incorporates the ideas of Lemmas 11.9 and 11.11 below into topology, so even less remains that is peculiar to the topos case.] Some further simplifications could be made with the aid of the theory of replete objects [BR98], and we switch notation back to Σ for some parts of the present argument that can easily be generalised.

We conclude with a “converse” of Paré’s theorem: a new characterisation of elementary toposes that is not based on the notion of subset.

Definition 11.1 An elementary topos is a category E with an exponentiating classifier Ω as in Section 2, but for all monos. In particular, since X ↪ X × X is classified, all objects are discrete, so all equalisers and pullbacks exist by Proposition 10.1.

Bill Lawvere and Myles Tierney originally included finite limits and cartesian closure in the definition [Law71], but these conditions are redundant.

Remark 11.2 Anders Kock [KM74] constructed function-types by applying (−)^{Y} to the pullback square on the left:

[figure: X; 1; X^{Y}; 1; Ω^{X}; { }_{X}; ∩; s_{X}; Ω; ⊤; Ω^{X×Y}; (s_{X})^{Y}; Ω^{Y}; ⊤]

where { }_{X} is mono by Lemma 6.12 and s_{X}(ϕ) says that ϕ is a singleton^{5}. Appealing though this observation is for its directness, it is only applicable to the topos situation, where { }_{X} is open. Corollary 11.5 is available more generally.

Kock’s student and co-author Christian Mikkelsen constructed finite colimits using the minimal topos axioms. However, their existence follows much more easily from the next result, due to Robert Paré [Par74], which was the inspiration for the present work. (It is reproduced in Mikkelsen’s thesis, [Mik76, p. 57].) Nevertheless, Mikkelsen’s characterisation of X +Y ⊂ Ω^{X} ×Ω^{Y} is much simpler than the one obtained by unwinding the monadic result: [Tay99] uses it in Example 2.1.7, before defining categories in Section 4.1 and monads in Section 7.5.

Theorem 11.3 For a topos, Ω^{(−)} ⊣ Ω^{(−)} is monadic. Proof Since every object X is discrete, η_{X} is mono by Lemma 6.12, so Ω^{(−)} is faithful [Mac71, §IV 3]. But as η_{X} is classified (open), it is regular mono, so Ω^{(−)} also reflects invertibility (and X is replete in the sense of synthetic domain theory).

We know that the equaliser

[figure: X; i; Ω^{A}; Ω^{α}; η_{Ω^{A}}; ΩΩ^{Ω^{A}}]

exists in any topos (since ΩΩ^{Ω^{A}}is discrete), but we need to show that Ω^{i} is also the coequaliser. In fact, there is a split coequaliser diagram with ∃_{η_{Ω^{A}}} as the other map.

Since Ω^{η_{A}} · η_{Ω^{A}} = Ω^{η_{A}} · Ω^{α} = id_{Ω^{A}} (it is called coreflexive), the square on the left is a pullback:

[figure: X; i; Ω^{A}; Ω^{X}; ∃_{i}; Ω^{Ω^{A}}]

[figure: Ω^{A}; i; η_{Ω^{A}}; ΩΩ^{Ω^{A}}; Ω^{α}; Ω^{Ω^{A}}; Ω^{i}; ∃_{η_{Ω^{A}}}; ΩΩ^{Ω^{Ω^{A}}}; Ω^{Ω^{α}}]

As i and η_{Ω^{A}} are mono, they’re open and admit existential quantification satisfying the Beck– Chevalley condition on the right. This says that Ω^{i} and ∃_{i} split the idempotent Ω^{Ω^{α}} · ∃_{η_{Ω^{A}}}, since also Ω^{i} · ∃_{i} = id. This idempotent is the one that arises from the split coequaliser diagram, since Ω^{η_{Ω^{A}}} · ∃_{η_{Ω^{A}}} = id and Ω^{α} · i = η_{Ω^{A}} · i. Hence, by Beck’s theorem, the adjunction is monadic. □

Remark 11.4 In the monadic situation,

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

5Actually a description in the sense of Russell, cf. [Tay99, §1.2]. See also Section A 9.

is always an Σ-split equaliser. What is peculiar to the topos case is that the quantifiers exist and are splittings. In fact the universal quantifier could be used instead, and these are the least and greatest splittings:

∃_{η_{X}} ⩽ η_{Ω^{X}} ⩽ ∀_{η_{X}} ∃η_{Ω^{Ω^{X}}} ⩽ ΩΩ^{η_{Ω^{X}}} ⩽ ∀η_{Ω^{Ω^{X}}}

The dual of the Euclidean principle is not needed to use the universal quantifier, since the argument is based on the Beck–Chevalley condition rather than the Frobenius law, cf. Proposition 3.11.

Corollary 11.5 Any topos E is cartesian closed. Proof Since it is a right adjoint, (−)^{Y} preserves equalisers. More precisely, we first construct the equaliser

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

(since all finite limits exist in E), and then a little easy diagram chasing shows that it also has the required universal property of the exponential. □

Conjecture 11.6 If all η_{X} are open inclusions then E is a topos. (If ∃_{η_{1}} exists then negation is definable; if ∀_{η_{1}} exists then implication appears to be definable.)

Now we shall look for a converse to Paré’s theorem, i.e. given a monadic category, what further conditions would force it to be an elementary topos? These conditions will be in the form of the existence of quantifiers in higher order logic.

Lemma 11.7 The object Ω is discrete iff it is an internal Heyting algebra. Proof Define x =_{Ω} y as usual by (x ⇒ y) ∧ (y ⇒ x), and conversely x ⇒ y by ((x ∧ y) =_{Ω} x). □

Although it follows that all powers of Ω are Heyting algebras, (⇔) : Ω^{X} × Ω^{X} → Ω^{X} has the wrong type to be the equality predicate.

Proposition 11.8 Every object of a topos is compact, i.e. it has a universal quantifier. [We do not mean the sense of Dubuc and Penon [DP86], which also requires the dual Frobenius law.] Proof By Proposition 7.10, since the singleton {λx.⊤} ⊂ Ω^{X} is classified. □

Lemma 11.9 If Ω is discrete and Ω^{X} is compact then Ω^{Ω^{X}} is also discrete. Proof Leibnizian equality: F =Ω^{Ω^{X}} G iff ∀ϕ:Ω^{X} . F ϕ =_{Ω} Gϕ. □

Lemma 11.10 If X is T_{0} (i.e. η_{X} : X → Ω^{Ω^{X}} is mono) and Ω^{Ω^{X}} is discrete then X is also discrete. Proof Proposition 6.11. □

There is another famous reduction amongst quantifiers in higher order logic:

Lemma 11.11 If Ω is discrete and both Ω and X are compact then X is overt. Proof ∃x. ϕ[x] is ∀σ. (∀x. (ϕ[x] ⇒ σ)) ⇒ σ. □

Theorem 11.12 Let Ω be a Euclidean semilattice in a category E such that the adjunction Ω^{(−)} ⊣ Ω^{(−)} is monadic. Then the following are equivalent:

(a) E is a topos with subobject classifier Ω;

(b) all objects are overt and discrete;

(c) all objects are overt, Ω is discrete and all Ω^{X} are compact;

(d) Ω is discrete and all objects are compact. Hence E is also a pretopos and cartesian closed. Proof [a⇒d] Proposition 11.8; [d⇒c] Lemma 11.11; [c⇒b] Lemma 11.10.

[b⇒a] Condition (b) says that the pretopos of overt discrete objects that we discussed in the previous section is in fact the whole of E. Hence all maps are open (Lemma 10.2), and in particular Ω classifies all monos by Theorem 3.10 and Corollary 10.3, so E is a topos. □

Remark 11.13 From this point of view, CDLat^{op} falls short of being a topos in that Υ is not discrete, but the discrete objects are sets (Examples 2.12 and 6.14). □

Putting this Theorem together with Theorem 4.2 and Remark 4.3, we have justified the claim that the monadicity property plays the role of comprehension, in the sense that it provides a new formalism for elementary toposes that makes no mention of subsets, and doesn’t even need dependent types.

Corollary 11.14 The free category with an exponentiating Heyting algebra, such that the adjunction is monadic, all objects are overt and all algebras are compact, is a topos. [This suffers from the same error as Theorem 4.2.] □

Remark 11.15 In terms of our common formulation of geometric and higher order logic, we have seen that the difference between them is measured by the availability of quantifiers of various kinds. I feel that some of these quantifiers (in particular ∀_{Ω^{X}} : Ω^{Ω^{X}} → Ω, from which we deduced discreteness of Ω^{Ω^{X}}) take the atomic theory of matter beyond what is justified by our intuition of “collections” and other mathematical objects (such as Abelian groups with bases of formal triangulations, from which homology and category theory developed).

Whilst a great deal of the geometrical core of mathematics could potentially be developed within our geometric logic, there are some things that cannot be done in this logically weak scheme, notably questions of well-foundedness, termination, strong normalisation and consistency in recursion theory and proof theory. We might try to formulate an intermediate scheme of quantifiers to handle these matters, retaining the Euclidean and monadic conditions as the basic framework.

At first sight, the above results would appear to rule this out, if ⇒ is to be allowed and ∀_{Ω^{X}} forbidden, but something similar to the latter is to be included. However, synthetic domain theory has already shown that a model may have two objects, Σ and Ω, classifying weaker and stronger fragments of logic (Remark 2.13). The extra quantifier could make use of both objects, but since all maps Ω → Σ are constant, we are left with

∀ : Π^{Σ^{X}}⟶ Π,

where Π is the name of the intermediate classifier, with Σ ⊂ Π ⊂ Ω. We might hope to use it to give a synthetic proof of the general recursion theorem, that the induction scheme suffices for recursion [Tay99, §6.3].

But what is already clear from these investigations is that our “synthetic” arguments in topology are much simpler and to the point than the traditional ones in point-set topology, locale theory and continuous lattices. So long as we give up trying to detect equality of predicates, they also have a programming interpretation.

Acknowledgements. The original inspiration for this work came while I was visiting Pino Rosolini at the Università degli Studi di Genova in March 1993, and many of the results were found during my second visit in October and November 1997; both visits were funded by the Italian Concilio Nazionale della Ricerca.

This paper was drafted during my visit to Macquarie University in August 1997.

The work has benefitted much from my discussions with Martín Escardó, Martin Hyland, Peter Johnstone, Anders Kock, Eugenio Moggi, Bob Paré, Bob Rosebrugh, Pino Rosolini, Andrea Schalk, Alex Simpson, Thomas Streicher, Steve Vickers, Graham White, Todd Wilson and Richard Wood.

The Euclidean principle was announced in the categories electronic mail forum on 29 June 1997, but I had first encountered this equation on 12 March 1997.

References

[Bar88] Robert Barnhart. Chambers Dictionary of Etymology. 1988.

[Bar92] Henk Barendregt. Lambda calculi with types. In Samson Abramsky et al., editors, Handbook of Logic in Computer Science, volume 2, pages 117–309. Oxford University Press, 1992.

[Ber78] Gérard Berry. Stable models of typed λ-calculi. In International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, pages 72–89. Springer-Verlag, 1978.

[BFS03] Anna Bucalo, Carsten Führmann, and Alex Simpson. An equational notion of lifting monad. Theoretical Computer Science, 294:31–60, 2003.

[Bou66] Nicolas Bourbaki. Topologie Générale. Hermann, 1966. English translation, “General Topology”, distrubuted by Springer-Verlag (1989).

[BP80] Michael Barr and Robert Paré. Molecular toposes. Journal of Pure and Applied Algebra, 17:127–132, 1980.

[BR98] Anna Bucalo and Giuseppe Rosolini. Repleteness and the associated sheaf. Journal of Pure and Applied Algebra, 127:147–151, 1998.

[BW85] Michael Barr and Charles Wells. Toposes, Triples, and Theories. Springer-Verlag, Berlin, Germany, Heidelberg, Germany, London, UK etc., 1985.

[CLW93] Aurelio Carboni, Steve Lack, and Robert Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84:145–158, 1993.

[Coc93] J. Robin B. Cockett. Introduction to distributive categories. Mathematical Structures in Computer Science, 3:277–307, 1993.

[CW87] Aurelio Carboni and Robert Walters. Cartesian bicategories. I. Journal of Pure and Applied Algebra, 49(1–2):11–32, 1987.

[DP86] Eduardo Dubuc and Jacques Penon. Objets compacts dans les topos. Journal of the Australian Mathematical Society Series A, 40:203–217, 1986.

[Esc99] Martín Escardó. On the compact regular coreflection of a stable compact locale. In Proceedings of the 15th conference on Mathematical Foundations of Programming Semantics (MFPS XV), volume 20 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.

[Esc04] Martín Escardó. Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21–156, 2004.

[FR97] Marcelo Fiore and Giuseppe Rosolini. Two models of synthetic domain theory. Journal of Pure and Applied Algebra, 116:151–162, 1997.

[Fre66a] Peter Freyd. Algebra-valued functors in general and tensor products in particular. Colloq. Math., 14:89–106, 1966.

[Fre66b] Peter J. Freyd. The theory of functors and models. In Theory of Models — Proceedings of the 1963 International Symposium at Berkeley, pages 107–120. North Holland, 1966.

[FS90] Peter Freyd and Andre Scedrov. Categories, Allegories, volume 39 of North-Holland Mathematical Library. North-Holland, Amsterdam, 1990.

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

[GHK^{+}80] Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael Mislove, and Dana S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980. Second edition, Continuous Lattices and Domains, published by Cambridge University Press, 2003.

[Hau14] Felix Hausdorff. Grundzüge der Mengenlehre. 1914. Chapters 7–9 of the first edition contain the material on topology, which was removed from later editions. Reprinted by Chelsea, 1949 and 1965; there is apparently no English translation.

[Hyl91] J. Martin E. Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria-Cristina Pedicchio, and Giuseppe Rosolini, editors, Proceedings of the 1990 Como Category Conference, number 1488 in Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[Hyl10] Martin Hyland. Some reasons for generalising domain theory. Mathematical Structures in Computer Science, 20(02):239–265, 2010.

[JM07] Achim Jung and Andrew Moshier. A Hofmann-=Mislove theorem for bitopological spaces. Electronic Notes in Theoretical Computer Science, 173:159–175, 2007.

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

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

[JT84] André Joyal and Myles Tierney. An extension of the Galois theory of Grothendieck. Memoirs of the American Mathematical Society, 51(309), 1984.

[KM74] Anders Kock and Christian Mikkelsen. Non-standard extensions in the theory of toposes. In Albert Hurd and Peter Loeb, editors, Victoria Symposium on Nonstandard Analysis, number 369 in Lecture Notes in Mathematics, pages 122–143. Springer-Verlag, 1974.

[Koc81] Anders Kock. Synthetic Differential Geometry. Number 51 in London Mathematical Society Lecture Notes. Cambridge University Press, 1981. Second edition, number 333, 2006.

[Law71] Bill Lawvere. Quantifiers and sheaves. In Actes du Congrès International des Mathématiciens, volume 1, pages 329–334. Gauthier-Villars, 1971.

[Law00] Bill Lawvere. Comments on the development of topos theory. In Jean-Paul Pier, editor, Development of Mathematics, 1950–2000. Birkhäuser, 2000.

[LR75] Joachim Lambek and Basil Rattray. Localizations and sheaf reflectors. Transactions of the American Mathematical Society, 210:275–293, 1975.

[Mac71] Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, Berlin, 1971.

[Mar47] Andrei Markov. On the representation of recursive functions. Doklady Akademii Nauk SSSR, 58:1891–2, 1947.

[Mik76] Christian Mikkelsen. Lattice-theoretic and Logical Aspects of Elementary Topoi. PhD thesis, Århus Universitet, 1976. Various publications, number 25.

[ML84] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.

[MR77] Michael Makkai and Gonzalo Reyes. First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories. Number 611 in Lecture Notes in Mathematics. Springer-Verlag, 1977.

[MRW02] Francisco Marmolejo, Robert Rosebrugh, and Richard Wood. A basic distributive law. Journal of Pure and Applied Algebra, 168:209–226, 2002.

[Par74] Robert Paré. Colimits in topoi. Bulletin of the American Mathematical Society, 80(3):556–561, May 1974.

[Pho90a] Wesley Phoa. Domain Theory in Realizability Toposes. PhD thesis, University of Cambridge, 1990. University of Edinburgh Dept. of Computer Science report CST-82-91 and ECS-LFCS-91-171.

[Pho90b] Wesley Phoa. Effective domains and intrinsic structure. In Logic in Computer Science 5, pages 366–377. IEEE Computer Society Press, 1990.

[Ric56] Henry Rice. Recursive and recursively enumerable orders. Transactions of the American Mathematical Society, 83:277, 1956.

[Ros86] Giuseppe Rosolini. Continuity and Effectiveness in Topoi. D. phil. thesis, University of Oxford, 1986.

[RT98] Giuseppe Rosolini and Paul Taylor. Abstract stone duality in synthetic domain theory. In preparation, 1998.

[Sam87] Giovanni Sambin. Intuitionistic formal spaces: a first communication. In D. Skordev, editor, Mathematical Logic and its Applications, pages 187–204. Plenum, 1987.

[Tay87] Paul Taylor. Homomorphisms, bilimits and saturated domains — some very basic domain theory. 1987.

[Tay90] Paul Taylor. An algebraic approach to stable domains. Journal of Pure and Applied Algebra, 64:171–203, 1990.

[Tay91] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[Ver94] Japie J. C. Vermeulen. Proper maps of locales. Journal of Pure and Applied Algebra, 92:79–107, 1994.

[Vic98] Steven Vickers. Topical categories of domains. Mathematical Structures in Computer Science, 1998.

[Wil94] Todd Wilson. The Assembly Tower and some Categorical and Algebraic Aspects of Frame Theory. PhD thesis, Carnegie–Mellon University, May 1994.

[Woo04] Richard J. Wood. Ordered sets via adjunctions. In Maria-Cristina Pedicchio and Walter Tholen, editors, Categorical Foundations, number 97 in Encyclopedia of Mathematics and its Applications, pages 1–47. Cambridge University Press, 2004.

The papers on abstract Stone duality may be obtained from

                             www.Paul Taylor.EU/ASD

[O] Paul Taylor, Foundations for Computable Topology. in Giovanni Sommaruga (ed.), Foundational Theories of Mathematics, Kluwer 2011.

[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.

[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 122 (2005) 247-296.

[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, 2 (2006) 1–70.

[H–] Paul Taylor, An elementary theory of the category of locally compact locales. APPSEM

Workshop, Nottingham, March 2003.

[H] Paul Taylor, An elementary theory of various categories of spaces and locales. November 2004.

[I] Andrej Bauer and Paul Taylor, The Dedekind reals in abstract Stone duality. Mathematical Structures in Computer Science, 19 (2009) 757–838.

[J] Paul Taylor, A λ-calculus for real analysis. Journal of Logic and Analysis, 2(5), 1–115 (2010)

[K] Paul Taylor, Interval analysis without intervals. February 2006.

[L] Paul Taylor, Tychonov’s theorem in abstract Stone duality. September 2004.

[N] Paul Taylor, Computability in locally compact spaces. 2010.

[AA] Paul Taylor, Equideductive categories and their logic. 2010.

[BB] Paul Taylor, An existential quantifier for topology. 2010.

[CC] Paul Taylor, Cartesian closed categories with subspaces. 2009.

[DD] Paul Taylor, The Phoa principle in equideductive topology. 2010.

[EE] Paul Taylor, Discrete mathematics in equideductive topology. 2010.

[FF] Paul Taylor, Equideductive topology. 2010.

[GG] Paul Taylor, Underlying sets in equideductive topology. 2010.