BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Condensed Type Theory - Dr Johan Commelin (Utrecht University)
DTSTART:20240502T160000Z
DTEND:20240502T170000Z
UID:TALK212212@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:Condensed sets form a topos\, and hence admit an internal type
  theory. In this talk I will describe a list of axioms satisfied by this p
 articular type theory. In particular\, we will see two predicates on types
 \, that single out a class CHaus of "compact Hausdorff" types and a class 
 ODisc of "overt and discrete" types\, respectively. A handful of axioms de
 scribe how these classes interact. The resulting type theory is spirituall
 y related Taylor's "Abstract Stone Duality".\n\nAs an application I will e
 xplain that ODisc is naturally a category\, and furthermore\, every functi
 on ODisc → ODisc is automatically functorial. This axiomatic approach to
  condensed sets\, including the functoriality result\, are formalized in L
 ean 4. If time permits\, I will comment on some of the techniques that go 
 into the proof.\n\nJoint work with Reid Barton.\n\n—-\n\nWATCH ONLINE HE
 RE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 
 Meeting ID: 370 771 279 261 Passcode: iCo7a5
LOCATION:Live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR