{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T04:38:21Z","timestamp":1777955901842,"version":"3.51.4"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T00:00:00Z","timestamp":1754438400000},"content-version":"unspecified","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    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\n                    <jats:italic>resizing axioms<\/jats:italic>\n                    . In this work, we show how to achieve such a translation\n                    <jats:italic>without<\/jats:italic>\n                    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\n                    <jats:sans-serif>HoTT\/UF<\/jats:sans-serif>\n                    , which we investigate systematically.\n                  <\/jats:p>","DOI":"10.1017\/s0960129525000088","type":"journal-article","created":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:12:02Z","timestamp":1754482322000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["The patch topology in univalent foundations"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5319-4916","authenticated-orcid":false,"given":"Igor","family":"Arrieta","sequence":"first","affiliation":[{"name":"University of Birmingham"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4091-6334","authenticated-orcid":false,"given":"Mart\u00edn H.","family":"Escard\u00f3","sequence":"additional","affiliation":[{"name":"University of Birmingham"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0190-3020","authenticated-orcid":false,"given":"Ayberk","family":"Tosun","sequence":"additional","affiliation":[{"name":"University of Birmingham"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2025,8,6]]},"reference":[{"key":"S0960129525000088_ref8","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1286198140"},{"key":"S0960129525000088_ref7","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200910037"},{"key":"S0960129525000088_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80076-8"},{"key":"S0960129525000088_ref10","first-page":"1","volume-title":"29th EACSL Annual Conference on Computer Science Logic (CSL 2021)","volume":"183","author":"de Jong","year":"2021"},{"key":"S0960129525000088_ref19","article-title":"Notions of anonymous existence in Martin-L\u00f6f type theory","volume":"13","author":"Kraus","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129525000088_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"S0960129525000088_ref24","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S0960129525000088_ref25","unstructured":"Tosun, A. (2023) Formalization of locale theory in Agda. Part of the TypeTopology library. HTML rendering of Agda code available at https:\/\/www.cs.bham.ac.uk\/~mhe\/TypeTopology\/Locales.index.html"},{"key":"S0960129525000088_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00695-3"},{"key":"S0960129525000088_ref27","unstructured":"Voevodsky, V. (2011). Resizing rules \u2014 their use and semantic justification. Talk at 18th International Conference on Types for Proofs and Programs (TYPES), Bergen, Norway, September 11, 2011. https:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/2011_Bergen.pdf"},{"key":"S0960129525000088_ref11","first-page":"1","volume-title":"6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)","volume":"195","author":"de Jong","year":"2021"},{"key":"S0960129525000088_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0897-3_12"},{"key":"S0960129525000088_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"S0960129525000088_ref5","doi-asserted-by":"publisher","DOI":"10.1142\/9789811236488_0006"},{"key":"S0960129525000088_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(99)00172-3"},{"key":"S0960129525000088_ref16","doi-asserted-by":"publisher","DOI":"10.4000\/philosophiascientiae.406"},{"key":"S0960129525000088_ref1","unstructured":"Aczel, P. and Rathjen, M. (2010). Notes on Constructive Set Theory. Book draft. https:\/\/www1.maths.leeds.ac.uk\/~rathjen\/book.pdf"},{"key":"S0960129525000088_ref22","unstructured":"Rijke, E. (2022). Introduction to homotopy type theory, Book draft available on arXiv: 2212.11082 [math.LO]."},{"key":"S0960129525000088_ref3","first-page":"1","volume-title":"21st International Conference on Types for Proofs and Programs (TYPES 2015)","volume":"69","author":"Cohen","year":"2018"},{"key":"S0960129525000088_ref18","first-page":"350","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","volume":"1","author":"Johnstone","year":"2002"},{"key":"S0960129525000088_ref17","volume-title":"Cambridge Studies in Advanced Mathematics","author":"Johnstone","year":"1982"},{"key":"S0960129525000088_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-8641(97)00225-3"},{"key":"S0960129525000088_ref26","doi-asserted-by":"publisher","DOI":"10.46298\/entics.10808"},{"key":"S0960129525000088_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511600579"},{"key":"S0960129525000088_ref9","volume-title":"Domain theory in constructive and predicative univalent foundations","author":"de Jong","year":"2023"},{"key":"S0960129525000088_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"S0960129525000088_ref15","unstructured":"Escard\u00f3, M. H. and contributors (2018). TypeTopology. Agda development available at https:\/\/github.com\/martinescardo\/TypeTopology"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129525000088","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T00:09:07Z","timestamp":1777939747000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129525000088\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":27,"alternative-id":["S0960129525000088"],"URL":"https:\/\/doi.org\/10.1017\/s0960129525000088","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e18"}}