The Patch Topology in Univalent Foundations
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913985986560000 |
|---|---|
| author | Arrieta, Igor Escardó, Martín Hötzel Tosun, Ayberk |
| author_facet | Arrieta, Igor Escardó, Martín Hötzel Tosun, Ayberk |
| contents | 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 and locally small frames with small bases. This requires predicative reformulations of several fundamental concepts of locale theory in predicative HoTT/UF, which we investigate systematically. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_03134 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Patch Topology in Univalent Foundations Arrieta, Igor Escardó, Martín Hötzel Tosun, Ayberk Logic in Computer Science 03F65 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 and locally small frames with small bases. This requires predicative reformulations of several fundamental concepts of locale theory in predicative HoTT/UF, which we investigate systematically. |
| title | The Patch Topology in Univalent Foundations |
| topic | Logic in Computer Science 03F65 |
| url | https://arxiv.org/abs/2402.03134 |