Paul Taylor: The importance of subspace topology
Abstract: The "finite open subcover" (compactness) property of the closed real interval plays a key role in classical analysis, but it can be difficult to achieve this in constructive theories, especially if these are based on points. Two examples of this failure are "the set of computably representable reals" and the equaliser of function-spaces that one gets by interpreting the Dedekind reals in the category Dcpo.
The idea of "topology as lambda calculus" originates from Dana Scott's work on continuous lattices in 1972. The topology on a space X is the exponential type X→Sigma, where Sigma is the Sierpinski space, which classically has one open and one closed point. Then compactness of a space K can be understood as a term all_K:(K→Sigma)->Sigma, which is easily transformed into must_K(X→Sigma)->Sigma given any term (continuous function) K->X, in particular when K is a subspace of X. One can characterise all_K as a right adjoint, whilst must_K preserves top and meet. However, without additional hypothesis, there is no way to recover K from must_K, or to define must_II for the closed interval as a subspace of R.
