Structural Metatheory for Finitary One-Dimensional Higher Inductive Types

This entry develops the structural metatheory of a finitary, one-dimensional, nondependent calculus of higher inductive types directly in Isabelle/HOL. Its inductive syntax, raw typing relation, reduction relation, and signature environment uniformly describe ordinary inductive types and higher inductive types.

Signatures declare finite point and path constructors with checked endpoints. Path methods must respect both declared faces. A finite open-term boundary criterion checks each method once under canonical constructor arguments, and simultaneous substitution transports those obligations to every typed instance. Strong normalization and confluence yield a canonical normal-form comparison theorem: typed terms are joinable exactly when their unique normal forms agree. The selected canonical function uses Hilbert choice and is not an executable normalizer.

The development proves weakening, term and dimension substitution, subject reduction, progress, strong normalization, Church-Rosser confluence, unique normal forms, canonicity, and empty-signature consistency. It also formalizes the boundary-computation square and dimension-capture counterexample that motivate the calculus design.