Our new notion of sobriety, expressed in terms of the λcalculus rather than lattice theory, is a weaker form of the fundamental idea of the abstract Stone duality programme.
Definition 4.1
When the category C of types of values is dual to
its category Alg of algebras of observations,
we say that (C,Σ) is monadic.
More precisely, the comparison functor C^{op}→Alg
defined by Lemmas 3.3 and 3.6,
(which commutes both with the left adjoints and with the right adjoints) is to be an equivalence of categories, i.e. full, faithful and essentially surjective.
Remark 4.2
It is possible to characterise several weaker conditions than
categorical equivalence, both in terms of properties of the objects of C,
and using generalised “mono” requirements on η_{X}.
In particular,
the functor C^{op}→A is faithful iff all objects are “ T_{0}”
(cf. Remark 1.13),
and also reflects invertibility iff they are replete
[Hyl91, Tay91].
Another way to say this is that each η_{X} is mono or extremal mono,
and a third is that Σ is a weak or strong cogenerator.
For example, ℕ with primitive recursion is T_{0} so long as the calculus is consistent, but repleteness and sobriety are equivalent to general recursion [for decidable predicates] (Sections 9–10).
In this paper we are interested in the situation where the functor is full and faithful, i.e. that all homomorphisms are given uniquely by Lemma 3.6. We shall show that the corresponding property of the objects is sobriety, and that of η_{X} is that it be the equaliser of a certain diagram.
Lemma 4.3
Let (A,α) be an algebra, Γ any object
and H:A→Σ^{Γ} any map in C.
Then H is a homomorphism iff its double exponential transpose
P:Γ→Σ^{A} (Proposition 2.11) has equal composites
Proof We have H=η_{A};Σ^{P} and P=η_{Γ};Σ^{H}. [⇒] P;Σ^{α}=η_{Γ};Σ^{H};Σ^{α}=η_{Γ};Σ^{2}η_{Γ};Σ^{3} H =η_{Γ};η_{Σ2 Γ};Σ^{3} H=η_{Γ};Σ^{H};η_{Σ A} =P;η_{Σ A}. [⇐] α;H=α;η_{A};Σ^{P}=η_{Σ2 A};Σ^{2}α;Σ^{P} =η_{Σ2 A};Ση_{Σ A};Σ^{P}=Σ^{P} =Σ^{2}η_{A};Ση_{Σ A};Σ^{P} =Σ^{2}η_{A};Σ^{3} P;Ση_{Γ}=Σ^{2} H;Ση_{Γ}. ▫
Corollary 4.4
The (global) elements of the equaliser are the those functions
A→Σ that are homomorphisms. ▫
Definition 4.5 Such a map P is called prime.
(We strike through the history of uses of this word, such as in
Definition 1.7 and Corollary 5.8.
In particular, although the case X=ℕ will turn out to be
the most important one, we are not just talking about
the numbers 2, 3, 5, 7, 11, ...!)
As we always have A=Σ^{X} in this paper,
we usually write P as a term Γ⊢ P:Σ^{ΣX}.
Lemma 4.6
In Lemma 4.3, η_{X} is the prime
corresponding to the homomorphism id:Σ^{X}→Σ^{X}.
If P:Γ→Σ^{A} is prime and J:B→ A a homomorphism
then P;Σ^{J} is also prime.
In particular, composition with Σ^{2} f preserves primes.
▫
Definition 4.7
We say that an object X∈obC is sober if the diagram
is an equaliser in C, or, equivalently, that the naturality square
for η with respect to η_{X} is a pullback.
Remark 4.8 We have only said that
the existing objects can be expressed as equalisers,
not that general equalisers can be formed.
In fact, this equaliser is of the special form described below,
which Jon Beck exploited to characterise monadic adjunctions
[Mac71, Section VI 7], [BW85, Section 3.3],
[Tay99, Section 7.5].
The category will be extended to include such equalisers,
so we recover a space pts(A,α) from any algebra,
in [B].
Notice the double role of Σ here, as both a space and an algebra. Peter Johnstone has given an account of numerous well known dualities [Joh82, Section VI 4] based the idea that Σ is a schizophrenic object. (This word was first used by Harold Simmons, in a draft of [Sim82], but removed from the published version.)
Moggi [Mog88] called sobriety the equalizing requirement, but did not make essential use of it in the development of his computational monads.
Applegate and Tierney [Eck69, p175] and Barr and Wells [BW85, Theorem 3.9.9] attribute these results for general monads to Jon Beck. See also [KP93] for a deeper study of this situation.
Proposition 4.9 Any power, Σ^{U}, is sober.
Proof This is a split equaliser: the dotted maps satisfy

