[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}(ψ)∧ φ=∃_{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

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.

- All isomorphisms are pre-open maps.
- Inclusions of open subsets are pre-open maps (Theorem 3.10).
- The composite of two pre-open maps is pre-open.
- 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. - 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

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 non-compact 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*∈*ob*** C** is said to be

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.

- Every set, presheaf or poset is both overt and compact.
- Classically, every domain, topological space or locale is overt.
- In recursion, ℕ is overt, as are all recursively enumerable datatypes.
- See [JT84, §V 3] and [Pho90a, §6.5]
for some discussion of overt objects,
in particular the partial-function space [ℕ⇀
*X*]. - If every function Σ
^{Y}→Σ^{X}is monotone then ∃_{X}≡*ev*_{⊤}⊣Σ^{!}⊣∀_{X}≡*ev*_{⊥}for any object*X*that has ⊤ and ⊥, by Lemma 5.2, because ⊥⊣!⊣⊤. - In particular, every
*domain*(with ⊥) is compact. - Similarly, all stable domains are compact, since the only icicle to which ⊥ belongs is the whole domain (Example 4.5).

But there are also other compact *pre*domains,
*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

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

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

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.

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.

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

∀_{ℕ}(λ 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}.

This subspace is in general neither open nor closed, but

assuming the Scott principle [D, F]. ▫

- 4
- Unfortunately 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].