This chapter reports the main result of the dissertation, normalization for cubical type theory and its corollaries: injectivity of type constructors, and decidability of equality & typing. These results were first obtained by Sterling and Angiuli for the fragment of cubical type theory without universes; the present chapter extends the results of op. cit. to support a cumulative hierarchy of universes.
The central innovation of this chapter is to generalize the notion of neutral form to accommodate the computational behavior of terms that have free variables of type \mathbb {I} discussed in our synopsis of Chapter 6. In the conventional account of neutral and normal forms, neutrals {\color {DarkRed}{e}} are built up inductively from
x for term variables x : A, function applications to normal forms {{\color {DarkRed}{e}}}\mathrel {{\color {DarkRed}{\bullet }}}{{\color {DarkBlue}{m}}}
and projections from neutral pairs {{\color {DarkRed}{e}}}{\color {DarkRed}{.1}}, {{\color {DarkRed}{e}}}{\color {DarkRed}{.2}}; our account of neutrals is much the same, except that each neutral form {\color {DarkRed}{e}} comes equipped with a “frontier
of instability” \boldsymbol {\partial }{{\color {DarkRed}{e}}}, a predicate on its free \mathbb {I}-variables that indicates when it “needs to compute further”. We think of a neutral form for an n-cube as being undefined on its frontier of instability; the process of restricting a neutral to its frontier of instability is then referred to as destabilization.
When x : A is a variable of an ordinary type, the frontier of instability \boldsymbol {\partial }\,{\mathopen {}\left ({\color {DarkRed}{\mathsf {var}}}\,{x}\right )\mathclose {}} is empty because variables never need to compute further. Where something new happens is the path type: given a neutral form {\color {DarkRed}{e}} : \mathsf {ne}\,{\mathopen {}\left ({u}\mathrel {{\sim }_{A}}{v}\right )\mathclose {}}
of path type, we have for each term r : \mathbb {I} a neutral form {{\color {DarkRed}{e}}}\mathrel {{\color {DarkRed}{@}}}{r} : \mathsf {ne}\,A whose frontier of instability is defined like so:
\boldsymbol {\partial }\,{\mathopen {}\left ({{\color {DarkRed}{e}}}\mathrel {{\color {DarkRed}{@}}}{r}\right )\mathclose {}}
=
\boldsymbol {\partial }{\color {DarkRed}{e}}
\lor
{\mathopen {}\left (r=0\right )\mathclose {}}
\lor
{\mathopen {}\left (r=1\right )\mathclose {}}
In other words, the path neutral application {{\color {DarkRed}{e}}}\mathrel {{\color {DarkRed}{@}}}{r} needs to compute as soon as e needs to compute, and as soon as the interval term r : \mathbb {I} becomes equal to a constant. Prior to the introduction of the frontier of instability, the neutrals are embedded into the normals at base types unconditionally, i.e. for each neutral form {\color {DarkRed}{e}} : \mathsf {ne}\,\mathsf {bool}, we have a normal form {\color {DarkBlue}{\lfloor }}{e}{\color {DarkBlue}{\rfloor }} : \mathsf {nf}\,\mathsf {bool}.
Now that neutrals are equipped with frontiers of instability, a more refined notion of normal form is needed: when {\color {DarkRed}{e}} is a neutral form, the corresponding normal form should contain (recursively) normal forms for e that are defined under the frontier of instability \boldsymbol {\partial }\,{\color {DarkRed}{e}}. To be more concrete,
let x : {\mathsf {tt}}\mathrel {{\sim }_{\mathsf {bool}}}{\mathsf {tt}} be a variable of path type and r : \mathbb {I} is a term; then {{\color {DarkRed}{\mathsf {var}}}\,x}\mathrel {{\color {DarkRed}{@}}}{r}:\mathsf {ne}\,{\mathopen {}\left ({\mathsf {tt}}\mathrel {{\sim }_{\mathsf {bool}}}{\mathsf {tt}}\right )\mathclose {}} is a neutral form for the term xr whose frontier of instability is the boundary (r = 0) \lor (r = 1); the corresponding normal form must therefore glue onto {{\color {DarkRed}{\mathsf {var}}}\,x}\mathrel {{\color {DarkRed}{@}}}{r} additional normal forms for x0 and
x1. We refer to the process of completing a neutral with additional data defined on its frontier of instability as stabilization; the stabilized normal form of xr is then written
{\color {DarkBlue}{\lfloor }}{{{\color {DarkRed}{\mathsf {var}}}\,x}\mathrel {{\color {DarkRed}{@}}}{r} \mid r = 0 \hookrightarrow {\color {DarkBlue}{\mathsf {tt}}}, r = 1 \hookrightarrow {\color {DarkBlue}{\mathsf {tt}}}}{\color {DarkBlue}{\rfloor }}
where {\color {DarkBlue}{\mathsf {tt}}} is the normal form representing the term \mathsf {tt}
Just as the embedding of neutrals into normals is “stabilized” by a com patible normal form defined on the neutral’s frontier of instability, so too must the Tait saturation yoga be adjusted. Conventionally one requires the computability predicate for a type A to be equipped with a function that takes neutral forms {\color {DarkRed}{e}} of terms e : A to computability witnesses for the same term. In the stabilized Tait saturation yoga, we strengthen the induction hypothesis to require for each neutral form {\color {DarkRed}{e}} a function that extends a computability witness defined only on the frontier of instability \boldsymbol {\partial }{\color {DarkRed}{e}} to a computability witnessed defined everywhere
The twin innovations of frontiers of instability and stabilization then suffice to adapt the synthetic normalization argument of Chapter 5 to a proof of normalization (and thus decidability) for cubical type theory.