Patch Locale of a Spectral Locale in Univalent Type Theory

Ayberk Tosun, Martín Hötzel Escardó

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 previo…