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