Returning from logic to topology, recall from Definition 1.5 that we need to represent points, open subobjects and compact subobjects in our calculus. These will be given by terms of type X, Σ^{X} and Σ^{ΣX} respectively, but whilst the first two correspond exactly, the question of which second order terms denote compact subspaces is more complicated.
We pick up the treatment of compact objects from Section C 7, and show how this leads to the representation of compact subobjects as quantifiers or modal operators. Following [HM81], these should preserve finite meets and directed joins, but the basic idea of ASD is that the directed joins come for free. A compact subobject is therefore represented by a term A:Σ^{ΣX} for which A⊤⇔⊤ and A(φ∧ψ)⇔ Aφ∧ Aψ.
This abstract idea works very well as far as the relationship between compact and closed subspaces of a compact Hausdorff space. But then we run into some trouble, because at that point we actually need to use Scott continuity, but our logical structure will not be strong enough to do this until Section 9. There is an alternative treatment in [J] that avoids this problem by restricting to the Hausdorff case, and in particular ℝ and ℝ^{n}; you may prefer to read that instead of this section, or in parallel with it.
In the experimental spirit, we try to go further down the path laid by [HM81, JS96], but we stumble into more and more potholes, showing how much more work needs to be done in ASD to make it into a full theory of general topology. But Jung and Sünderhauf do have something interesting to show us when we make this excursion, namely a very close duality between compact and open subobjects of stably locally compact objects.
The abstract analogue of the way in which locale theory treats local compactness is much simpler than this. In that case any term A:Σ^{ΣX} may be used — it doesn’t have to preserve meets.
Remark 5.1
Traditionally^{2},
a topological space K has been defined to be
compact if every open cover,
i.e. family {U_{s} ∣ s∈ S} of open subspaces such that K=⋃_{s} U_{s},
has a finite subcover, F⊂ S with K=⋃_{s∈ F} U_{s}.
If the family is directed (Definition 1)
then F need only be a singleton,
i.e. there is already some s∈ S with K=U_{s}.
The Scott topology on the lattice Σ^{K} offers a simpler way of saying that K is compact. In this lattice, ⊤ denotes the whole of K, so compactness says that if we can get into the subset {⊤}⊂Σ^{K} by a directed join ⋃_{s}^{↑} U_{s} then some member U_{s} of the family was already there^{3}. In other words, {⊤}⊂Σ^{K} is an open subset in the Scott topology on the lattice.
Definition 5.2 In abstract Stone duality we say that
an object K is compact if there is a pullback
Using the fact that Σ classifies open subobjects (Remark 3.2), together with its finitary lattice structure (but not the Scott principle), Proposition C 7.10 shows that ∀_{K} exists with this property iff it is right adjoint to Σ^{!K} (where !_{K} is the unique map K→1). It is then demonstrated that this map does indeed behave like a universal quantifier in logic (the corresponding existential quantifier was given by Definition 4.3).
Lemma 5.3 If K and L are compact objects then K+L
is also compact, as is ∅.
Proof ∀_{K+L}(φ,ψ)⇔∀_{K}φ∧∀_{L}ψ and ∀_{∅}=⊤:Σ^{∅}≅1→Σ. ▫
The following result is the well known fact that the direct image of any compact subobject is compact (whereas inverse images of open subobjects are open).
Lemma 5.4
Let K be a compact object and p:K↠ X be Σepi^{4},
i.e. a map for which Σ^{p}:Σ^{X}→Σ^{K} is mono.
Then X is also compact, with quantifier ∀_{X}=∀_{X}·Σ^{p}.
Proof The given quantifier, Σ^{!K}⊣∀_{K}, satisfies the inequalities
id ≤ ∀_{K}·Σ^{p}·Σ^{!X} = ∀_{K}·Σ^{!K} 
Σ^{p}·Σ^{!X}·∀_{K}·Σ^{p} = Σ^{!K}·∀_{K}·Σ^{p} ≤ Σ^{p}, 
from which we deduce Σ^{!X}⊣∀_{K}·Σ^{p}, since Σ^{p} is mono. ▫
What becomes of the quantifier ∀_{K} when K no longer stands alone but is a subobject of some other object X? We see that any compact subobject K⊂ X defines a map A:Σ^{X}→Σ or A:Σ^{ΣX} that preserves ⊤ and ∧. We shall call this a necessity (▫) modal operator, rather than a quantifier, since we have lost the instantiation or ∀elimination rule Aφ⇒φ x.
Lemma 5.5 Let i:K→ X be any map, with K compact.
Then A≡∀_{K}·Σ^{i}:Σ^{X}→Σ preserves ⊤
and ∧.
Moreover Aφ≡∀_{K}(Σ^{i}φ)⇔⊤ iff Σ^{i}φ=⊤_{K}.
Proof Σ^{i} preserves the lattice operations and ∀_{K} is a right adjoint. ▫
Remark 5.6 In traditional language, for any open set U⊂ X
classified by φ:Σ^{X}, the predicate Aφ says whether K⊂ U.
Just as ∀_{K}:Σ^{K}→Σ classifies {⊤}⊂Σ^{K},
the map A:Σ^{X}→Σ classifies a Scottopen family F
of open subspaces of X, namely the family of neighbourhoods of K.
Preservation of ∧ and ⊤ says that
this family is a filter.
Notice that we have an example of the alternation K⊂ U of compact and open subobjects that we saw in Lemma 1.2. Also, recall from Definition 1.5 that we wanted to test x∈ U and K⊂ U; these are expressed by the λapplications φ x and Aφ respectively.
Proof
Corollary 5.8 A_{K}⊥⇔⊤ if K is empty, ⊥ if it’s inhabited. ▫
Remark 5.9 Classically, any compact (sub)space that satisfies
A_{K}⊥⇔⊥ must therefore contain a point, by excluded middle,
but Choice is still needed to find it
[Joh82, Exercise VII 4.3].
In the localic formulation, it is a typical use of the maximality principle
to find a prime filter containing F,
so A≤ P in our notation. ▫
The situation in which open and compact subobjects interact extremely well is that of a compact Hausdorff object (Definitions 4.2 and 5.2).
Lemma 5.10 Let X be a compact Hausdorff object and φ:Σ^{X}. Then

