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