多模态伴随类型理论的语义
Semantics of multimodal adjoint type theory
AI总结：
本文证明了无需额外左伴随即可在特定范畴图中解释多模态类型理论（MTT），通过“co-dextrification”构造添加左伴随以解释上下文锁函子，并引入多模态伴随类型理论（MATT）将右伴随内化为负模态，从而支持在拓扑斯和几何态射的有限图中进行解释。
摘要：
我们证明，与表面相反，2-范畴 M 上的多模态类型理论（MTT）可以在任何具有 M 大小极限且函子保持 M 大小极限的 M 形状范畴图中进行解释，无需额外的左伴随。这是通过一种称为“co-dextrification”的构造实现的，该构造自由地向任何此类图添加左伴随，随后可用于解释 MTT 的“上下文锁”函子。此外，如果图中的任何函子具有右伴随，这些右伴随也可以在类型理论中作为 FitchTT 风格的负模态被内化。我们为由此产生的组合一般模态类型理论引入了多模态伴随类型理论（MATT）这一名称。特别地，我们可以在任何拓扑斯和几何态射的有限图中解释 MATT，其中逆像函子对应正模态，正像函子对应负模态。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
