Normalization for Cubical Type Theory

TL;DR

This paper proves normalization for univalent cubical type theory, establishing key properties like decidability of judgmental equality and injectivity of type constructors, thus resolving a major open problem.

Contribution

It provides a reduction-free normalization proof for univalent cubical type theory, a significant advancement in its syntactic metatheory.

Findings

Normalization is reduction-free and bijective between terms and normal forms.

Decidability of judgmental equality is established.

Injectivity of type constructors is proven.

Abstract

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.