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.

翻译：我们证明，与表面现象相反，基于2-范畴M的多模态类型理论（MTT）可解释于任意M形状的范畴图，该图由具有并保持M大小极限的范畴与函子构成，且无需额外左伴随。这一结果通过名为“余右化”（co-dextrification）的构造实现，该构造可向任意此类图共自由添加左伴随，进而用于解释MTT的“上下文锁”函子。此外，若图中任一函子具有右伴随，这些右伴随也可在类型理论中内化，以FitchTT风格的负模态形式呈现。我们将由此产生的组合通用模态类型理论命名为多模态伴随类型理论（MATT）。特别地，我们可在任意有限拓扑斯与几何态射图景中解释MATT，其中逆像函子对应正模态，直像函子对应负模态。