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

Keri D'Angelo, Liron Cohen, Luke Serafin +1

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 cell…