一句话：证明了（单值、笛卡尔）立方类型论的归一化，得到无归约的范式双射，并推出判断相等的可判定性与类型构造子单射性。
本文为（单值、笛卡尔）立方类型论证明归一化，解决了该理论句法元理论中最后一个主要未决问题。作者采用无归约（reduction-free）的归一化方法，不是通过逐步归约，而是建立上下文中项的可定义等价类与一类可处理的 β/η-范式语言之间的双射，从而给出范式的组合刻画。该结果直接蕴含判断相等的可判定性，并推出类型构造子的单射性。这为立方类型论作为同伦类型论计算模型的句法基础提供了关键保证，也补全了其元理论拼图。
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of β/η-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.