Normalization for Cubical Type Theory

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.