Agda Implementors’ Meeting edition:XIX location:Paris date:22-28 May 2014
Dependent pattern matching is a fundamental technique for writing Agda code, but by default it implies the K axiom, making it incompatible with homotopy type theory. The —without-K flag imposes a syntactic check for definitions that rely on K, however so far it lacked a formal correctness proof. In this talk, I propose a new specification for —without-K that works by limiting the unification algorithm used for case splitting. It is strictly more liberal than the current specification, particularly when pattern matching on parametrized datatypes, and at the same time it solves a currently open problem with the syntactic check. More importantly, it allows a translation of definitions by pattern matching to eliminators in the style of Goguen et al. (2006) without relying on the K axiom, thus proving its correctness. So with it, we can finally stop worrying when using pattern matching in HoTT.