Semantics of multimodal adjoint type theory
Michael Shulman
TL;DR
This work addresses the semantic gap in modal dependent type theories by showing that a general interpretation over a $2$-category of modes can be achieved without preexisting left adjoints. It introduces $co$-$dextrification$, a cofree construction that adjoins left adjoints to an arbitrary $M$-shaped diagram, enabling interpretation of MTT and FitchTT and motivating the unified theory $MATT$. The framework supports interpretation in finite diagrams of toposes, with positive modalities for inverse image and negative modalities for direct image functors, and accommodates right adjoints as negative modalities when present. These results broaden the semantic reach of modal dependent type theories and raise natural questions about normalization, decidability, and homotopical interpretations within adjoint modal pre-models.
Abstract
We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-sized limits, without the need for extra left adjoints. This is achieved by a construction called "co-dextrification" that co-freely adds left adjoints to any such diagram, which can then be used to interpret the "context lock" functors of MTT. Furthermore, if any of the functors in the diagram have right adjoints, these can also be internalized in type theory as negative modalities in the style of FitchTT. We introduce the name Multimodal Adjoint Type Theory (MATT) for the resulting combined general modal type theory. In particular, we can interpret MATT in any finite diagram of toposes and geometric morphisms, with positive modalities for inverse image functors and negative modalities for direct image functors.