Axiom K is summarized by the following rule
Γ⊢p:x=xΓ⊢p=refl\frac { \Gamma\vdash p:x=x\quad} { \Gamma\vdash p=\textsf{refl} } Γ⊢p=reflΓ⊢p:x=x
There is only one proof of any equality, and that proof is refl\textsf{refl}refl. This axiom is invalidated in Homotopy Type Theory.