{-# OPTIONS --safe #-}
module KUIP where

open import Agda.Primitive renaming (Set to 𝒰)
open import Agda.Builtin.Equality

UIP : ∀ {ₙ} {A : 𝒰 ₙ} {x y : A} (p q : x ≡ y) → p ≡ q
UIP refl refl = refl