  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 $\beta/\eta$-normal forms. As corollaries we obtain both
decidability of judgmental equality and the injectivity of type constructors.
