If *X* is a locale, then its double powerlocale P*X* is defined
to be PU(PL(*X*)) where PU and PL are the upper and lower powerlocale
constructions. We prove various results relating it to exponentiation of
locales, including the following. First, if *X* is a locale for which
the exponential *S*^*X* exists (where *S* is the Sierpinski
locale), then P*X* is an exponential *S*^(*S*^*X*).
Second, if in addition *W* is a locale for which P*W* is
homeomorphic to *S*^*X*, then *X* is an exponential
*S*^*W*.

The work uses geometric reasoning, i.e. reasoning stable under pullback along geometric morphisms, and this enables the locales to be discussed in terms of their points as though they were spaces. It relies on a number of geometricity results including those for locale presentations and for powerlocales.

Keywords: locale, powerlocale, exponentiable, geometric logic

2000 MSC: 06D22, 03G30, 03F55, 54C35, 18C15

*Theory and Applications of Categories,*
Vol. 12, 2004,
No. 13, pp 372-422.

http://www.tac.mta.ca/tac/volumes/12/13/12-13.dvi

http://www.tac.mta.ca/tac/volumes/12/13/12-13.ps

http://www.tac.mta.ca/tac/volumes/12/13/12-13.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/12/13/12-13.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/12/13/12-13.ps