Discrete and Codiscrete Modalities in Cohesive HoTT, II

Explore discrete and codiscrete modalities in Cohesive Homotopy Type Theory (HoTT) in this advanced tutorial, the second part of a series. Delve into recent developments in modal extensions of homotopy type theory, focusing on their applications in synthetic formalizations of topology, differential geometry, and spectra. Examine the internal language presentations of cubical models of HoTT and gain insights into the frameworks used to design these type theories. Learn about the shape modality in real-cohesive HoTT, covering spaces, and the fibrational framework for modal dependent type theories. Discover the implications of this work for differential cohesive HoTT and its potential impact on mathematical foundations.