• 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 = reflK 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.

• What is axiom K
• Pattern matching without K