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)

In this note a T1 formal space is a formal space whose points are closed as subspaces. Any regular formal space is T1. We introduce the more general notion of a formal space, and prove that the class of points of a weakly set-presentable formal space is a set in the constructive set theory CZF. The same also holds in constructive type theory. We then formulate separation properties for constructive topological spaces , strengthening separation properties discussed elsewhere. Finally we relate (...) the properties for ct-spaces with corresponding properties of formal spaces. (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)

Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected.Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact (...) set is Bishop compact iff it is located. We translate this result to formal topology. ‘Bishop compact’ is translated as compact and overt. We propose a definition of locatedness on subspaces of a formal topology, and prove that a closed subspace of a compact regular formal space is located iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact — that is, totally bounded and complete — iff its localic completion is compact overt.Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales.We work constructively, predicatively and avoid the use of the axiom of countable choice. (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.