Patch Locale of a Spectral Locale in Univalent Type Theory

Add to your list(s) Download to your calendar using vCal

• Ayberk Tosun (University of Birmingham)
• Friday 08 July 2022, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Anupam Das.

A spectral locale is a locale in which the compact opens form a basis closed under finite meets, whereas a Stone locale is one that is compact and zero-dimensional (i.e. whose clopens form a basis). Every Stone locale is spectral as the clopens coincide with the compact opens in Stone locales. Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. The coreflector is the patch transformation that universally transforms a spectral locale into a Stone one. A proof in the internal language of an elementary topos was previously given by Escardó. This proof can be easily translated to univalent type theory using resizing axioms. In our work, we show how to achieve such a translation without using resizing axioms, by working with large, locally small frames with small bases. This question turns out to be nontrivial and involves predicative reformulations of several fundamental concepts of locale theory.

(This is a practice talk for an MFPS presentation. The talk will run for 20 minutes uninterrupted, including about 5 minutes of questions at the end in a conference setting. Afterwards there will be time for further questions, and then feedback for the presentation.)

=== Zoom details ===

https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09

Passcode: 217 Meeting ID: 818 7333 5084

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• LG23, SoCS and Zoom (see abstract for link)
• Lab Lunch

Note that ex-directory lists are not shown.