Lifting proof-relevant unification to higher dimensions

In a dependently typed language such as Coq or Agda, unification can be used to discharge equality constraints and detect impossible cases automatically. By nature of dependent types, it is necessary to use a proof-relevant unification algorithm where unification rules are functions manipulating equality proofs. This ensures their correctness but simultaneously sets a high bar for new unification rules. In particular, so far no-one has given a satisfactory proof-relevant version of the injectivity rule for indexed datatypes. In this paper, we describe a general technique for solving equations between constructors of indexed datatypes. We handle the main technical problem—generalization over equality proofs in the indices—by introducing new equations between equality proofs. Borrowing terminology from homotopy type theory, we call them higher-dimensional equations. To apply existing one-dimensional unifiers to these higher-dimensional equations, we show how unifiers can be lifted to a higher dimension. We show the usefulness of this idea by applying it to the unification algorithm used by Agda, though it can also be applied in languages that support identity types but not general indexed datatypes.status: publishe