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