§ Axiom K versus UIP

§ Where is K used in pattern matching

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.