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