Condensed Type Theory - Axioms and Applications

Explore the concept of condensed type theory in this 37-minute lecture by Johan Commelin from the Hausdorff Center for Mathematics. Delve into the topos of condensed sets and discover the axioms that define this particular type theory. Learn about two important predicates on types: "compact Hausdorff" (CHaus) and "overt and discrete" (ODisc). Examine how these classes interact and their significance in the theory. Understand the spiritual connection to Taylor's "Abstract Stone Duality" and explore practical applications, including the natural category structure of ODisc and the automatic functoriality of functions from ODisc to ODisc. Gain insights into the formalization of this axiomatic approach to condensed sets in Lean 4, and if time allows, learn about the techniques used in the proof. This lecture presents joint work with Reid Barton, offering a deep dive into advanced concepts in type theory and category theory.