nLab abstract Stone duality




Due to Paul Taylor, Abstract Stone Duality (ASD) is a reaxiomatisation of the notions of topological space and continuous function in general topology in terms of a lambda-calculus of computable continuous functions and predicates that is both constructive and computable. It thus forms 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.


Last revised on May 6, 2020 at 18:20:29. See the history of this page for a list of all contributions to it.