Uniqueness of identity proofs

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 ${\displaystyle x=x}$is equal to the trivial reflexivity proof.

These axioms thus have the respective types:

${\displaystyle {\mathsf {UIP}}:\prod _{X:{\mathsf {Type}}}\prod _{x,y:X}\prod _{p,q:x=y}p=q}$

${\displaystyle {\mathsf {K}}:\prod _{X:{\mathsf {Type}}}\prod _{x:X}\prod _{p:x=x}p={\mathsf {refl}}_{x}}$

In intensional type theory with the standard definition of the identity type as an indexed inductive type, UIP and K are unprovable, as first proved by Martin Hoffman and Thomas Streicher using a groupoid model. While this might first seem surprising since the identity type has just one constructor (reflexivity), the apparent contradiction is resolved by the fact that the identity type inductively defines the identity type family ${\displaystyle x=\bullet }$rather than the single type ${\displaystyle x=y}$. According to the identity type's induction principle, given an element ${\displaystyle x:X}$and a type family ${\displaystyle C:\prod _{y:X}\prod _{p:x=y}{\mathsf {Type}}}$as well as an element ${\displaystyle c:C(x,{\mathsf {refl}}_{x})}$, we may build a function ${\displaystyle f:\prod _{y:X}\prod _{p:x=y}C(y,p)}$satisfying the definitional equality ${\displaystyle f(x,{\mathsf {refl}}_{x})\equiv c}$. Informally speaking, the reason why this does not allow to prove, e.g., axiom K, is that the property to be proven should be ${\displaystyle C(y,p):\equiv p={\mathsf {refl}}_{x}}$, but this is ill-typed as ${\displaystyle p}$has type ${\displaystyle x=y}$while ${\displaystyle {\mathsf {refl}}_{x}}$has type ${\displaystyle x=x}$.

The axioms UIP and K are equivalent. Indeed, K is a special case of UIP, while UIP can be deduced from K by equality induction on ${\displaystyle p}$.

In Martin-Löf's original extensional type theory, UIP and K are provable. This is because extensional type theory includes the so-called equality reflection rule that derives a judgmental equality from a propositional equality, which makes the function ${\displaystyle C(y,p):\equiv p={\mathsf {refl}}_{x}}$well-typed. However, this type theory is not used in practice in proof assistants because it removes parts of proofs from the proof terms.

Martin Hofmann proved that together with functional extensionality, UIP and K in fact sufficient to capture the differences between intensional and extensional Martin-Löf type theory: extensional MLTT is conservative over intensional MLTT with the addition of the axioms of functional extensionality and UIP (or K).

In homotopy type theory, UIP has the interpretation that every type has a trivial homotopical structure where any two paths between the same points are homotopical (equivalently, as in axiom K, all loops are contractible). This is disprovable, as it contradicts the univalence axiom. However, many naturally occurring types ${\displaystyle X}$do satisfy that any two equality proofs between elements of ${\displaystyle X}$are equal. Such types are called sets, or h-sets, or homotopy 0-types, or 0-truncated types.