One idiosyncratic framing of type theory is as the study of operations invariant under substitution. Modal type theory, by contrast, concerns the controlled integration of operations—modalities—into type theory which violate this discipline, so-called non-fibered connectives. Modal type theory is therefore built around a fundamental tension: the desire to include modalities and powerful principles for reasoning with them on one hand, and the need to maintain the conveniences and character of Martin-Löf type theory which stem from substitution invariance.
In this thesis, we thoroughly explore and discuss this contradiction. We discuss several different formulations of modal type theory, explore their various syntactic properties, and relate them through their categorical semantics. In particular, we show that most modal type theories that have arisen in the last two decades can be understood through the abstraction of weak dependent right adjoints. We also put forward a new general modal type theory, MTT, based on this abstraction.
The generality of MTT means that, without any additional work, it can be specialized to an arbitrary collection of type theories related by modalities and natural transformations between them. It is therefore easy to obtain a type theory for a comonad, an adjunction, a local topos, or any other number of complex and realistic scenarios. In addition to showing that many modal type theories are closely related to specific instantiations of MTT, we thoroughly explore the syntax and semantics of MTT itself. We prove that MTT enjoys an unconditional normalization result and decidable type-checking under mild assumptions. We show how MTT may be interpreted into a wide variety of structured categories and use this to study the expressive power of the type theory and various extensions thereof.
Finally, we explore several concrete applications of MTT in the context of guarded type theory and guarded denotational semantics. We propose a highly usable language for guarded recursion and explore its particular models and metatheorems. We show a relatively sharp result bounding the extent to which classical guarded recursion can be added to any type theory with decidable type-checking and propose a system to mitigate this issue. Finally, we conduct an in-depth case study using guarded MTT to obtain a fully synthetic account of the Iris program logic, proving adequacy in a fully internal manner.