The patch topology in univalent foundations

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.