我无法理解为什么我的路径归纳在类型检查时出现了问题。它说“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