abstract Stone duality

Due to Paul Taylor, Abstract Stone Duality (ASD) is a reaxiomatisation of the notions of space and map in general topology in terms of a λ-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). Taylor has recently removed the restriction of local compactness.

Revised on October 20, 2016 05:10:02
by David Corfield
(129.12.18.176)