In Section 6, we justified the notion of effective basis in the classical models, i.e. for locally compact sober spaces and locales. This section considers the term model, showing by structural recursion that every definable object has an effective basis. We have already dealt with the base cases (ℕ, Σ^{ℕ}) in Example 6.7, and with Σsplit subobjects in Lemma 7.5. So we consider binary products first (leaving the reader to define the 1indexed basis for 1), but devote most of the section to the exponential Σ^{X}.
Lemma 8.1 If X and Y have effective bases then so
does X× Y, given by Tychonov rectangles.
Proof We are given (β^{n},A_{n}) and (γ^{m},D_{m}) on X and Y. Then, on X× Y, we define

Notice that the formula for F_{(n,m)} is not symmetrical in X and Y, though we have learned to expect properties of binary products to be asymmetrical and problematic [A]. In fact, if A_{n} and D_{m} are filter bases, we have another example of the same problem that held us back in Proposition 5.11, along with the core of its solution.
Lemma 8.2
If A:Σ^{ΣX} and D:Σ^{ΣY} both preserve
either ⊤ and ∧ or ⊥ and ∨ then
A(λ x.D(λ y.θ x y)) ⇔ D(λ y.A(λ x.θ x y)) 
whenever θ:Σ^{X× Y} is a finite union of rectangles.
Proof Applying the Phoa principle (Axiom 3.6) to a single rectangle,

This would have the required symmetry if we had
A(D⊥) ≡ A⊥∨(D⊥∧ A⊤) ⇔ (A⊥∧ D⊤)∨ D⊥ ≡ D(A⊥). 
If A⊤⇔⊤⇔ D⊤ then both sides are A⊥∨ D⊥, whilst if A⊥⇔⊥⇔ D⊥ then they are both ⊥. Under either hypothesis, the lattice dual argument shows the similar result
A(λ x.D(λ y.φ x∨ψ y)) ⇔ D(λ y.A(λ x.φ x∨ψ y)) 
for a cross. The result uses equational induction [E, §2], but we shall just illustrate this with the case where θ is a union of three rectangles,
θ x y ⇔ (φ_{1} x∧ψ_{1} y) ∨ (φ_{2} x∧ψ_{2} y) ∨ (φ_{3} x∧ψ_{3} y). 
If A and D preserve ⊥ and ∨ then A Dθ is also a union of three terms, to each of which the first part applies.
We may also use distributivity of ∨ over ∧ to reexpress the union θ as an intersection of eight crosses,

So if A and D preserve ∧ then A Dθ is a conjunction of eight factors, to each of which the second part applies, for example with φ=φ_{1}∨φ_{2} and ψ=ψ_{3}. In both cases, A Dθ⇔ D Aθ as required. ▫
Remark 8.3 This still awaits
Theorem 9.6 on Scott continuity to extend finite unions of
rectangles to infinite ones, but once we have that we may draw the
corollaries that
We shall need to be able to turn any effective basis into a ∨basis, which we do in the obvious way using finite unions of basic open subobjects. The corresponding unions of compact subobjects give rise to conjunctions of As by Lemma 3. Unfortunately, the result is topologically rather messy, both for products and for objects such as ℝ that we want to construct directly.
Lemma 8.4 If X has an effective basis indexed by
N then it also has a ∨basis indexed by Fin(N). If we were
given a filter basis, the result is one too.
Proof Given any basis (β^{n},A_{n}), define
γ^{ℓ} ≡ λ x.∃ n∈ℓ.β^{n} x D_{ℓ} ≡ λφ.∀ n∈ℓ.A_{n}φ. 
Then φ = ∃ n.A_{n}φ∧β^{n} ≤ ∃ℓ.D_{ℓ}φ∧γ^{ℓ} using singleton lists. Conversely,

Then (γ^{ℓ},D_{ℓ}) is a ∨basis, using list concatenation for +. The imposed order ≼ on Fin(N) is list or subset inclusion,
(ℓ≼ℓ′) ≡ (ℓ⊂ℓ′) ≡ ∀ n∈ℓ.n∈ℓ′. 
Finally, if the A_{n} were filters then so are the D_{ℓ}, since ∀ m∈ℓ preserves ∧ and ⊤. ▫
Remark 8.5
Computationally, it may be better to see this as an embedding
i:X↣Σ^{ΣN} rather than into Σ^{Fin N},
as this gives a very simple representation of the basis and dual basis.
Using the notation π_{ℓ}≡λ n.n∈ℓ and
[ℓ]≡∀ n∈ℓ.ψ n from [E],
which also provides a fixedpoint equation for ∃ℓ, this is:

