Strict Equality in Higher Identity Types: Axioms, Completeness, Decidability

Overview & Synopsis

Reasoning about higher identity types uses two equalities, strict equality and equivalence of cells witnessed by a path. Strict equality is a congruence for every operation on cells, but associativity and the identity laws fail for it. Equivalence of cells satisfies those two laws, but it is not a congruence. Representations of higher identity types often conflate equational properties that hold strictly with those that hold only up to a path. We separate the two and axiomatize the former, introducing SEq, an equational theory generated by eleven axioms for strict equality between cells. We prove soundness and completeness for homotopy models, and completeness already over finite CW-complexes. Nine of these axioms form a strongly normalizing rewrite system whose normal forms are unique up to picture equivalence, and the resulting word problem is decidable in exponential time. We also give presheaf models over a cubical base category in which composition arises from a pushout in the base category itself, without requiring Kan filling structure. The same pushout structure provides explicit higher-dimensional witnesses for associativity and the identity laws.