Ayberk Tosun ; Martín Hötzel Escardó - Patch Locale of a Spectral Locale in Univalent Type Theory

entics:10808 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII - https://doi.org/10.46298/entics.10808
Patch Locale of a Spectral Locale in Univalent Type TheoryArticle

Authors: Ayberk Tosun ORCID; 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 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.


    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: January 13, 2023
    Submitted on: January 13, 2023
    Keywords: Computer Science - Logic in Computer Science,Mathematics - General Topology

    Consultation statistics

    This page has been seen 160 times.
    This article's PDF has been downloaded 113 times.