{-# OPTIONS --safe --without-K #-}
open import Agda.Primitive renaming (Set to 𝒰)
open import Agda.Builtin.Equality

module UIPK (UIP : ∀ {ₙ} {A : 𝒰 ₙ} {x y : A} (p q : x ≡ y) → p ≡ q)
            where

J : ∀ {ₙ ₘ} {A : 𝒰 ₙ} {x y : A} (P : (a b : A) → a ≡ b → 𝒰 ₘ) → P x x refl → (p : x ≡ y) → P x y p
J _ Prefl refl = Prefl

square : ∀ {ₙ} {A : 𝒰 ₙ} {x y z w : A} → x ≡ z → y ≡ w → x ≡ y → z ≡ w
square refl refl p = p

transp : ∀ {ₙ ₘ} {A : 𝒰 ₙ} {x y : A} (P : A → 𝒰 ₘ) → x ≡ y → P x → P y
transp P refl Px = Px

K : ∀ {ₙ ₘ} {A : 𝒰 ₙ} {x : A} (P : x ≡ x → 𝒰 ₘ) → P refl → (p : x ≡ x) → P p
K {x = x} P Prefl p = (J (λ a b q → (r : a ≡ x) → (s : b ≡ x) → P (square r s q))
                         (λ a b → transp P (UIP refl (square a b refl)) Prefl)
                         p) refl refl