Given a locale L and any set-indexed family of continuous mappings , fi:L→Li with compact and completely regular co-domain, a compactification η:L→Lγ of L is constructed enjoying the following extension property: for every a unique continuous mapping exists such that . Considered in ordinary set theory, this compactification also enjoys certain convenient weight limitations.Stone–Čech compactification is obtained as a particular case of this construction in those settings in which the class of [0,1]-valued continuous mappings is a set for all L. (...) This will follow by the proof that–also in the point-free context–a compactification that allows for the extension of [0,1]-valued mappings suffices for deriving the full reflection.A constructive proof that the class is a set whenever L is locally compact and L′ is set-presented and regular is also obtained; together with the described compactification, this makes it possible to characterize the class of locales for which Stone–Čech compactification can be defined constructively. (shrink)

Working in constructive set theory we formulate notions of constructive topological space and set-generated locale so as to get a good constructive general version of the classical Galois adjunction between topological spaces and locales. Our notion of constructive topological space allows for the space to have a class of points that need not be a set. Also our notion of locale allows the locale to have a class of elements that need not be a set. Class sized mathematical structures need (...) to be allowed for in constructive set theory because the powerset axiom and the full separation scheme are necessarily missing from constructive set theory. We also consider the notion of a formal topology, usually treated in Intuitionistic type theory, and show that the category of set-generated locales is equivalent to the category of formal topologies. We exploit ideas of Palmgren and Curi to obtain versions of their results about when the class of formal points of a set-presentable formal topology form a set. (shrink)

Working in constructive set theory we formulate notions of constructive topological space and set-generated locale so as to get a good constructive general version of the classical Galois adjunction between topological spaces and locales. Our notion of constructive topological space allows for the space to have a class of points that need not be a set. Also our notion of locale allows the locale to have a class of elements that need not be a set. Class sized mathematical structures need (...) to be allowed for in constructive set theory because the powerset axiom and the full separation scheme are necessarily missing from constructive set theory. We also consider the notion of a formal topology, usually treated in Intuitionistic type theory, and show that the category of set-generated locales is equivalent to the category of formal topologies. We exploit ideas of Palmgren and Curi to obtain versions of their results about when the class of formal points of a set-presentable formal topology form a set. (shrink)

The class of points in a set-presented formal topology is a set, if all points are maximal. To prove this constructively a strengthening of the dependent choice principle to infinite well-founded trees is used.