Lemma 8.6 If an ∧basis was given,
Lemma 8.4 yields a lattice basis.
Proof We are given β^{1}=⊤ and β^{n}∧β^{m}=β^{n⋆ m}.
Let ℓ⋆ℓ′ be the list (it doesn’t matter in what order) of all n⋆ m for n∈ℓ and m∈ℓ′. In functional programming notation, this is
ℓ⋆ℓ′ ≡ flatten (map ℓ (λ n.map ℓ′(λ m.n⋆ m))), 
where map applies a function to each member of a list, returning a list, and flatten turns a list of lists into a simple list. Categorically, map is the effect of the functor List (−) on morphisms, and flatten is the multiplication for the List monad. Using the corresponding notions for K(−), ⋆ can similarly be defined for finite subsets instead.
Now let
β^{ℓ⋆ℓ′} ≡ (∃ n∈ℓ.∃ m∈ℓ′.β^{n⋆ m}) = (γ^{ℓ}∧γ^{ℓ′}) 
by distributivity in Σ^{X}, whilst γ^{{1}}≡β^{1} and D_{{1}}≡ A_{1} (where {1} is the singleton list) serve for γ^{1} and D_{1}. (This uses equational induction, [E, §2].) ▫
Remark 8.7
By switching the quantifiers, we may similarly obtain ∧bases,
and turn an ∨basis into a lattice basis.
In fact, this construction featured in the proof of Theorems 7.8
and 7.14.
This time the filter property is not preserved,
since if A_{n}φ means K^{n}⊂ U then A_{ℓ}φ
means that ∃ n∈ℓ.K^{n}⊂ U,
which is not the same as testing containment of a single compact subobject.
Proposition 12.14 shows how to define an ∧basis
for a locally compact object in which A_{n⋆ m} actually captures
the intersection of the compact subobjects.
Proposition 8.8
N and Σ^{N} have effective bases as follows:

indexed by n:N, ℓ:Fin(N) or L:Fin(Fin(N)). The interchange of sub and superscripts means that we’re reversing the imposed order on these indexing objects (Remark 4.12). ▫
The last of these also provides a basis for Σ^{ΣN}, using Axiom 4.10 twice.
Lemma 8.9 Σ^{ΣN} has a
Fin(Fin N)indexed prime ∧basis with
B^{L}≡A_{L}≡λ Φ.∀ℓ∈ L.Φβ^{ℓ} and A_{L} ≡ η_{Σ2 N}A_{L} ≡λF.F A_{L}, 
so, using Σ^{3} N as a shorthand for a tower of exponentials, Σ^{ΣΣN}≡ (((N→Σ)→Σ)→Σ),
F:Σ^{3} N, Φ:Σ^{ΣN} ⊢ F Φ ⇔ ∃ L:Fin(Fin N). F A_{L} ∧ ∀ℓ∈ L. Φβ^{ℓ}. 
Proof The prime ∧basis on Σ^{N} makes Σ^{ΣN}◁Σ^{Fin(N)} by
Φ↦λℓ.Φβ^{ℓ} and λξ.∃ℓ.Ψℓ∧∀ n∈ℓ.ξ n↤ Ψ, 
so Σ^{3} N◁Σ^{2}Fin(N) by
F↦λ Ψ.F(λξ.∃ℓ.Ψℓ∧∀ n∈ℓ.ξ n) and λ Φ.G(λℓ.Φβ^{ℓ})↤G. 
For any F:Σ^{3} N and Ψ:Σ^{Fin(N)}, let G be obtained from F in this way, and use the prime ∧basis on Σ^{Fin(N)}:

so F = λ Φ.G(λℓ.Φβ^{ℓ}) = λ Φ.∃ L. F A_{L} ∧ ∀ℓ∈ L.Φβ^{ℓ}. ▫
Lemma 8.10
If an object X has an effective basis (β^{n},A_{n}) then
its topology Σ^{X} has a prime lattice basis (D^{L},λ F.Fγ_{L}),
indexed by L:Fin(Fin N), where
γ_{L} ≡ λ x.∃ℓ∈ L.∀ n∈ℓ.β^{n} x and D^{L} ≡ λφ.∀ℓ∈ L.∃ n∈ℓ.A_{n}φ. 
Proof By Lemma 7.4, there is an embedding i:X↣Σ^{N} with Σsplitting I by
i x ≡ λ n.β^{n} x and Iφ ≡ Φ ≡ λξ.∃ n.A_{n}φ∧ξ n, so φ = λ x.Φ(i x). 
For F:Σ^{ΣX}, let F ≡ F·Σ^{i} ≡ λΨ.F(λ x.Ψ(i x)) :Σ^{3} N, so F· I=F·Σ^{i}· I=F. Then

since the given formulae are γ_{L}=Σ^{i} A_{L} and D^{L}=λφ.∀ℓ∈ L.Iφβ^{ℓ}. ▫
Theorem 8.11
Every definable (or locally compact, cf. Remark 6.3)
object X has a lattice basis, indexed by Fin(Finℕ),
and is a Σsplit subobject of Σ^{ℕ}.
Moreover, Σ^{X} is stably locally compact,
as it has a prime lattice basis (cf. Proposition 6.16). ▫
Remark 8.12 This is a “normal form” theorem, and, like all such
theorems, it can be misinterpreted.
It is a bridge over which we may pass in either direction
between λcalculus and a discrete encoding of topology,
not an intention to give up the very pleasant synthetic results
that we saw in [C].
In particular, we make no suggestion that either arguments in topology
or their computational interpretations need go via
the list or subset representation
(though [JKM99] seems to have this in mind).
Indeed, subsets may instead be represented by λterms
[E].
It is simply a method of proof, and is exactly what we need
to connect synthetic abstract Stone duality
with the older latticetheoretic approaches to topology,
as we shall now show.