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，其中逆像函子对应正模态，正直像函子对应负模态。