Axiom K (type theory)

Axiom K is summarized by the following rule

\frac
{ \Gamma\vdash p:x=x\quad}
{ \Gamma\vdash p=\textsf{refl} }

There is only one proof of any equality, and that proof is \textsf{refl}. This axiom is invalidated in Homotopy Type Theory.

References

• nLab: UIP and Axiom K