我们可以在不进行模式匹配（仅使用J和K的情况下，在Agda中获得等式/身份证明的唯一性吗？

Question

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

考虑到我在Agda中定义的相等性E ⁼（又名J）和K的从属消除器：

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页）使用only消除符来推导相等性/身份证明（UEP）的唯一性。

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

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

但是文章似乎暗示，应该可以仅使用递归R ⁼来证明不进行模式匹配的证明，就像sym，trans和resp一样：

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，然后从那里K可以处理其余部分。

完整定义：

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