A universal characterization of the double powerlocale

CF Townsend, Steven Vickers

Research output: Contribution to journalArticle

29 Citations (Scopus)
172 Downloads (Pure)


This is a version from 29 Sept 2003 of the paper published under the same name in Theoretical Computer Science 316 (2004) 297{321. The double powerlocale P(X) (found by composing, in either order,the upper and lower powerlocale constructions PU and PL) is shown to be isomorphic in [Locop; Set] to the double exponential SSX where S is the Sierpinski locale. Further PU(X) and PL(X) are shown to be the subobjects P(X) comprising, respectively, the meet semilattice and join semilattice homomorphisms. A key lemma shows that, for any locales X and Y , natural transformations from SX (the presheaf Loc(
Original languageEnglish
Pages (from-to)297-321
Number of pages25
JournalTheoretical Computer Science
Publication statusPublished - 1 Jan 2004


  • Scott continuity
  • locale
  • topos
  • powerdomain


Dive into the research topics of 'A universal characterization of the double powerlocale'. Together they form a unique fingerprint.

Cite this