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 overtdiscrete 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 compactsobertopological 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.