Tags:linear type theory, modal type theory, MTT, multimodal type theory, multimode type theory and ordered type theory
Abstract:
Multimode type theory (MTT) is parametrized by a mode theory: a 2-category whose objects, morphisms and 2-cells serve as internal modes, modalities and 2-cells. So far, this mode theory has remained in the metatheory, with syntactic modal type and term formers being indexed by metatheoretic gadgets. Building a syntactic lock calculus on top of the mode theory has several advantages: the modal aspects of substitution take the form of more familiar syntactical substitutions, the lock operation on contexts can be axiomatized as pseudofunctorial so that models of MTT no longer need to be strict(ified), and we can have internal mode, modality and 2-cell polymorphism with intensional 2-cell equality.