Uniqueness of identity proofs

Statement

In type theory, uniqueness of identity proofs (UIP) is a possible axiom for dependent type theory which asserts that any two proofs of the same equality are themselves equal. An equivalent and closely related axiom is Streicher's axiom K, which asserts that any proof of an equality $x = x$ is equal to the trivial reflexivity proof.