Foundations for Computable TopologyPaul Taylor 
This paper is an introduction to Abstract Stone Duality, in particular its philosophical methodology and the underlying ideas from category theory and Stone duality. An abridged version will appear in Foundational Theories of Classical and Constructive Mathematics, edited by Giovanni Sommaruga and published by SpringerVerlag (BibTeX).
Foundations should be designed for the needs of mathematics and not vice versa. We propose a general technique for doing this that exploits mathematical results in categorical logic and the duality between algebra and geometry. This paper is a survey of the application of this technique to devising a revolutionary reaxiomatisation of general topology called Abstract Stone Duality. The Sierpinski space plays a key role as the classifier for both open and closed subspaces. ASD is inherently computable, and has a very strong duality between open and closed concepts. It provides a purely recursive theory of elementary real analysis in which, unlike in previous approaches, the real closed interval [0,1] in ASD is compact.
Acknowledgements I would like to thank I would like to thank Andrej Bauer, David Corfield, Anders Kock, Fred Linton, Gabor Lukasz, Andy Pitts, Sridhar Ramesh, Guiseppe Rosolini, Giovanni Sommaruga, Hayo Thielecke and Graham White for their very helpful comments on earlier drafts of this paper.
@incollection{TaylorP:fofct, author = {Taylor, Paul}, title = {Foundations for Computable Topology}, editor = {Sommaruga, Giovanni}, booktitle = {Foundational Theories of Classical and Constructive Mathematics}, year = 2011, month = {January}, number = 76, publisher = {SpringerVerlag}, series = {Western Ontario Series in Philosophy of Science}, isbn = {9789400704305}, url = {PaulTaylor.EU/ASD/foufct}}

Download the paper to print it PDF, DVI, compressed PostScript or A5 booklet.
Table of contents and the HTML version The HTML version is not up to date; it will be revised when the paper is finished and the book goes to print.
Introduction, elimination, beta and eta rules for logical connectives, and their relationship to adjunctions in category theory. Building a category from a type theory. From headline theorems to adjunctions to introduction etc rules for new logical connectives to the new theory and its computational interpretation. Critique of the Euclid–Bourbaki style and of the traditional category of “topological spaces”, here called “Bourbaki spaces”. The duality between algebra and geometry. Locale theory. Expressing Stone duality using lambdacalculus and a monad. Beck’s theorem; Sigmasplit subspaces and their applications. Categorical and typetheoretic formulation of Stone duality in this abstract form. Primes, sobriety, nuclei. Classifiers for subsets, open subspaces and closed subspaces. The Euclidean and Phoa principles.
Development of the lambda calculus for topology including the lattice structure and Euclidean or Phoa principles. The Euclidean principle makes Sigma a dominance. Discrete, Hausdorff, compact and overt spaces. Partial map classifier. Pretoposes and arithmetic universes. Overt discrete spaces as sets. Recursion, induction and the need for equalisers. ASDstyle characterisation of elementary toposes. General recursion (minimalisation). The (noncomputable) underlying set axiom. Overt discrete spaces form a topos. Comparing the monads. Formulations of Scott continuity in denotational semantics, elementary real analysis and locale theory. Characterisation and properties of locally compact spaces. Application to real analysis. This section has been completely rewritten, but is currently available only in the PDF, DVI and PS versions above; the HTML version of the old text has been removed.

This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.