In 2009, Caramello proved that each topos has a largest dense subtopos whose internal logic satisfies De Morgan law (also known as the law of the weak excluded middle). This finding implies that every locale has a largest dense extremally disconnected sublocale, referred to as its DeMorganization. In this paper, we take the first steps in exploring the DeMorganization in the localic context, shedding light on its geometric nature by showing that it is always a fitted sublocale and by providing a concrete description. Explicit examples of DeMorganizations for toposes that do not satisfy De Morgan law are rather difficult to find. We present a contribution in that direction, with the main result of the paper showing that for any metrizable locale (without isolated points), its DeMorganization coincides with its Booleanization. This, in particular, implies that any extremally disconnected metric locale (without isolated points) must be Boolean, generalizing a well-known result for topological spaces to the localic setting.

Abstract Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. A proof in the internal language of an elementary topos was previously given by the second-named author. This proof can be easily translated to univalent type theory using resizing axioms . In this work, we show how to achieve such a translation without resizing axioms, by working with large, locally small, and small-complete frames with small bases. This requires predicative reformulations of several fundamental concepts of locale theory in predicative HoTT/UF , which we investigate systematically.

This paper presents a version of the lower separation axioms and the principle of enriched continuous extension for quantale-enriched topological spaces. As a remarkable result, among other things, we point out that in the case of commutative Girard quantales the principle of continuous extension holds for projective modules in Sup.