Drafts of two new papers on Abstract Stone Duality are now available, and I would very much appreciate your comments about them. Computably based locally compact spaces An elementary theory of the category of locally compact locales http://www.di.unito.it/~pt/ASD These two papers bring ASD into line with the "official" theory of locally compact sober spaces and locales, in two completely different ways. The ASD "Manifesto" was also revised recently. =================================== Computably based locally compact spaces The first paper shows that the main version of ASD is equivalent to the category of "computably based" locally compact locales, and computably continuous functions. By a "basis" I mean a family of open subspaces U^n and accompanying family of compact subspaces K^n, the topological information being captured by the inclusion relation K^n subset U^m. For locales the corresponding idea is the "way below" relation. The finitary properties of this are characterised, including in particular the "Wilker condition" concerning the inclusion of a compact subspace in the union of two open ones. The motivation of the paper is principally how to "import" traditional topology into ASD, using the real line as a running example. This paper is the expanded version of the one that I presented at "Category Theory and Computer Science" in Ottawa and the "Domains Workshop" in Birmingham last August/September. =================================== An elementary theory of the category of locally compact locales The second paper shows that, when we add an "underlying set" axiom, the category becomes equivalent to the category of locally compact locales over any elementary topos. The usual structure of locale theory (direct and inverse image maps, Heyting implication, etc) is DERIVED, in a type-theoretic style. This is a new characterisation, not only of this category of spaces, but also of elementary toposes themselves. (The same technique can be applied to the opposite of the category of constructively completely distributive lattices, but I haven't filled in the details of this yet.) ASD axiomatises its category of spaces directly, not starting from a category of sets. However, the full subcategory of overt discrete spaces has emerged to fill this role. In the traditional situation, the forgetful functor from spaces to sets has both adjoints (the discrete and indiscriminate topologies), but of these three functors, only the leftmost exists in standard ASD. This paper postulates its right adjoint, which yields the couniversal overt discrete object related to any given space. (Such a thing would be unacceptable in the main theory, as the equality predicate on the underlying set of the powerset of N would solve the Halting Problem.) Whereas the category of sets is an (often unstated) assumption in a typical mathematical discourse, in this case the topos itself is constructed from the axioms, viz as this full subcategory. More significantly, the infinitary joins that are needed to axiomatise either traditional topology or locale theory are also a consequence of the axioms, and not a part of them. This is the sense in which the new axiomatisation deserves to be called elementary. In fact, the logical power of the theory (powersets in the topos, and the infinitary joins) arises out of the ``underlying set'' assumption. We have another example to show that closure of a full subcategory under (co)limits is a long way from providing an adjoint, and indeed the existence of the adjoint can be very strong foundational principle in itself. For example, when well-foundedness is presented in categorical terms using coalgebras, the extensional ones form a reflective subcategory, but the axiom of replacement may be needed to construct the reflection functor. See Exercise 9.62 in my book, "Practical Foundations of Mathematics". Paul Taylor pt@di.unito.it