Condensed Type Theory
Add to your list(s)
Download to your calendar using vCal
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/engb/microsoftteams/joinameeting?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:
Note that exdirectory lists are not shown.
