Re: Uniform locales in Shv(X)

Jeff Egger <jeffegger@yahoo.ca> wrote in part:

I have an idea of how this might be done, but it requires a detour through gauge spaces [...] which I'm not sure is constructively valid.

Presumably it's not valid if we don't at least have the classical theorem that every pointwise uniformity comes from a family of psuedometrics. The proof that I know of this relies on dependent choice, as well as forming infima of inhabited sets of nonnegative real numbers. These infima are constructively valid if we allow our pseudometrics to take values in the upper real numbers instead of only the real numbers. I don't know what to do about the dependent choice, however. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]