在Agda中实现路径归纳

Question

我无法理解为什么我的路径归纳在类型检查时出现了问题。它说“C x 应该是一个函数类型，但它不是”，当引用 C（refl x） 时。也许我的 refl 的定义有误，或者我的 {} 和 () 有问题？

data _≡_ {A : Set}(a : A) : A → Set where
      refl : a ≡ a
infix 4 _≡_

pathInd : ∀ {u} → {A : Set} → 
          (C : {x y : A} → x ≡ y → Set u) → 
          (c : (x : A) → C (refl x)) → 
          ({x y : A} (p : x ≡ y) → C p)
pathInd C c (refl x) = c x

- user2154420

Answer 1

refl不是一个函数。这里是你需要的定义：

pathInd : ∀ {u} → {A : Set} → 
          (C : {x y : A} → x ≡ y → Set u) → 
          (c : (x : A) → C {x} refl) → 
          ({x y : A} (p : x ≡ y) → C p)
pathInd C c {x} refl = c x

此外，使用此定义的_≡_，您的pathInd可以正常工作：

data _≡_ {A : Set} : A → A → Set where
      refl : ∀ a -> a ≡ a

- effectfully