Now we relate subspaces as we have just described them to Stone duality as presented in Section 1. In the abstract setting, the diagrams shown there are as follows, where Alg is the category of Eilenberg–Moore algebras for the monad induced by the adjunction Σ^{(−)}⊣Σ^{(−)}.
We shall show that subspaces (i.e. certain equalisers) exist in S and carry the subspace topology iff (idempotents split and) the functor S^{op}→Alg is an equivalence of categories. This functor is full and faithful iff all objects are sober (Theorem A 4.10), so our task in this paper is to say when it is essentially surjective. In fact we shall construct the pseudoinverse functor. The argument works though the proof of Beck’s theorem in our special case.
Definition 3.1
An algebra (A,α) is spatial if
there is some algebra isomorphism
Recall from Lemma A 4.3 that a map H:A→Σ^{U} (not necessarily an isomorphism) is a homomorphism iff its double exponential transpose P has equal composites
so our first attempt at spatiality of (A,α) is to form this equaliser [Fak70]. Afterwards we have to find out when H is an isomorphism.
Proposition 3.2
The contravariant functor X↦(Σ^{X},Ση_{X}):S^{op}→Alg
has a symmetric adjoint on the right, called pts, so
iff for each algebra (A,α) the equaliser
exists in S.
Proof By the foregoing argument, there must also be a correspondence with maps
but this is just the universal property of the equaliser. ▫
The inverse functor pts:Alg→S^{op} takes the algebra A to the “set” Alg(A,Σ) of homomorphisms, just as the forward one took the object X to the functionspace S(X,Σ). (Remark 7.4 explains how Alg(A,B) can sometimes be defined as an object of S, rather than as an external homset.)
Theorem 3.3
The contravariant adjunction of
Σ^{(−)} and pts is an equivalence between S^{op} and
Alg iff all objects of S are sober and all algebras in Alg
are spatial.
Proof Sobriety and spatiality merely say that the units of the symmetric adjunction,
X→pts(Σ^{X},Σ^{ηX}) and H:A→Σ^{pts A}, 
are isomorphisms. ▫
More particularly, without assuming that all objects are sober, the functor pts:Alg^{op}→S is full and faithful (making Alg^{op} reflective in S) iff all algebras are spatial. Joachim Lambek and Basil Rattray considered this situation abstractly (writing Q A for our Σ^{pts A}), together with applications to Abelian categories and elementary toposes [LR75]. More recently, Giuseppe Rosolini connected their results with topos models of synthetic domain theory [BR98a].
We can characterise spatiality in terms more like those of the previous section.
Proposition 3.4
(A,α)≅Σ^{X} iff
there are i:X→Σ^{A} and I:Σ^{X}→Σ^{2} A such that
i is prime, I;Σ^{i}=id_{ΣX} and Σ^{i};I=α;η_{A}≡η_{Σ2 A};Σ^{2}α. 
In this case, i:X=pts(A,α)→Σ^{A} is the equaliser in Proposition 3.2, and Σ^{(−)} takes it to a split coequaliser.
Proof If H:A≅Σ^{X} is an isomorphism of algebras then its double exponential transpose i ≡ η_{X};Σ^{H} is prime, and we may put I ≡ H^{−1};η_{A}=η_{ΣX};Σ^{2} H^{−1}. Then
I;Σ^{i} = η_{ΣX};Σ^{2} H^{−1};Σ^{2} H;Σ^{ηX} = η_{ΣX};Σ^{ηX} = id 
Σ^{i};I = Σ^{2} H;Σ^{ηX};H^{−1};η_{A} = α; H;H^{−1};η_{A} = α; η_{A}. 
Conversely, if i is prime then its double transpose H≡η_{A};Σ^{i} is a homomorphism, and H^{−1}=I;α because
η_{A};Σ^{i};I;α = η_{A};α;η_{A};α = id 
I;α;η_{A};Σ^{i} = I;η_{Σ2 A};Σ^{2}α;Σ^{i} = I;η_{Σ2 A};Σ^{ηΣA};Σ^{i} = I;Σ^{i} = id 
since i, being prime, has equal composes with Σ^{α} and η_{ΣA}.
To show that X is the equaliser, consider P:Γ→Σ^{A}⇉Σ^{3} A. The double transpose K:A≡Σ^{X}→Σ^{Γ} of P is a homomorphism, so, since X is sober, K=Σ^{k}, where k:Γ→ X mediates to the equaliser. The image of the equaliser diagram under Σ^{(−)} is the split coequaliser shown above. ▫
Remark 3.5 In the λcalculus, these equations are

