一句话：扩展笛卡尔 cubical 计算类型论，引入索引 cubical 归纳类型模式并证明其可规范性定理。
高阶归纳类型（HITs）为同伦类型论提供了定义和推理高维归纳对象的手段，但同 univalence 公理一样，同伦类型论并未规定 HITs 的计算行为。Cubical 类型论借助 dimension variables 的判断性基础设施，已为 univalence 和特定 HITs 给出计算解释。本文扩展 Angiuli 等人提出的笛卡尔 cubical 计算类型论，加入索引 cubical 归纳类型（CITs）的模式，将 HITs 适配到 cubical 情形。作者分离出 cubical 归纳类型的 canonical values，并相对于这些值证明 canonicity theorem，从而为该类高阶归纳类型提供计算意义。
Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the computational behavior of HITs. Computational interpretations have now been provided for univalence and specific HITs by way of cubical type theories, which use a judgmental infrastructure of dimension variables. We extend the cartesian cubical computational type theory introduced by Angiuli et al. with a schema for indexed cubical inductive types (CITs), an adaptation of higher inductive types to the cubical setting. In doing so, we isolate the canonical values of a cubical inductive type and prove a canonicity theorem with respect to these values.
@article{paperbot658,
title = {Higher inductive types in cubical computational type theory},
author = {Evan Cavallo and Robert Harper},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290314}
}