Discrete and Codiscrete Modalities in Cohesive HoTT

Explore discrete and codiscrete modalities in Cohesive Homotopy Type Theory (HoTT) through this in-depth tutorial lecture. Delve into recent developments in modal extensions of homotopy type theory, examining their applications in synthetic formalizations of topology, differential geometry, and spectra. Gain insights into internal language presentations of cubical models of HoTT. Learn about the fibrational framework for modal simple and dependent type theories, the shape modality in real-cohesive HoTT, and covering spaces. Discover the intricacies of discrete and codiscrete modalities in cohesive HoTT, and explore differential cohesive HoTT. Benefit from the collaborative research efforts of experts in the field, including Jacob Gross, Max S. New, Ian Orton, Jennifer Paykin, Andrew M. Pitts, Egbert Rijke, Mitchell Riley, Urs Schreiber, Michael Shulman, and Bas Spitters.

Tutorial 3 Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT