Condensed Type Theory

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

• Johan Commelin (Utrecht University)
• Thursday 02 May 2024, 17:00-18:00
• Live-streamed at MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Jonas Bayer.

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 particular 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 describe how these classes interact. The resulting type theory is spiritually related Taylor’s “Abstract Stone Duality”.

As an application I will explain that ODisc is naturally a category, and furthermore, every function ODisc → ODisc is automatically functorial. This axiomatic approach to condensed sets, including the functoriality result, are formalized in Lean 4. If time permits, I will comment on some of the techniques that go into the proof.

Joint work with Reid Barton.

—-

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• Live-streamed at MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.