§ Axiom K versus UIP
- UIP: all proofs of equality are equal:
(p q: Eq A a a'): Eq (Eq A a a') p q - Axiom K: all proofs of equality are equal to refl:
(p: Eq A a a): Eq (Eq A a a) p (refl A a)
§ Where is K used in pattern matching
-
K can be proven by depenedent pattern matching on the identity type!
K : (p : x = x) -> p = refl
K refl = refl
In fact, Conor McBride showed in his thesis ("Dependently typed functional
programs and their proofs (2000)") that K is the only thing that dependent
pattern matching really adds to dependent type theory.
Indexed type definitions could be interpreted as non-indexed definitions with
extra equality proofs in constructors that set the indices. In Agda, what
ultimately matters is the method for unifying indices in dependent pattern
matching, so ≡ can be seen as a wrapper for whatever notion of equality
stems from pattern matching. But pattern matching is ultimately reducible to
applications of either Axiom K or Axiom J. So, even in the context of Agda,
you should just look at the bare-bones refl/Axiom J definition of equality to
see where the extra equalities come from.