nLab abstract Stone duality




topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory



Due to Paul Taylor, Abstract Stone Duality (ASD) is a re-axiomatisation of the notions of topological space and continuous function in general topology in terms of a lambda-calculus of computable continuous functions and predicates.

Abstract Stone duality is both constructive and computable, thus being one approach to synthetic topology.

The topology on a space is treated not as a discrete lattice, but as an exponential object of the same category as the original space, with an associated λ-calculus (which includes an internal lattice structure). Every expression in the λ-calculus denotes both a continuous function and a program. ASD does not use the category of sets (or any topos), but the full subcategory of overt discrete objects plays this role (an overt object is the dual to a compact object), forming an arithmetic universe (a pretopos with lists) with general recursion; an optional ‘underlying set’ axiom (which is not predicative) will make this a topos.

The classical (but not constructive) theory of locally compact sober topological spaces is a model of ASD, as is the theory of locally compact locales over any topos (even constructively). In “Beyond Local Compactness” on the ASD website, Taylor removes the restriction of local compactness.


On Dedekind real numbers via abstract Stone duality:

review in:

See also:

Last revised on February 21, 2023 at 11:01:11. See the history of this page for a list of all contributions to it.