Uniqueness of identity proofs

In type theory, uniqueness of identity proofs (UIP) refers to the axiom stating that any two identifications $p,q:x\equiv y$ are themselves identified.