{-# 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