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 an injective function from equivalence classes of terms in context to a tractable language of $\beta/\eta$-normal forms. As corollaries we obtain both decidability of judgmental equality as well as the injectivity of type constructors in judgmentally consistent contexts.

翻译：我们证明(单价、笛卡尔)立方类型理论是正常化的,它解决了立方类型理论合成元论中最后一个主要的开放问题。 我们的正常化结果是无排减的,从上下文的等值术语到可伸缩的语言$\beta/\eta$-tal-formal 形式。 作为累加者,我们既获得了判决平等可变性,也获得了类型构建者在判断一致环境中的注射。