by Lemma 2.10, the equations on the right being naturality of η with respect to Σ^{ηU} and η_{ΣU}. Hence if P:Γ→Σ^{3} U has equal composites then P=P;Σ^{ηU};η_{ΣU}, and the mediator is P;Σ^{ηU}. ▫
Theorem 4.10
The functor Σ^{(−)}:C^{op}→Alg given in Definition 4.1
is full and faithful iff all objects are sober.
Proof [⇒] We use P:Γ→Σ^{2} X to test the equaliser. By Lemma 4.3, its double transpose H:Σ^{X}→Σ^{Γ} is a homomorphism, so by hypothesis H=Σ^{f}=η_{ΣX};Σ^{P} for some unique f:Γ→ X, and this mediates to the equaliser.
[⇐] Let H:Σ^{X}→Σ^{Γ} be a homomorphism, so the diagram on the left above commutes, as do the parallel squares on the right, the lower one by naturality of Σ^{η} with respect to H. Since X is the equaliser, there is a unique mediator f:Γ→ X, and we then have H=η_{ΣX};Σ^{P}=η_{ΣX};Ση_{X};Σ^{f}=Σ^{f}. ▫
Remark 4.11
Translating Definition 1 into the λcalculus,
the property of being a homomorphism H:Σ^{X}→Σ^{U}
can be expressed in a finitary way
as an equation between λexpressions,
F:Σ^{3} X⊢(λ u.F(λφ.Hφ u)) = H(λ x.F(λφ.φ x)), 
the two sides of which differ only in the position of H.
The double exponential transpose P of H is obtained in the λcalculus simply by switching the arguments φ and u (cf. Remark 1.11). Hence ⊢ P:U→Σ^{ΣX} is prime iff
u:U, F:Σ^{3} X ⊢ F(P u) = P u(λ x.F(λφ.φ x)). 
Replacing the argument u of P by a context Γ of free variables, Γ⊢ P:Σ^{ΣX} is prime iff
Γ, F:Σ^{3} X ⊢ F P ⇔ P(λ x.F(λφ.φ x)) 
or F P ⇔ P(η_{X};F). This is the equation in Lemma 4.3, with A=Σ^{X}, applied to F.
[In the context of the additional lattice structure, including Scott continuity, P is prime iff it preserves ⊤, ⊥, ∧ and ∨ Theorem G 10.2.]
Corollary 4.12 The type X is sober iff
for every prime Γ⊢ P:Σ^{2} X
there is a unique term Γ⊢focusP:X such that
Γ, φ:Σ^{X} ⊢ φ(focusP) ⇔ Pφ. 
Hence the sidecondition on the introduction rule for focusP in Remark 2.12 is that P be prime. Indeed, since φ↦φ x is itself a homomorphism (for fixed x), this equation is only meaningful in a denotational reading of the calculus when P is prime. (On the other hand Thielecke’s force operation has this as a βrule, with no side condition, but specifies a particular order of evaluation.) ▫
Remark 4.13 So far, we have used none of the special structure on Σ in
Remarks 2.4ff. We have merely used the restricted
λcalculus to discuss what it means for the other objects of
the category to be sober with respect to it.
In Sections 6–8
we shall show how to enforce this kind of sobriety on them.
If P=η_{X}(x) then the right hand side of the primality equation easily reduces to the left. Otherwise, since F is a variable, the left hand side is headnormal, and so cannot be reduced without using an axiom such as the Euclidean principle (Remark 2.4), as we shall do in Proposition 10.6.
The introduction of subspaces [B][E] also extends the applicability of the equation, by allowing it to be proved under hypotheses, whilst using the continuity axiom (Remark 2.6) it is sufficient to verify that P or H preserves the lattice connectives. In other words, the mathematical investigations to follow serve to show that the required denotational results are correctly obtained by programming with computational effects.
Remark 4.14 In his work on continuations, Hayo Thielecke uses R
for our Σ and interprets it as the answer type.
This is the type of a subprogram that is called like a function,
but, since it passes control by calling another continuation,
never returns “normally” — so the type of the answer is irrelevant.
Thielecke stresses that R
therefore has no particular properties or structure of its own.
In the next section, we shall show that the Sierpiński space in topology behaves categorically in the way that we have discussed, but it does carry additional latticetheoretic structure.
Even though a function or procedure of type void never returns a “numerical” result — and may never return at all — it does have the undisguisable behaviour of termination or nontermination. Indeed, we argued in Remark 1.2 that termination is the ultimate desideratum, and that therefore the type of observations should also carry the lattice structure. Proposition 10.6, which I feel does impact rather directly on computation, makes use of both this structure and the Euclidean principle.
[The referee pointed out that there are, in practice, other computational effects besides nontermination, such as input–output.]
Thielecke’s point of view is supported by the fact that the class of objects that are deemed sober depends rather weakly on the choice of object Σ: in classical domain theory, any nontrivial Scott domain would yield the same class.
Remark 4.15 Although it belongs in general topology, sobriety was first
used by the Grothendieck school in algebraic geometry
[AGV64, IV 4.2.1]
[GD71, 0.2.1.1] [Hak72, II 2.4].
They exploited sheaf theory, in particular the functoriality of
constructions with respect to the lattice of open subsets, the points
being secondary.
An algebraic variety (the set of solutions of a system of polynomial equations) is closed in the Euclidean topology, but there is a coarser Zariski topology in which they are defined to be closed. When the polynomials do not factorise, the closed set is not the union of nontrivial closed subsets, and is said to be irreducible. A space is sober (classically) iff every irreducible closed set is the closure of a unique point, known in geometry as the generic point of the variety. Such generic points, which do not exist in the classical Euclidean topology, had long been a feature of geometrical reasoning, in particular in the work of Veronese (c. 1900), but it was Grothendieck who made their use rigorous.