Compactness under constructive scrutiny

The aim of this thesis is to understand the constructive scope of compactness. We show that it is possible to define, constructively, a meaningful notion of compactness in a more general setting than the uniform/metric space one. Fur-thermore, we show that it is not possible to define compactness constructively in a topological space. We investigate exactly what principles are necessary and sufficient to prove classically true theorems about compactness, as well as their antitheses. We develop beginnings of a constructive theory of differentiable manifolds. i Acknowledgments People to thank fall into the four categories: family, friends, teachers and colleagues—most fall into more than one. This thesis is dedicated to all of them; I am sure that without their contributions this thesis would be emptier. Naturally, D.S. Bridges deserves the biggest share of thanks for his (uniformly