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.

Intro
Analogy
Unary type theory
Structural Rules
Mode theories
Parametrized spectra
Dependency
Simple type theory
Dependent type theory
Subtle Parts
Mode Theory for Simple Types
Mode Theory for Dependent Types
Modalities
Modal dependent type theories