A Fibrational Framework for Modal Dependent Type Theories
Explore a comprehensive lecture on modal dependent type theories within the Hausdorff Trimester Program: Types, Sets and Constructions. Delve into recent developments in homotopy type theory extensions, their design frameworks, and applications in real-cohesive and differential-cohesive HoTT. Learn about the fibrational framework for modal simple and dependent type theories, shape modality in real-cohesive HoTT, covering spaces, and discrete and codiscrete modalities in cohesive HoTT. Examine the intricate relationships between unary type theory, structural rules, mode theories, parameterized spectra, and dependency. Gain insights into the subtle aspects of mode theory for simple and dependent types, as well as the complexities of modalities and modal dependent type theories. This lecture, part of a series, presents collaborative work by renowned researchers in the field of type theory and its applications to topology, differential geometry, and spectra.