module UIP where open import Equality open import Level uip : {ℓ : Level} {A : Set ℓ} {x y : A} {p q : x ≡ y} → ----------- p ≡ q uip {p = refl} {refl} = refl