Dear Jeff, I think the problem is that (as far as I know) no one has developed a nice constructive theory of uniform locale. If I'm mistaken about that I would be really happy to know more about it. I have done in my thesis (in chapitre 3 section 3, https://www.imj-prg.fr/~simon.henry/Thesis.pdf) the case of constructive metric locale, under the assumption that the map $Y \rightarrow X$ is open. Removing this openness hypothesis seems difficult but I stil have hope that this is possible, and I have a few idea about it... For the general case it seems to me that the only definition that have a chance to work properly without the openess condition is the definition by entourage and this one should be easy to externalise: any local section of the sheaf of entourage will corresponds to an open sublocale of Y \times_X Y, (containing the restriction of the diagonal to the open sublocale of $X$ on which it is defined ), and it should not be to hard to give the axioms that these have to satisfy... is this the kind of things your are looking for ? Best wishes, Simon Henry
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.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]