## § 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.