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.

翻译：本文结合了多模态类型论（MTT）中对模态的原理性处理方法与立方类型论（CTT）中计算行为良好的恒等类型实现。其结果——立方模态类型论（Cubical MTT）——兼具两个系统的理想特性。事实上，整体效果超越了部分之和：Cubical MTT 验证了模态的可取外延性原理，而 MTT 仅能通过特设方式支持这些原理。我们研究了 Cubical MTT 的语义学，并基于拓扑斯内部语言提出了一种构建 Cubical MTT 模型的公理化方法，利用该方法构造了预层模型。最后，我们通过在树的拓扑斯的立方版本中构建（立方）守卫递归模型，证明了这种模型公理化方法的实用性与有效性。随后，我们利用该模型为 Löb 归纳法提供了公理化的合理性证明，从而借助 Cubical MTT 实现了对守卫递归的流畅推理。