Parametric Cubical Type Theory and HIT Free Theorems

Prerequisites. Direct starred prerequisites: Chapter 60. No later core chapter depends on this route.

Opening obstruction

Cubical paths internalize equality while parametric bridges require an affine dimension discipline; identifying the dimensions destroys one of the needed structural laws.

Development contract

Freeze the two-dimensional Path/Bridge/Gel/extent syntax, prove Cavallo–Harper relativity and the binary smash-product free theorem, and build the book-owned affine-dimension checker. The source’s incomplete Bridge/Gel presheaf and Kan obligations are excluded rather than printed as a proof.