In this section we prove that focus and description are interdefinable, for the natural numbers. In the following notation, we need to show that φ is a description iff P is prime.
Lemma 10.1 This is a retraction,
cf. the connection between {} and η in [BW85, Lemma 5.1.3] and Lemma C 6.12. ▫
[In fact there is an adjunction or coclosure as shown, since

using the Euclidean principle (Remark 2.4) and the substitution rule for equality.]
First, we characterise the image of Σ^{ℕ}↣Σ^{Σℕ}.
Lemma 10.2 Γ⊢ P:Σ^{2}ℕ is of the form
λ ψ.∃ n.φ[n] ∧ ψ[n]
for some Γ⊢φ:Σ^{ℕ}
iff it preserves ∃_{ℕ}.
In this case, φ=λ n.P(λ m.n=m).
Proof Suppose that P preserves ∃. Then

by the Euclidean principle (Remark 2.4). The other way is easy. ▫
For the rest of this section, P and φ will be related in this way.
Lemma 10.3 P preserves ⊤ iff φ satisfies the existence condition,
and P preserves ∧ iff φ satisfies the uniqueness condition.
Proof For the first, observe that P⊤ ⇔ ∃ n.φ[n]. For the second, if φ[n_{1}]∧ψ_{1}[n_{1}] and φ[n_{2}]∧ψ_{2}[n_{2}] then n_{1}=n_{2}=n by uniqueness. ▫
Proposition 10.4 If P is prime then φ is a description,
and the n.φ[n] satisfies the rules for focusP
(Definition 8.2).
Proof As P is prime, it preserves ⊤, ∧ and ∃ because its double exponential transpose is a homomorphism, in particular with respect to ⊤, ∧ and ∃, as in Proposition 5.5. Also, P=λψ.∃ n.φ[n]∧ψ[n] by the Lemma, so Pψ⇔ψ[the n.φ[n]], which means that the βrules agree. For the ηrules,
φ= 
 ≡(λ m.m=n) iff P=thunkn≡λψ.ψ[n], 
which are respectively a description and prime, and then (the m.φ[m])=(focusP)=n. ▫
Corollary 10.5
Any overt discrete object that admits definition by description is sober.
In particular, all sets and all objects of any topos are sober.
▫
The converse is the case X=ℕ of Theorem 5.7, that if H:Σ^{ℕ}→Σ^{U} is a frame homomorphism (i.e. it preserves ⊤, ∧ and ∃) then it is an Eilenberg–Moore homomorphism. Of course, we showed that for LKLoc, by reinterpreting results from the literature, not for our abstract calculus. The proof below depends on (primitive) recursion, so only applies to ℕ rather than to discrete overt spaces in general, although when the whole theory is in place the result will hold for them too. [It is easy to show that if φ is a description then P preserves ⊤, ⊥, ∧ and ∨; then it is prime by Theorem G 10.2.]
But before considering ℕ we have to deal with 2≡{0,1}. As we did not ask for this as a base type in Section 2, ψ:Σ^{2} may be replaced by <ψ_{0},ψ_{1}>∈Σ×Σ, and similarly for the type of P. (Alternatively, one could formulate a result with ψ:Σ^{ℕ} to capture the same point.) See B 11 for further discussion of disjoint unions in abstract Stone duality.
Proposition 10.6 Let α:Σ be decidable,
with β⇔¬α (Definition 9.11). Then
P ≡ λψ.(α∧ψ[0])∨(β∧ψ[1]) 
is prime. This justifies definition by cases: (if α then 0 else 1)≡focusP.
Proof Let P_{αβ} be the obvious generalisation, so
γ∧ P_{αβ} = P_{(γ∧α)(γ∧β)} 
by distributivity. The equation that we have to prove for Definition 8.1 may be written
(α∨β)∧F P_{αβ} ⇔ (α∧F P_{⊤⊥}) ∨ (β∧F P_{⊥⊤}). 
By the Euclidean principle (Remark 2.4) and the lattice laws, we have

Lemma 10.7 For any description φ, we define, by primitive recursion,
φ^{≥}[0]≡⊤ φ^{>}[n]≡φ^{≥}[n+1]≡φ^{≥}[n]∧¬φ[n] 
φ^{<}[0]≡⊥ φ^{≤}[n]≡φ^{<}[n+1]≡φ^{<}[n]∨φ[n]. 
Then φ^{<}[n] has the properties of the ordinary arithmetic order, that is, (the m.φ[m])< n, and similarly for the others. ▫
Proposition 10.8 If φ is a description then P is prime,
and focusP satisfies the rules for the n.φ[n].
Proof The idea of the proof is to define a permutation f:ℕ≅ℕ that cycles the witness to 0 and any smaller values up by 1, leaving bigger numbers alone. The function f itself is defined by (cases and) primitive recursion, but it only has an inverse with general recursion. Let
f(n) ≡  ⎧ ⎪ ⎨ ⎪ ⎩ 
 δ(n,m) ≡  ⎧ ⎪ ⎨ ⎪ ⎩ 

so δ(n,m) ⇔ f(n)=m. The operations Σ^{f} and I, defined by

are mutually inverse, because, by expanding disjunctions,

Thus Σ^{f} is a homomorphism, as is its inverse I by Proposition 3.5. But so too is evaluation at 0, so
ψ ↦ θ[0] ≡ ∃ n.δ(0,n) ≡ ∃ n.φ[n]∧ψ[n] 
is a homomorphism, and P is prime. The β and ηrules agree as before. ▫
Remark 10.9
Sobriety says that the functor Σ^{(−)}:C^{op}→A
in Definition 4.1 is full and faithful.
But in this proof we only used the fact that it reflects invertibility,
so it suffices to assume that ℕ is replete.
Then f^{−1} is the diagonal mediator that is provided by
the orthogonality property
[Hyl91, Tay91].
Corollary 10.10 H:Σ^{ℕ}→Σ^{U} is an Eilenberg–Moore
homomorphism iff it preserves ⊤, ∧ and ∃. ▫
This result can be extended from ℕ to higher types on the assumption of the continuity axiom (Remark 2.6). Hence there is a version of Theorem 5.7 that links the notions of homomorphism and sobriety that we have introduced entirely abstractly using the λcalculus with those that arise from the ℕindexed lattice structure in Remarks 2.4ff. Although the proof would only require one more section, it begins to make serious use of domaintheoretic ideas, and so properly belongs in a discussion of that subject [F][G]. Besides, surprisingly much progress can be made with the development of topology without the extra axiom.