UIP

Definition

Let $\Gamma$ be a type theoretic context, $A$ be a type, and $x,y$ be terms such that $\Gamma ⊢x,y:A$. UIP states the following: $\Gamma ;x,y:A;p,q:x{=}_{A}y⊢p{=}_{x=y}q$

Remarks

UIP is inconsistent with univalence, since there are two distinct proofs that $2=2$, and these are probably distinct.