PLS Lab

Uniqueness of Identity Proofs (UIP)

In intensional type theory, the principle of uniquness of identity proofs (UIP) stipulates that objects can only be equal in one way.

Formulated as a rule, the UIP at a type \Gamma \vdash A \textsf{ type} states the existence of a construction

\frac{
	\Gamma \vdash A \textsf{ type}
  	\quad
  \Gamma \vdash M, N : A
  	\quad
  \Gamma \vdash P, Q : \textsf{Id}_A(M, N)
}{
	\Gamma \vdash \textsf{uip}_A(M, N, P, Q) : \textsf{Id}_{\textsf{Id}_A(M, N)}(P, Q)
}

That is: given any two terms M, N : A, and two proofs P, Q : \textsf{Id}_A(M, N) that they are propositionally equal, those two proofs P and Q are propositionally equal themselves.

This may be equivalently formulated as an axiom:

\textsf{uip}_A : (x, y : A) \to (p, q : \textsf{Id}_A(x, y)) \to \textsf{Id}_{\textsf{Id}_A(x, y)}(p, q)

Unlike its equivalent axiom, Axiom K, \textsf{uip}_A does not have good computational behaviour: see the nLab.

Because of equality reflection, this rule is trivially derivable in extensional type theory.

Pattern-matching allows one to construct an inhabitant of UIP: given variables p, q : \textsf{Id}_A(M, N), pattern-match on both of them to reduce them to \textsf{refl}(X) with X = M = N, and then return \textsf{refl}(\textsf{refl}(X)).

Hedberg's theorem implies that UIP holds at types with decidable equality.

The groupoid model of type theory was constructed with the explicit purpose of refuting UIP. As at least one of its models refutes it, intensional Martin-Löf type theory does not prove UIP.

References