COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Condensed Type Theory
Condensed Type TheoryAdd 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. 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 listsPhysics of the Impossible Thinking from the East? Geographies of Postsocialism and the Geopolitics of Knowledge CuboOther talksLMB Seminar: Title TBC Author-Meets-Readers: Theory and Explanation in Geography Using the Proteome Discoverer to Interogate your Data Alphafold2 at the LMB - Use and Applications Thicker Than Blood: Kinship, Its Multiplicity, and Entanglements - a Cambridge Reproduction Forum Mechanics of Soft Composites: The Interplay between Geometrical Structuring and Large Deformation to Achieve Novel Behavior |