University of Birmingham > Talks@bham > Lab Lunch > Patch Locale of a Spectral Locale in Univalent Type Theory

Patch Locale of a Spectral Locale in Univalent Type Theory

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

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 ===

Passcode: 217 Meeting ID: 818 7333 5084

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.