Modal Dependent Type Theory and Dependent Right Adjoints

TL;DR

This paper develops a new framework for modal dependent type theory by introducing categories with families with a dependent right adjoint, and provides both semantic and syntactic models including extensions with universes.

Contribution

It introduces categories with families with a dependent right adjoint (CwDRA) and a dependently typed Fitch-style modal lambda-calculus, unifying semantics and syntax for modal dependent type theory.

Findings

Finite limit categories with adjunctions give rise to CwDRA

The dependently typed Fitch-style calculus can be interpreted in CwDRA

Extended models include universes for richer type theories

Abstract

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.