Dear Hasse, The presheaves that Townsend and I used are on the category Loc of locales. The fact that Loc is large may be seen as a problem, but another illegitimacy is the way a presheaf is a functor to Sets. This means, for instance, that for a representable presheaf y(X), where X is a locale, we take y(X)(W) = Loc(W,X) to be a _set_ for any pair of locales X and W, and that is foundationally tendentious. Whatever kind of collection Loc(W,X) is (if W is locally compact then we can take it to be another locale, but otherwise not), the ability to extract a "set of points" from it is sensitive to the foundations. We tried to be foundationally conservative in what we did with the presheaves, and you can see come remarks on this in the conclusions of our paper. (I should stress that we did not claim to have embedded Loc in a CCC, and we tried not to make use of any particular categorical properties of Presh(Loc).) Insofar as the representable presheaves y(X) can be acceptable, then so too are their exponentials y(Y)^y(X), since y(Y)^y(X)(W) = Loc(WxX,Y). What we showed is that then the exponential y($)^(y($)^y(X)) also exists (where $ = the Sierpinski locale), and in fact is representable of the form y(PP(X)) where PP(X) is the "double powerlocale" on X. Thus PP(X) has a claim to be thought of as $^($^X) even when X is not exponentiable (locally compact). PP is a foundationally robust construction, available in both topos-valid locale theory and predicative formal topology. Regards, Steve Vickers. Hasse Riemann wrote:
Another is how to embed the category of locales in a CCC WITHOUT using illegitimate presheaves (Vickers and Townsend) or the axiom of collection (Heckmann).
I don't follow to the end here. Why should presheaves be illegitimate?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]