LFCS Seminar: Tuesday, 27th May: Ayberk Tosun Title: Constructive and Predicative Locale Theory in Univalent Foundations Abstract: Univalent foundations (also known as homotopy type theory or HoTT/UF) is a variant of Martin-Löf Type Theory that introduces several novelties, which turn out to be particularly well-suited for thedevelopment of constructive and predicative mathematics. In this talk, I will present my doctoral work with Martín Escardó on the constructive and predicative development of point-free topology within the foundtional setting of HoTT/UF, with a particular focus on the theory of spectral and Stone locales. Specifically, I will explain how the theory of spectral and Stone locales can be developed in a fully constructive and predicative manner in HoTT/UF, and I will present two applications of this framework: (1) a predicative version of the Stone duality for spectral locales, and (2) a predicative construction of the patch locale of a spectral locale, which universally transforms it into a Stone locale. I will then discuss how this framework can be used to investigate the constructive topology of domains, and will present a new, topological characterization of Tom de Jong’s notion of sharp element, formulated in terms of the patch locale of the Scott locale of a Scott domain. Time permitting, I will also discuss some ongoing work on the constructive treatment of the Lawson topology of a Scott domain. All the results to be presented in this talk have been fully formalized in the Agda proof assistant, as part of Escardó’s TypeTopology library. May 27 2025 16.10 - 17.10 LFCS Seminar: Tuesday, 27th May: Ayberk Tosun Ayberk Tosun, University of Birmingham https://ayberkt.xyz/ Venue: IF G.03
LFCS Seminar: Tuesday, 27th May: Ayberk Tosun Title: Constructive and Predicative Locale Theory in Univalent Foundations Abstract: Univalent foundations (also known as homotopy type theory or HoTT/UF) is a variant of Martin-Löf Type Theory that introduces several novelties, which turn out to be particularly well-suited for thedevelopment of constructive and predicative mathematics. In this talk, I will present my doctoral work with Martín Escardó on the constructive and predicative development of point-free topology within the foundtional setting of HoTT/UF, with a particular focus on the theory of spectral and Stone locales. Specifically, I will explain how the theory of spectral and Stone locales can be developed in a fully constructive and predicative manner in HoTT/UF, and I will present two applications of this framework: (1) a predicative version of the Stone duality for spectral locales, and (2) a predicative construction of the patch locale of a spectral locale, which universally transforms it into a Stone locale. I will then discuss how this framework can be used to investigate the constructive topology of domains, and will present a new, topological characterization of Tom de Jong’s notion of sharp element, formulated in terms of the patch locale of the Scott locale of a Scott domain. Time permitting, I will also discuss some ongoing work on the constructive treatment of the Lawson topology of a Scott domain. All the results to be presented in this talk have been fully formalized in the Agda proof assistant, as part of Escardó’s TypeTopology library. May 27 2025 16.10 - 17.10 LFCS Seminar: Tuesday, 27th May: Ayberk Tosun Ayberk Tosun, University of Birmingham https://ayberkt.xyz/ Venue: IF G.03
May 27 2025 16.10 - 17.10 LFCS Seminar: Tuesday, 27th May: Ayberk Tosun Ayberk Tosun, University of Birmingham https://ayberkt.xyz/
