PhD Thesis, Department of Computing, Imperial College, 1996. 158 pages.
Our work is entirely constructive; none of the mathematics developed uses the excluded middle or any choice axioms. No use is made of a natural numbers object.
We get a glimpse of the parallel between the preframe approach and the SUP-lattice approach to locale theory by developing the preframe coverage theorem and the SUP-lattice coverage theorem side by side and as examples of a generalized coverage theorem.
Proper locale maps and open locale maps are defined and seen to be parallel. We argue that the compact regular locales are parallel to the discrete locales. It is an examination of this parallel that is the driving force behind the thesis.
We proceed with examples: relational composition in Set can be expressed as a statement about discrete locales; we then appeal to our parallel and examine relational composition of closed relations of compact regular locales. A technical achievement of the thesis is the discovery of a preframe formula for this relational composition.
We use this formula to investigate ordered compact regular locales (where the order is required to be closed). We find that Banaschewski and Bruemmer's compact regular biframes (Stably continuous frames [Math. Proc. Camb. Phil. Soc. (1988) 104 7-19]) are equivalent to the compact regular posets with closed partial order. We also find that the ordered Stone locales are equivalent to the coherent locales. This is a localic, and so constructive, version of Priestley's duality.
Further, using this relational composition, we can define the Hausdorff systems as the proper parallel to Vickers' continuous information systems (Information systems for continuous posets [Theoretical Computer Science 114 (1993) 201-229]) The category of continuous information systems is shown by Vickers to be equivalent to the (constructively) completely distributive lattices; we prove the proper parallel to this result which is that the Hausdorff systems are equivalent to the stably locally compact locales. This last result can be viewed as an extension of Priestley's duality.
Journal of Pure and Applied Algebra 116 (1997) 323-335.
Given the category OStoneSp of ordered Stone spaces (as introduced by Priestley, 1970) and the category CohSp of coherent spaces (= spectral spaces) one can construct a pair of functors between them which Priestley (1970) has shown, using the prime ideal theorem, define an equivalence.
In this paper we define ordered Stone locales. These are classically just the ordered Stone spaces. It is well known that the localic analogue of the coherent spaces is the category of coherent locales. We prove, entirely constructively, that the category of coherent locales is equivalent to the category of ordered Stone locales.