Proof These are the lattice duals of (x=y)∧φ x ⇔ (x=y)∧φ y, φ x ⇔ ∃ y.(x=y)∧φ y, reflexivity, symmetry and transitivity in any overt discrete object, and the following proof is just the dual of that in Lemma C 6.7.
The closed subobject Δ:X⊂ X× X is coclassified by (≠_{X}), so the corresponding nucleus, in the senses of both locale theory (j≡Δ_{*}·Δ^{*}) and of abstract Stone duality (E≡∀_{Δ}·Σ^{Δ}, Axiom 3.3(c) and Lemma 3.8) takes
φ:Σ^{X× X} to λ x y.(x≠ y)∨φ y. 
Consider in particular ψ≡Σ^{p0}φ, or ψ(x,y)≡φ x; then
∀_{Δ}φ = ∀_{Δ}·Σ^{Δ}·Σ^{p0}φ = ∀_{Δ}·Σ^{Δ}ψ = (∀_{Δ}⊥)∨Σ^{p0}φ. 
The same thing in λcalculus notation, and its analogue for p_{1}, are
(∀_{Δ}φ)(x,y) ⇔ (x≠ y)∨ φ x ⇔ (x≠ y)∨ φ y. 
Now apply ∀_{p0}≡∀ y, so φ = ∀_{p0}·∀_{Δ}φ = ∀_{p0}(∀_{Δ}⊥∨Σ^{p0}φ), i.e. φ x ⇔ ∀ y.(x≠ y)∨φ y . Inequality is irreflexive by definition. We deduce symmetry by putting φ≡λ u.(y≠ u) and the dual of the transitive law with φ≡λ u.(u≠ z). ▫
The idea of the following construction is that K⊂ U iff U∪ V=X, and conversely x∈ V iff K⊂ X∖{x}, where K is compact and V is its complementary open subobject, encoded by A and ψ respectively. The lattice dual of this result — that open and overt subobjects coincide in an overt discrete object — was proved for ℕ in Section A 10.
Proposition 5.11 In any compact Hausdorff object K,
there is a retraction Σ^{K}◁Σ^{ΣK} given by

where, if A is so defined from ψ then it preserves ⊤ and ∧.
Later we shall show that closed and compact subobjects agree exactly.
Proof ψ↦ A↦λ x.A(λ y.ψ y∨ x≠ y)=ψ, by the second part of the Lemma. Then A⊤⇔⊤ easily, whilst A(φ_{1}∧φ_{2})⇔ Aφ_{1}∧ Aφ_{2} by distributivity.
On the other hand, A↦ψ↦λφ.∀ x.A(λ y.φ y∨ x≠ y), whilst the first part of the Lemma says that A=λφ.A(λ y.∀ x.φ y∨ x≠ y), so for the bijection between closed and compact objects we need A to commute with ∀ x. To show this, we need to know about the Tychonov product topology on X× X (Remark 8.3), and to use Scott continuity (Theorem 9.6). ▫
As we said, it is not obligatory that the As that we shall use to define locally compact objects in the next section actually satisfy these conditions, i.e. preserve ⊤ and ∧. Consider the localic situation.
Example 5.12 For β∈ L in a continuous lattice
(Definition 3), the subset
↑β ≡ {φ ∣ β≪φ} ⊂ L 
is Scottopen, and therefore classified by some A:Σ^{L} (Remark 3.2). However, ↑β need not be a filter (cf. Definition 2.9), so A need not preserve ⊤ or ∧. ▫
We obtain similar behaviour even in traditional topology. The following may seem a strange thing to do, but it will fall into place as we start to use the λcalculus.
Notation 5.13
In [A] we found it useful to regard any map
F:Σ^{X}→Σ^{Y} (not necessarily a homomorphism for the monad
or of frames, but nevertheless Scottcontinuous) as a “second class”
map F:Y−× X,
and to write HS for the category composed of such maps.
The work cited there explains how they interpret “control effects”
such as jumps in programming languages.
We shall in particular meet I:Σ^{X}→Σ^{Y}
such that Σ^{i}· I=id, where i:X↣ Y.
Remark 5.14 Just as in Lemma 5.5
we formed the modal operator corresponding to the direct image i K
of K along i:K→ X as the composite A=∀_{K}·Σ^{i},
so we may form the direct image F A
along a second class map F:K−× X as ∀_{K}· F.
Its open neighbourhoods are given, as in Remark 5.6, by
( 
 K⊂φ) ⇔ (∀_{K}· F)φ ⇔ A(Fφ) ⇔ (K⊂ Fφ). 
