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}