University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Condensed Type Theory

  Browse A-Z

Log in

Googledetails Microsoftdetails

šŸ” Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ā„¹ļø Information

Condensed Type Theory

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/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:

Note that ex-directory lists are not shown.

Other lists

"Iā€™m not European at all. Eurika.ā€ Natalia Goncharova: Her Art and Times. Talk by Dr Natalia Budanova. Madingley Hall In person in the Max Perutz Lecture Theatre (CB2 0QH) and via Zoom link https://mrc-lmb-cam-ac-uk.zoom.us/j/98728840077?pwd=Z0MZ2xWLsyUC6fI31cIklaUbSYALwy.1

Other talks

Title to be confirmed Title TBC External Seminar - Hilde Nelissen TBC Tissue-scale communication in cancer development How Far Can Good Go Without God? The Limits of a Naturalistic Ethic Polar Oceans Seminar Talk
 

Ā© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity