  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 turns out to be nontrivial and involves predicative reformulations
of several fundamental concepts of locale theory.
