Can we derive Uniqueness of Equality/Identity Proofs in Agda without pattern matching (using only J & K)?

Question

I'm trying to construct solutions in Agda to the exercises given in this introduction to Type Theory & Homotopy Type Theory.

Given the dependent eliminators for equality E⁼ (aka J) and K that I've defined in Agda like so:

J : {A : Set}
   → (C : (x y : A) → x ≡ y → Set)
   → ((x : A)   → C x x refl)
   → (x y : A) → (p : x ≡ y) → C x y p
J C f x .x refl = f x 

K : {A : Set}
  → (C : (x : A) → x ≡ x → Set)
  → ((x : A) → C x refl)
  → (x : A) → (p : x ≡ x) → (C x p)
K P f x refl = f x

Exercise 16 (page 13) is to derive the Uniqueness of Equality/Identity Proofs (UEP) using only the eliminators.

I know that UEP is provable in Agda via pattern matching thanks to axiom K like so:

uep : {A : Set}
    → (x y : A)
    → (p q : x ≡ y)
    → (p ≡ q)
uep x .x refl refl = refl

but the article seems to imply that it should be possible to derive a proof without pattern matching just like sym , trans, and resp can be proved using only the recursor R⁼ :

R⁼ : {A : Set} (C : A → A → Set)
     → (∀ x → C x x)
     → ∀ {x y : A} → x ≡ y → C x y 
R⁼ _ f {x} refl = f x 


sym : ∀ {A : Set} → {x y : A} → x ≡ y → y ≡ x
sym {A} = R⁼ {A} ((λ x y → y ≡ x)) (λ x → refl)

trans : ∀ {A : Set} → (x y z : A) → x ≡ y → y ≡ z → x ≡ z
trans {A} x y z  = R⁼ {A} (λ a b → (b ≡ z → a ≡ z)) (λ x₁ → id)

resp : {A B : Set} → (f : A → B) → {m n : A} → m ≡ n → f m ≡ f n
resp {A} {B} f = R⁼ {A}  (λ a b → f a ≡ f b) (λ x → refl)

Given that UEP is a direct consequence of K my intuition is this should surely be possible but I've not been successful so far. Is the following provable with some combination of J and K? :

uep : {A : Set}
    → (x y : A)
    → (p q : x ≡ y)
    → (p ≡ q)
uep x y p q = {!!}

user3237465 user3237465 · Accepted Answer · 2020-01-01T16:00:35

If you write

uep : {A : Set}
    → (x y : A)
    → (p q : x ≡ y)
    → (p ≡ q)
uep = J (λ _ _ p → ∀ q → p ≡ q) {!!}

and look into the hole, you'll see its type is

(x : A) (q : x ≡ x) → refl ≡ q

So J allows to turn the x ≡ y arguments into an x ≡ x one and from there K can handle the rest.

Full definition:

uep : {A : Set}
    → (x y : A)
    → (p q : x ≡ y)
    → (p ≡ q)
uep = J (λ _ _ p → ∀ q → p ≡ q) (K (λ _ q → refl ≡ q) (λ _ → refl))

Can we derive Uniqueness of Equality/Identity Proofs in Agda without pattern matching (using only J & K)?

1 Answers