Eliminating dependent pattern matching without K

Dependent pattern matching is an intuitive way to write programs and proofs in dependently typed languages. It is reminiscent of both pattern matching in functional languages and case analysis in on-paper mathematics. However, in general, it is incompatible with new type theories such as homotopy type theory (HoTT). As a consequence, proofs in such theories are typically harder to write and to understand. The source of this incompatibility is the reliance of dependent pattern matching on the so-called K axiom – also known as the uniqueness of identity proofs – which is inadmissible in HoTT. In this paper, we propose a new criterion for dependent pattern matching without K, and prove it correct by a translation to eliminators in the style of Goguen et al. (2006 Algebra, Meaning, and Computation). Our criterion is both less restrictive than existing proposals, and solves a previously undetected problem in the old criterion offered by Agda. It has been implemented in Agda and is the first to be supported by a formal proof. Thus, it brings the benefits of dependent pattern matching to contexts where we cannot assume K, such as HoTT.