论文标题
立方类型理论的内部参数
Internal Parametricity for Cubical Type Theory
论文作者
论文摘要
我们定义了一种计算类型理论，该理论结合了笛卡尔立方体类型理论的内容相等性结构与内部参数原语。合并的理论既支持一致性及其关系等效性，我们称之为相对论。我们通过分析较高的电感类型之间的多态性函数来证明该理论的使用，观察立方相等性如何正规化参数类型理论，并检查立方体和参数类型理论之间的相似性和差异，这些理论密切相关。我们还将正式界面抽象到计算解释中，并表明这也具有一个预局部模型。
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.