The ηequation, which says that Σ^{X} is a retract of A, was discussed in the previous section: it makes X a Σsplit subspace of Σ^{A}.
The βequation makes H:A↣Σ^{X} a subalgebra that is “Usplit” in Beck’s language, i.e. split by a function that need not be a homomorphism. This property says that there are enough points to distinguish the elements of A, considered as “open subsets” of X.
Remark 3.6 The same caveat applies to our definition of “spatial” algebras
as to that of “sober” spaces in
Remark A 5.10:
the correspondence with the latticetheoretic notion in
[Joh82, Section II 1.5]
is a conceptual one rather than a theorem.
In particular, recall from [Joh82, Theorem VII 4.3] that
(using the axiom of choice) any distributive continuous lattice A
has enough points (completely coprime filters) in the classical sense.
All algebras over LKLoc are spatial in the constructive sense that
there are enough generalised “points”
Γ→pts(A,α), cf. [Vic95].
Beck’s theorem and our treatment of subspaces consider the maps and equations in the main equaliser diagram, without requiring the objects to be Σ^{2} A, Σ^{3} X, etc.
Definition 3.7
A parallel pair u,v:Y⇉ Z in S
is called a Σsplit pair
if there is some map (not necessarily a homomorphism) J:Σ^{Y}→Σ^{Z}
such that
J;Σ^{u} = id_{ΣY} and Σ^{u};J;Σ^{v} = Σ^{v};J;Σ^{v}. 
Notice that we just mark one of the maps with a hook, to emphasise the fact that the conditions are not symmetrical in u and v.
It is helpful to see these equations expressed in other ways. Using Notation 2.11, they are
u; 
 = id and v; 
 ;u = v; 
 ;v. 
Mixing application with categorical composition, we have
u;J(ψ) = ψ and v;J(u;θ) = v;J(v;θ). 
Using the λcalculus, the equations are

We shall need the equaliser i:X→ Y of u and v, for which we would like Σ^{i}:Σ^{Y}→Σ^{X} also to be the coequaliser of Σ^{u} and Σ^{v}. In this case there is a (unique) map I:Σ^{X}→Σ^{Y} with I;Σ^{i}=id_{ΣX} and Σ^{i};I=J;Σ^{v}.
Reversing the arrows, there is a similar notion of Σsplit coequaliser (Section 11), whilst (unqualified) split equalisers and coequalisers also arise, in which the equations already hold at the base level, without applying the functor Σ^{(−)}. Split (co)equalisers are absolute in the sense that, being equationally defined, they are preserved by all functors. Absolute coequalisers were first studied by Robert Paré [Par71]. Examples of absolute pushouts may be found in Section 7, [Tay99, Exercise 5.3] and [D].
We construct the equaliser of a split pair by splitting an idempotent (Remark 4.1). In particular, Σ^{X} splits E ≡ Σ^{v};J. Conversely, any idempotent e:Y→ Y gives rise to a split pair (e,id), with J ≡ E ≡ Σ^{e}, so such splittings are necessary.
There is no greater generality in supposing that i is split only after further iteration of the functor Σ^{(−)}, since if I;Σ^{3} i=id then I;Σ^{i}=id by the unit law, where I ≡ η_{ΣX};I;Σ^{ηY}.
Proposition 3.8
If the functor pts exists,
all objects are sober and idempotents split, then
S has equalisers of all Σsplit pairs.
If, additionally, all algebras are spatial,
Σ^{(−)} takes these equalisers to (split) coequalisers.
Conversely, if S has equalisers of all Σsplit pairs, and Σ^{(−)} takes them to coequalisers, then all algebras are spatial.
Proof Let u,v:Y⇉ Z have splitting J:Σ^{Z}→Σ^{Y}, so that E ≡ Σ^{v};J is an idempotent on Σ^{Y}, and let A be its splitting, as in the top rows of the diagrams. Since this coequaliser is absolute, Σ^{2} A is also a coequaliser, so the structure α may be obtained as the mediator; similar arguments involving Σ^{4}A show that it satisfies the equations for an Eilenberg–Moore algebra.
I claim that pts(A,α) is the equaliser of u and v.
All composites pts(A,α)→Σ^{4} Y are equal, so they factor through η_{Y} since Y is sober. This defines the dotted map. It has equal composites with u and v because all composites pts(A,α)→Σ^{2} Z are equal and η_{Z} is mono.
Any test map Γ→ Y having equal composites with u and v also has equal composites with Σ^{2} u and Σ^{2} v, since η is natural, so it factors through their equaliser, Σ^{A}. For the same reasons it has equal composites with Σ^{A}⇉Σ^{3} A, and so factors through their equaliser pts(A,α). The mediator is unique because i and Σ^{q} are mono.
Now apply Σ^{(−)} to the lefthand diagram, so Σ^{pts(A,α)}≅ A and Σ^{i}≅α by Theorem 3.3 since A is spatial. Then Σ^{(−)} takes the top two rows of the diagram on the left to the one on the right.
Since pts is itself a Σsplit equaliser, the converse follows from Proposition 3.4. ▫
Remark 3.9 Because of the fact that Σ^{(−)} takes it
to the coequaliser of Σ^{Y}⇇Σ^{Z},
the diagram X→ Y⇉ Z is also an equaliser in HS,
i.e. with respect to “second class” test maps
F:Γ−× Y⇉ Z (Notation 2.11).
This is in contrast to the situation for products, where the failure of the extension of the universal property from S to HS is essentially related to the interpretation of computational effects [Thi97a]. The fact that equalisers are valid even in the presence of such effects may be regarded as the categorical justification of the use of Floyd–Hoare logic for imperative as well as functional programs.
It is still not clear precisely what the exactness properties of Σ^{(−)} should be, as not all equalisers are taken to coequalisers:
Example 3.10 (Steven Vickers) Suppose that S has disjoint coproducts,
as is the case for Set and LKSp,
and also in the abstract situation by Theorem 11.8.
Then
is an equaliser (where swap interchanges the elements of 2), but Σ^{(−)} takes it to
where swap interchanges the components of the product. ▫
We can now prove the intuitionistic form of Stone duality for locally compact locales.
Theorem 3.11
LKLoc is monadic.
Proof We must show that every object is sober, that equalisers of Σsplit pairs exist, and that Σ^{(−)} takes them to coequalisers. Recall from the theory of locales and continuous lattices [GHK++80, Joh82] that the topology on a locally compact locale is a distributive continuous lattice, whilst the category Cont of continuous lattices and Scott continuous functions is fully embedded (via the Scott topology) as a subcategory of LKLoc that is closed under retracts.
The equaliser diagram of locales involved in the definition of sobriety gives rise to diagram of frames shown above, where ↞ denotes a frame homomorphism and ↣ a Scott continuous function. This is a split coequaliser in Cont and so ā fortiori a coequaliser in LKFrm, i.e. an equaliser in LKLoc.
Now let u,v:Y⇉ Z be a Σsplit pair in LKLoc. We follow it around the diagram of categories and functors above.
E ≡ J;Σ^{v} is a Scott continuous idempotent on the continuous frame Σ^{Y}, so it is split by some continuous lattice Q. Hence
is a split coequaliser diagram in LKLoc, although we may just as well see it as being in Cont or Set.
The forgetful functor U:Frm→Set, being monadic [Joh82, Theorem II 1.2], creates this coequaliser in Frm, so the lattice Q is actually a frame, and the map Σ^{Y}↠ Q is a frame homomorphism. This means that Q≅Σ^{X} for some locale X, which is locally compact since Q is continuous, and q ≡ Σ^{i}. Hence the diagram is a coequaliser in LKFrm, so X is the equaliser in LKLoc, which Σ^{(−)} takes to the original split coequaliser. ▫
We conclude our introductory discussion with an example of a nonspatial algebra.
Classically, the twopoint set classifies subsets in Set, open subsets in LKSp (when it is given the Sierpiński topology), and upper subsets in Pos (when it is given the order ⊥<⊤). The monad may therefore be defined on Pos using this object, which we call Υ.
Example 3.12 In (Pos,Υ), all objects are
sober classically but not intuitionistically
(Remark C 5.10(c)). Pos does not have the monadic
property, because the unit interval, A=[0,1] with the usual
arithmetical order, is an Eilenberg–Moore algebra (in a unique way)
that does not have enough points.
This discussion of [0,1] extends that in [FW90, Example 9]. In fact, the algebras for this version of the monad are constructively completely distributive lattices [MRW02].
Proof Classically, the upper sets of A are of the form (a,1] or [a,1]. Indeed Σ^{A· n}=A^{op}·(n+1), where A· n is A×n with the lexicographic order: <a,i>≤<b,j> if a< b, or a=b and i≤ j.
The maps we’re interested in act as the identity on the real part, and as shown above on the numerical part. ▫