Proof of K and UIP from elimination rule of John Major equality

JM.agda

{-# OPTIONS --with-K #-}
module JM where

open import Level

infix 4 _≅_

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
  ≅-refl : x ≅ x

≅-elim
  : ∀ {a} {A : Set a} {x : A} {p}
  → (P : (y : A) → (x ≅ y) → Set p)
  → P x ≅-refl → (y : A) → (x≅y : x ≅ y) → P y x≅y
≅-elim P q y ≅-refl = q

JMProp.agda

{-# OPTIONS --without-K #-}
module JMProp where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
open import JM

≅-sym : ∀ {a} {A : Set a} {x y : A} → x ≅ y → y ≅ x
≅-sym {_} {_} {x} {y} = ≅-elim (λ y _ → y ≅ x) ≅-refl y

≅-subst : ∀ {a} {A : Set a} {p} (P : A → Set p) → {x y : A} → x ≅ y → P x → P y
≅-subst P {x} {y} x≅y px = ≅-elim (λ y _ → P y) px y x≅y

≅-UIP : ∀ {a} {A : Set a} {x y : A} → (x≅y : x ≅ y) → (x≅y) ≅ ≅-refl {a} {A} {x}
≅-UIP {a} {A} {x} {y} x≅y = ≅-elim (λ _ x≅y → x≅y ≅ ≅-refl {a} {A} {x}) ≅-refl y x≅y

≅-K : ∀ {a} {A : Set a} {x : A} {p} (P : x ≅ x → Set p) → P ≅-refl → (x≅x : x ≅ x) → P x≅x
≅-K P pr x≅x = ≅-subst P (≅-sym (≅-UIP x≅x)) pr

≡→≅ : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≅ y
≡→≅ refl = ≅-refl

≅→≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
≅→≡ {_} {_} {x} {y} = ≅-elim (λ y _ → x ≡ y) refl y

≡→≅→≡ : ∀ {a} {A : Set a} {x y : A} → (x≡y : x ≡ y) → ≅→≡ (≡→≅ (x≡y)) ≡ x≡y
≡→≅→≡ refl = refl

K : ∀ {a} {A : Set a} {x : A} {p} (P : x ≡ x → Set p) → P refl → (x≡x : x ≡ x) → P x≡x
K P pr x≡x = subst P (≡→≅→≡ x≡x) lem
  where
    lem : P (≅→≡ (≡→≅ x≡x))
    lem = ≅-K (λ x≅x → P (≅→≡ x≅x)) pr (≡→≅ x≡x)

UIP : ∀ {a} {A : Set a} {x : A} → (x≡x : x ≡ x) → x≡x ≡ refl
UIP = K (λ x≡x → x≡x ≡ refl) refl