On some peculiar aspects of the constructive theory of point-free spaces

Abstract

This paper presents several independence results concerning the topos-valid and the intuitionistic (generalised) predicative theory of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined. © 2010 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.