一句话：将多模态类型论的模态机制与立方类型论的计算良好同一类型结合，建立立方模态类型论并给出模型语义。
论文把多模态类型论（MTT）对模态的原则化处理与立方类型论（CTT）计算性质良好的同一类型结合起来，提出立方模态类型论（Cubical MTT）。它兼具两者优点，并为 MTT 此前只能以特设方式支持的模态外延性原则提供验证。作者研究其语义，基于拓扑斯内部语言给出构造 Cubical MTT 模型的公理化方法，并用该方法构造预层模型。最后，在树的拓扑斯的立方版本中构造（立方）守卫递归模型，以证明 Löb 归纳的公理化，从而用 Cubical MTT 顺畅地推理守卫递归。
In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical type theory (CTT). The result -- cubical modal type theory (Cubical MTT) -- has the desirable features of both systems. In fact, the whole is more than the sum of its parts: Cubical MTT validates desirable extensionality principles for modalities that MTT only supported through ad hoc means. We investigate the semantics of Cubical MTT and provide an axiomatic approach to producing models of Cubical MTT based on the internal language of topoi and use it to construct presheaf models. Finally, we demonstrate the practicality and utility of this axiomatic approach to models by constructing a model of (cubical) guarded recursion in a cubical version of the topos of trees. We then use this model to justify an axiomatization of L\"ob induction and thereby use Cubical MTT to smoothly reason about guarded recursion.
@article{paperbot2697,
title = {Unifying cubical and multimodal type theory},
author = {Frederik Lerbjerg Aagaard and Magnus Baunsgaard Kristensen and Daniel Gratzer and Lars Birkedal},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:25)2024}
}