Discrete and Codiscrete Modalities in Cohesive HoTT
Offered By: Hausdorff Center for Mathematics via YouTube
Course Description
Overview
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.
Syllabus
Tutorial 3 Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT
Taught by
Hausdorff Center for Mathematics
Related Courses
Introduction to programming with dependent types in ScalaStepik Georges Gonthier - Computer Proofs - Teaching Computers Mathematics, and Conversely
International Mathematical Union via YouTube A Fibrational Framework for Modal Dependent Type Theories
Hausdorff Center for Mathematics via YouTube A Fibrational Framework for Modal Simple Type Theories
Hausdorff Center for Mathematics via YouTube Discrete and Codiscrete Modalities in Cohesive HoTT, II
Hausdorff Center for Mathematics via YouTube