By *abstract* Stone duality we mean that the
topology or contravariant powerset functor, seen as a self-adjoint
exponential $\Sigma^{(-)}$ on some category,
is monadic.
Using Beck's theorem, this means that certain equalisers exist
and carry the subspace topology.
These subspaces are encoded by idempotents that play
a role similar to that of nuclei in locale theory.

Paré showed that any elementary topos has this duality, and we prove it intuitionistically for the category of locally compact locales.

The paper is largely concerned with the construction of such a category
out of one that merely has powers of some fixed object $\Sigma$.
It builds on *Sober Spaces and Continuations*,
where the related but weaker notion of abstract sobriety was considered.
The construction is done first by formally adjoining certain equalisers
that $\Sigma^{(-)}$ takes to coequalisers,
then using Eilenberg-Moore algebras,
and finally presented as a lambda calculus similar to
the axiom of comprehension in set theory.

The comprehension calculus has a normalisation theorem, by which every type can be embedded as a subspace of a type formed without comprehension, and terms also normalise in a simple way. The symbolic and categorical structures are thereby shown to be equivalent.

Finally, sums and certain quotients are constructed using the comprehension calculus, giving an extensive category.

Keywords: axiom of comprehension; subtype; typed lambda calculus; Stone duality; subspace topology; locally compact spaces; nucleus of a locale; injective object; monadic adjunction; Beck’s theorem.

2000 MSC: 03E70, 03G30, 06D22, 06E15, 18B05, 18B30, 18C20, 18E10, 54C35, 54D45.

*Theory and Applications of Categories*, Vol. 10, 2002, No. 13, pp 301-368 .

http://www.tac.mta.ca/tac/volumes/10/13/10-13.dvi

http://www.tac.mta.ca/tac/volumes/10/13/10-13.ps

http://www.tac.mta.ca/tac/volumes/10/13/10-13.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/10/13/10-13.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/10/13/10-13.ps