Topological inductive definitions

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 FSp(i) of inductively generated formal spaces. Considered in impredicative systems as the intuitionistic set theory IZF, FSp and FSp(i) 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 FSp(i) is complete (in particular has all products), but does not contain some naturally occurring classes of formal spaces. Moreover, completeness of FSp(i) 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 FSp(i) as full subcategories, and, as FSp and FSp(i), 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. (C) 2011 Elsevier B.V. All rights reserved.