However, ∀_{K}· F need only be a filter when F preserves ⊤ and ∧.
Even when A does preserve meets, and so classifies a Scottopen filter of open subspaces, it need not correspond to a (locally) compact subspace. (It does in a compact Hausdorff object, but even there we do not yet have to tools to prove it, cf. Proposition 5.11.) We make a brief excursion into classical topology to illustrate the duality of open and compact subspaces, and their alternating inclusions (Notation 1.3). Recall from Definition 1.1 that any open subspace is the union of the compact subspaces inside it: the first result answers the dual question of when a compact subspace is the intersection of the open subspaces that contain it.
Lemma 5.15 Using excluding middle in classical topology
[HM81, p221 def 2.1],
{y∈ X ∣ ∃ x∈ K.x≤ y} = ⋂_{↓}{U⊂ X open ∣ K⊂ U}, 
where ≤ is the specialisation order (Definition 3.7). We call this the saturation of K. Hence compact subspaces of X can be recovered from their modal operators iff X is T_{1} (when ≤ is trivial). For a specific nonexample, let X≡Σ and K≡{⊥}, so A≡λφ.φ⊥ and the saturation of K is Σ. ▫
What we might hope to recover from the modal operator A, therefore, is the saturation of K, as Karl Hofmann and Michael Mislove did for sober spaces [HM81, Theorem 2.16], and Peter Johnstone did for locales [Joh85]. This result shows that we have identified enough of the properties of modal operators, at least in the classical model.
Lemma 5.16 Let F⊂Σ^{X} be a Scottopen
filter of open subspaces of a sober (but not necessarily locally
compact) space. Then, assuming the axiom of choice,
K≡⋂_{↓}F⊂ X is a compact subspace,
and F={U ∣ K⊂ U}. ▫
Lemma 5.17
[HM81, p221 thm 2.16]
Let K≡⋂_{↓}_{s} K_{s}
be a codirected intersection of compact saturated subspaces of a sober space.
Then K is also compact saturated, and A_{K}=⋁^{↑} A_{Ks}.
If all of the K_{s} are inhabited then so is K. ▫
Theorem 5.18
[Kel55, Problem 5 F(a)]
Compact saturated subspaces of a locally
compact sober space form a continuous preframe under reverse inclusion.
That is, for any compact saturated subspace K⊂ X,
K = ⋂_{↓}{L compact saturated ∣ L≺≺ K}. 
Here L≺≺ K means that there is an open subspace U with K⊂ U⊂ L (sic — Notation 1.3), but this is equivalent to L≪ K, the orderreversed analogue of Definition 2, i.e.
K ⊃ ⋂_{↓}_{s} M_{s} ⇒ ∃ s. K⊃ M_{s}. ▫ 
Corollary 5.19
Using Choice in classical topology,
stably locally compact sober spaces enjoy the dual Wilker property
(cf. Lemma 1.10):
if K∩ L⊂ U then there are open subspaces V and W
and compact ones K′ and L′ such that
K′∩ L′⊂ U, K⊂ V⊂ K′ and L⊂ W⊂ L′
[JS96, Theorem 23].
Proof Use Lemma 2.7 in the continuous lattice of compact saturated subspaces under reverse inclusion. It is significant in this that the abstract joins in the lattice be given by intersections of subspaces. ▫
Remark 5.20 There is still a problem.
Even when X itself is locally compact,
and we have a filter F that is Scottopen and therefore classified
by a term A of type Σ^{ΣX},
the compact subspace K that they define need not be locally compact.
Therefore they need not be definable as actual objects
in the theory that we describe in this paper.
However, an extension to and beyond the category of all locales is envisaged
for later work.
Preliminary investigations in this suggest
that any A:Σ^{ΣX} that preserves ⊤ and ∧
can be expressed as the universal quantifier of a compact subobject.
However, as we said at the beginning of this section, the “dual bases” that we shall introduce in the next section use the As and not the Ks. It is a desirable property of A that it be a filter, i.e. preserve ⊤ and ∧, because then we can fully exploit the intuitions of traditional topology. But it is not necessary: locale theory gives rise to bases that don’t have this property, and both ways of doing things have their advantages.