Modal Dependent Type Theory and Dependent Right Adjoints
In recent years we have seen several new models of dependent type
theory extended with some form of modal necessity operator, including
nominal type theory, guarded and clocked type theory, and spatial and
cohesive type theory. In this paper we study modal dependent type
theory: dependent type theory with an operator satisfying (a dependent
version of) the K-axiom of modal logic. We investigate both semantics
and syntax. For the semantics, we introduce categories with families
with a dependent right adjoint (CwDRA) and show that the examples
above can be presented as such. Indeed, we show that any finite limit
category with an adjunction of endofunctors gives rise to a CwDRA via
the local universe construction. For the syntax, we introduce a
dependently typed extension of Fitch-style modal lambda-calculus, show
that it can be interpreted in any CwDRA, and build a term model. We
extend the syntax and semantics with universes.