一句话：提出融合笛卡尔立方类型理论与内部参数性原语的计算类型理论，同时支持 univalence 与关系等价（relativity）。
本文定义了一种计算类型理论，将笛卡尔立方类型理论中具有内容相等的等式结构与内部参数性原语相结合。该理论同时支持 univalence 及其关系对应物 relativity，从而在统一框架中处理同伦与参数性现象。作者通过分析高阶归纳类型之间的多态函数展示其用途，并观察到立方相等如何规整化（regularize）参数类型理论；同时比较了立方类型理论与参数类型理论之间的相似与差异。最后，论文抽象出计算解释的形式接口，并证明该接口也可在 presheaf 模型中解释。
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.