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 - 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. 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. |
## Other listsPhysics of the Impossible Thinking from the East? Geographies of Postsocialism and the Geopolitics of Knowledge Cubo## Other 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 |