In this talk, we discuss the process of extending Martin-Löf dependent type theory with one or more modalities: special unary type constructors distinguished by their relatively poor behavior. We introduce a proposed class of modalities—weak dependent right adjoints—which proven flexible enough to accommodate many interesting examples (guarded recursion, internalized parametricity, cohesion, etc.) but still rigid enough to admit a calculus with good syntactic properties. We show then how these weak dependent right adjoints may be assembled into a general framework for modal type theory (MTT). Finally, time permitting, we highlight a recent application of MTT to Riehl and Shulman's theory of synthetic ∞-categories.

This talk contains joint work with Alex Kavvos, Andreas Nuyts, Lars Birkedal, Jonathan Weinberger, and Ulrik Buchholtz.