我们可以在没有模式匹配的情况下（仅使用 J 和 K）在 Agda 中推导出 Equality/Identity 证明的唯一性吗？

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 页）是使用仅消除器推导 Equality/Identity 证明 (UEP) 的唯一性。

我知道 UEP 在 Agda 中可以通过模式匹配来证明，这要归功于公理 K，如下所示：

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 参数，然后 K 可以处理其余参数。

完整定义：

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

我们可以在没有模式匹配的情况下（仅使用 J 和 K）在 Agda 中推导出 Equality/Identity 证明的唯一性吗？

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

equality

agda

homotopy-type-theory