Abstract

In intuitionistic generalized predicative systems as constructive set theory, or constructive type theory, two categories have been proposed to play the role of the category of locales: the category FSp of formal spaces, and its full subcategory FSpi of inductively generated formal spaces. Considered in impredicative systems as the intuitionistic set theory IZF, FSp and FSpi are both equivalent to the category of locales. However, in the mentioned predicative systems, FSp fails to be closed under basic constructions such as that of finite products, while FSpi is complete , but does not contain some naturally occurring classes of formal spaces. Moreover, completeness of FSpi only holds under the assumption of strong principles for the existence of inductively defined sets.In this paper, working in the context of constructive set theory, the category ImLoc of imaginary locales is introduced. ImLoc is complete already over weak formulations of constructive set theory, contains FSp and FSpi as full subcategories, and, as FSp and FSpi, is equivalent to the category of locales in IZF.Applications of the concept of imaginary locale to a proof of a point-free version of Tychonoff embedding theorem, and to set-representation theorems, are then presented