types - 获得路径归纳以在 Agda 中工作

Question

我不明白为什么我的路径归纳没有正确地进行类型检查。当提到 C (refl x) 时，它说“C 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

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