Tags:Categorical models, Cubical type theory, Homotopy type theory and Modal type theory

Abstract:

There is recent interest in modal dependent type theories, e.g. guarded type theory, nominal type theory, clocked type theory, cohesive type theory, crisp type theory, and spatial type theory. In this work we describe the model theory of Fitch style modal dependent type theories which allows as to treat modalities which are not necessarily (co)monadic. These include nominal type theories, guarded type theory and clocked type theory. The goal of this work is to isolate and study a common construction of these modal type theories. The construction centers around an adjoint pair of operators, where the left adjoint is an operation on contexts and the right adjoint is an operation on families.