equality - 我们可以在没有模式匹配的情况下(仅使用 J & K)在 Agda 中导出平等/身份证明的唯一性吗？

Question

我正在尝试在 Agda 中构建 this 中给出的练习的解决方案类型论和同伦类型论简介。

鉴于我定义的相等的依赖消除器 E⁼(又名 J)和 K在 Agda 中像这样:

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

练习 16(第 13 页)是仅使用消除器来导出平等/身份证明的唯一性 (UEP)。

由于公理 K，我知道 UEP 可以通过模式匹配在 Agda 中证明，如下所示:

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

但是这篇文章似乎暗示应该可以在没有模式匹配的情况下导出证明，就像 sym 、 trans 和 resp 一样可以仅使用递归器 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)

鉴于 UEP 是 K 的直接结果，我的直觉是这肯定是可能的，但到目前为止我还没有成功。以下是否可以通过 J 和 K 的某种组合来证明？ :

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

Answer 1

如果你写

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

观察这个洞，你会发现它的类型是

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

因此，J 允许将 x ≡ y 参数转换为 x ≡ x 1，然后从那里 K > 可以处理剩下的事情。

完整定义:

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