Compactness and Local Compactness

Abstract

The cover definition of compactness is basically point-free; therefore there is no surprise that the basic facts are very much like in the classical case. But a surprise does come: the point-free variant of Stone-?Cech compactification is fully constructive (no choice principle and no use of the excluded middle). Thus in particular, the fact that products of compact (regular) locales are compact is constructive, unlike the Tychonoff Theorem of classical topology (see Section 4 – in particular 4.5 and 6.5).