Dear all,
I found myself wondering yesterday "what does a uniform locale internal to
Shv(X) look like?". In theory, this ought to be quite a simple thing: a locale map Y-->X equipped with a "fibrewise uniform structure". Has anyone
already worked out a precise definition for the latter phrase? Pointers to
relevant literature would be greatly appreciated!
Cheers, Jeff.
Peter Johnstone started to investigate a theory of uniform locales based on topos logic in: "A constructive theory of uniform locales. I. Uniform covers". General topology and applications (Staten Island, NY, 1989), 179-193, Lecture Notes in Pure and Appl. Math., 134, Dekker, New York, 1991. As far as I remember, the role of overtness is also discussed in the paper. An approach to metric and uniform locales that is suited to constructive predicative systems can be found in G. Curi, "On the collection of points of a formal space". Annals of Pure and Applied Logic 137, 1-3, 2006, pp. 126-146, and G. Curi, "Constructive metrisability in point-free topology". Theoretical Computer Science 305 (2003), no. 1-3, 85-109. With kind regards, Giovanni Curi [For admin and other information see: http://www.mta.ca/~cat-dist/ ]