Making use of the availability of bases for all definable objects, this section establishes the basic properties that justify the claim that abstract Stone duality is an account of domain theory and general topology, at least in so far as its morphisms are continuous functions. We first prove something that was claimed in Remark 4.8.
Proposition 9.1
Let M be an overt discrete object with effective basis
(β^{n},A_{n}) indexed by an overt discrete object N.
Then M is the subquotient of N by an open partial equivalence relation.
Proof Write n⊩ x for n:N, x:M ⊢ A_{n}{x}∧ β^{n} x (using discreteness of M) and N′={n ∣ ∃ x.n⊩ x}⊂ N, which is open, using overtness.
Then, using the basis expansion of open {x},
⊤ ⇔ (x=_{M} x) ⇔ 
 (x) ⇔ ∃ n.A_{n} 
 ∧β^{n} x ⇔ ∃ n.n⊩ x, 
so every point x:M has some code n:N′. The latter belongs only to x since

Hence N′→Σ^{M} by n↦λ x.n⊩ x factors through {}:M↣Σ^{M}, and M is N/∼ where (m∼ n)≡(∃ x.m⊩ x∧ n⊩ x) [C]. ▫
We leave it as an exercise to define partial equivalence relations on List (N) whose quotients are List (M) and K(M).
Corollary 9.2 Every definable overt discrete object
is a subquotient of ℕ by an open partial equivalence relation. ▫
This does not restrict how “big” overt discrete objects can be in general models of ASD: for example, ℵ_{1} still belongs to the classical model. It simply says that, having required certain base types to be overt discrete, as we did with ℕ in Axiom 4.4, the additional overt discrete objects that can be constructed from them are no bigger.
Corollary 9.3 In the free model, if an object X has a basis indexed by any
overt discrete object M then it has one indexed by ℕ.
Proof Let n:ℕ, m:M⊢ n⊩ m be the relation defined in the Proposition and (β^{m},A_{m}) the basis on X. Define
γ^{n} ≡ λ x.∃ m.n⊩ m∧β^{m} x and D_{n} ≡ λφ.∃ m.n⊩ m∧ A_{m}φ. 
So γ^{n}=β^{m} and D_{n}=A_{m} if n⊩ m, but γ^{n}=⊥ and D_{n}=⊥ if n∉ N′. Then, using the properties of ⊩, (γ^{n},D_{n}) is an effective basis because

The next goal is Scott continuity, i.e. preservation of directed joins. Recall from Definition 4.13 that these are defined in terms of a structure (S,0,+) that indexes two families
s:S ⊢ α_{s}:Σ and φ^{s}:Σ^{X}. 
Lemma 9.4 Γ, ℓ:Fin(M) ⊢
(∀ m∈ℓ.∃ s:S.α_{s}∧φ^{s} m) ⇔
(∃ s:S.α_{s}∧∀ m∈ℓ.φ^{s} m) .
Proof We have to show ⇒, as ⇐ is easy. For the base case, ℓ≡ 0, put s≡ 0. For the induction step, ℓ′=m::ℓ, suppose by the induction hypothesis that
α_{t}∧φ^{t} m ∧ α_{s}∧∀ m∈ℓ.φ^{s} m 
Put u≡ s+t:S, so α_{u}⇔α_{s+t}⇔α_{s}∧α_{t} and φ^{s},φ^{t}≤φ^{u}, so we have α_{u}∧∀ m∈m::ℓ.φ^{u} m.
This proof is for lists, but a similar induction scheme works for subsets too, cf. [Tay99, Section 6.5]. Since this equational hypothesis is of the form σ⇔⊤, it can be eliminated in favour of an open subobject of the context [E, §2]. ▫
Lemma 9.5
Any Γ⊢F:Σ^{3} N preserves the directed join
Γ⊢∃ s.α_{s}∧ Φ^{s}:Σ^{ΣN}.
Proof Using the previous lemma for X≡ Σ^{N} and M≡Fin N,

Theorem 9.6 Any Γ⊢ F:Σ^{ΣX}
preserves the directed join ∃ s.α_{s}∧φ^{s}:Σ^{X}.
Proof Making the same substitutions as in Lemma 8.10,

Corollary 9.7 All F:Σ^{Y}→Σ^{X} preserve directed joins. ▫
We can now see the construction in Lemma 8.10 as a composite, of Lemma 8.4 twice and the following result. In order to apply F:Σ^{ΣX} to the basis decomposition of φ:Σ^{X}, the decomposition must be a directed join.
Lemma 9.8 If X has a ∨basis then
Σ^{X} has a prime ∧basis.
Proof For F:Σ^{ΣX} and φ:Σ^{X}, since the ∨basis gives a directed join,
Fφ ⇔ F(∃ n.A_{n}φ∧β^{n}) ⇔ ∃ n.A_{n}φ∧ Fβ^{n}. 
This is the decomposition of F with respect to the prime ∧basis with
B^{n} ≡ A_{n} and A_{n} ≡ λ F.Fβ^{n}. 
Notice that it reverses the imposed order on the indexing object. ▫
We can also go up to the second exponential with just one level of lists.
Lemma 9.9 Let (β^{n},A_{n}) be a ∨basis for X.
Then
B^{ℓ}≡λ F.∀ n∈ℓ.Fβ^{n} and A_{ℓ}≡λF.F(λφ.∃ n∈ℓ.A_{n}φ) 
define a prime ∧basis for Σ^{ΣX}, i.e. we have a basis decomposition
F:Σ^{3} X ⊢ F = λ F.∃ℓ. F(λφ.∃ n∈ℓ.A_{n}φ)∧∀ n∈ℓ.Fβ^{n}. 
Proof (A_{n},λ F.Fβ^{n}) is a basis and (λφ.∃ n∈ℓ.A_{n}φ, λ F.∀ n∈ℓ.Fβ^{n}) an ∨basis for Σ^{X} by Lemmas 9.8 and 8.4. Finally, Lemma 9.8 gives the prime ∧basis for Σ^{ΣX}. ▫
As a corollary, we have another result similar to Corollary 9.2, although this one does restrict the size of overt discrete compact objects. Such objects are called Kuratowski finite: see [E] for more detail. Beware that even finiteness is not the same as being a numeral, for example a Möbius band has a finite set of edges that is locally equal to 2, but this set is not a numeral.
Theorem 9.10
An object N is overt discrete compact iff it is listable,
and therefore a quotient of a numeral by an open equivalence relation.
Proof Expanding the quantifier ∀_{N} using the filter ∨basis for N indexed by List N,
∀_{N}φ ⇔ ∃ℓ.∀ n.n∈ℓ∧∀ m∈ℓ.φ m, 
so ⊤⇔∀_{N}⊤⇔∃ℓ.∀ n.n∈ℓ. The numeral is (the length of) ℓ, though we require the Existence Property (cf. Remark 4.11) to pin down its order and so make it a quotient of a numeral. ▫
As another corollary, we can complete the business of Proposition 5.11 and Lemma 8.2.
Theorem 9.11 Let A:Σ^{Y}→Σ^{X} and B:Σ^{V}→Σ^{U}.
commute. Hence × is a symmetric monoidal structure in the category whose objects are those of S and whose morphisms A:X−× Y are the A that preserve ⊤ and ∧, cf. Section A 3. In particular, these maps commute with ∀_{K}, for any compact K.
Proof Lemma 8.2 and Theorem 9.6. ▫
Corollary 9.12 Closed and compact subobjects coincide in any compact Hausdorff
object, whilst open and overt ones agree in any overt discrete object. ▫