---
tag: 5H3JRM0WSS
kind: statement
role: proposition
name: Uniqueness of identity proofs
aliases: [axiom-k, streichers-axiom-k]
sources:
  - wikipedia: en:79140369@r1277745965
    locator: Uniqueness of identity proofs
    note: adopted
    mention: wikipedia://en/79140369
    sections: [Statement]
same_as:
  wikidata: Q132573452
  wikipedia: Uniqueness of identity proofs
inventory: [PW69FH3KNF]
---

## 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.