论文标题
统一立方体和多模式理论
Unifying cubical and multimodal type theory
论文作者
论文摘要
在本文中，我们结合了多模式类型理论（MTT）的原则性方法，以及从立方体类型理论（CTT）中对身份类型的计算表现良好的实现。结果 - 立方模态类型理论（立方MTT）具有两个系统的理想特征。实际上，整体不仅仅是其各个部分的总和：立方MTT验证了MTT仅通过临时手段支持的模式的理想扩展原理。我们研究了立方MTT的语义，并为基于Topoi的内部语言生成立方MTT的模型提供了一种公理方法，并使用它来构建前模型。最后，我们通过在树木拓扑的立方版本中构建（立方）保护的递归模型，证明了这种公理方法对模型的实用性和实用性。然后，我们使用此模型来证明Löb诱导的公理化合理性，从而使用立方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öb induction and thereby use Cubical MTT to smoothly reason about guarded recursion.
