Martin Escardo 2012. We use the UIP (uniqueness of identity proofs) for definable types only, as opposed to universally quantified or hypothetical types, in fact for ₂, ℕ and ℕ∞ and no other type. It is known that the UIP is provable for definable types from the propositional axiom of extensionality, which we are assuming (cf. Hofmann & Streicher's paper on the groupoid interpretation). It would be too painful and time consuming to actually define the UIP for each type we need it using extensionality. Hence in this module we prove the UIP with pattern matching, which amounts to the K axiom, but we promise to use it for definable types only. (grep all Agda files for UIP to make sure!) \begin{code} module UIP where open import Equality UIP : (X : Set) → ∀{x x' : X} → ∀(r s : x ≡ x') → r ≡ s UIP X {x} {.x} refl refl = refl UIP-refl : (X : Set) → ∀{x : X} → ∀(r : x ≡ x) → r ≡ refl UIP-refl X {x} r = UIP X {x} {x} r refl \end{code}