BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:Patch Locale of a Spectral Locale in Univalent Typ
e Theory - Ayberk Tosun (University of Birmingham)
DTSTART:20220708T130000Z
DTEND:20220708T140000Z
UID:TALK4950AT
URL:/talk/index/4950
DESCRIPTION:A spectral locale is a locale in which the compact
opens form a basis closed under finite meets\, wh
ereas a Stone locale is one that is compact and ze
ro-dimensional (i.e. whose clopens form a basis).
Every Stone locale is spectral as the clopens coin
cide with the compact opens in Stone locales. Ston
e locales together with continuous maps form a cor
eflective subcategory of spectral locales and perf
ect maps. The coreflector is the patch transformat
ion\nthat universally transforms a spectral locale
into a Stone one. A proof in the internal languag
e of an elementary topos was previously given by E
scardÃ³. This proof can be easily translated to uni
valent type theory using resizing axioms. In our w
ork\, we show how to achieve such a translation wi
thout using resizing axioms\, by working with larg
e\, locally small frames with small bases. This qu
estion turns out to be nontrivial and involves pre
dicative reformulations of several fundamental con
cepts of locale theory. \n\n(This is a practice ta
lk for an MFPS presentation. The talk will run for
20 minutes uninterrupted\, including about 5 minu
tes of questions at the end in a conference settin
g. Afterwards there will be time for further quest
ions\, and then feedback for the presentation.)\n\
n=== Zoom details ===\n\nhttps://bham-ac-uk.zoom.u
s/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT
09\n\nPasscode: 217 Meeting ID: 818 7333 5084\n
LOCATION:LG23\, SoCS and Zoom (see abstract for link)
CONTACT:Anupam Das
END:VEVENT
END:VCALENDAR