立方类型论的内部参数性
Internal Parametricity for Cubical Type Theory
AI总结：
本文提出一种结合立方类型论与内部参数性原语的计算类型论，支持非直性和相对性，通过分析高阶归纳类型间的多态函数展示其应用，并给出预层模型。
摘要：
我们定义了一种计算类型论，将笛卡尔立方类型论的内容性相等结构与内部参数性原语相结合。该组合理论同时支持非直性（univalence）及其关系等价物，我们称之为相对性（relativity）。我们通过分析高阶归纳类型之间的多态函数来展示该理论的应用，观察立方相等如何正则化参数性类型论，并考察立方类型论与参数性类型论之间的相似性和差异，这两者密切相关。我们还抽象出计算解释的正式接口，并表明该接口也具有预层模型。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
