Favonia: Normalization in Cubical Type Theory

Abstract: Cubical type theory is the first known strategy to give constructive meanings to new features introduced by homotopy type theory, including univalence and higher inductive types. However, the new judgmental structure complicates the usual story of normalization, which makes efficient implementations challenging.

The fundamental problem is that we have to consider partial elements under a theory of equations of dimensions, and a normal form may cease to be normal under a different theory. In this talk, I will explain our current attempts towards an updated account for cubical type theory.