I am not an expert on elementary topos (meaning by this to work with the internal language in a Grothendiek topos) and I rather be told than struggle with the following: Consider an elementary topos EE, a locale G in EE, the unique locale morphism i^*: Omega --> G, and any arrow b: X x Y --> G: Consider the following formulae on "b": ed): Supremun_y b(x, y) = 1 uv): b(x, y) inf b(x, y') <_= i^*[[y = y']]. Let u: X x Y --> Map(X, Y) be the universal locale furnished with such an arrow (that is, forall b exists! t^* : Map(X, Y) --> G t^* u = b. Gavin Wraith (in "Localic Groups", Cahiers de Top. et Geom. Diff. Vol XXII-1 1981) defines an object Points(G) = LocalMorphisms(G, Omega) C Omega^G and says that it is clear that: a) Points(Map(X, Y)) = Y^X. From this taking global sections it follows that: b) There is a bijection between arrows X x Y --> Omega and arrows X --> Y (where the arrow on the right satisfy ed) and uv)) QUESTION 1] I ask for a convincing proof of a), or better, of the weaker ? b). Concerning b), consider the following conditions on a relation R C X x Y: exed) pi_1: R --> X is an epimorphism. exuv) The family y = pi_2 (x, y): Z --> R --> Y is a compatible family with respect to the family x = \pi_1 (x, y): Z --> R --> X (indexed by all (x, y): Z --> R) Then, using that epis are strict it follows using standard category theory: R satisfy exed) and exuv) iff exists! f: X --> Y such that R = Gamma_f (the Graph of f) Thus, b) will follow if we can prove : R satisfy exed) and exuv) iff cf_R satisfy ed) and uv) (cf_R = characteristic function). This is more related with the formula uv'): b(x, y) inf b(x', y') inf i^*[[x = x']] <_= i^*[[y = y']]. Also, by standard category theory it follows that "exed) + exuv)" are equivalent to "pi_1 is mono and epi". This may help ? NOTE: All the above is very clear in the topos of Sets, but my problem is that I am very uncomfortable when the experts write "we do as if the base topos is the topos of Sets". Does this slogan apply to the above ?. SUBQUESTION] Are uv) and uv') equivalent ? Now a more substantial question: QUESTION 2] Consider now a geometric morphism g: FF --> EE. We have a bijection between arrows X x Y --> g_* Omega_FF and arrows g^*X x g^*Y --> Omega__EE. I want to know if the arrows satisfying ed) and uv) correspond under this bijection. e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]