获得路径归纳以在 Agda 中工作 [英] Getting path induction to work in Agda

问题描述

我不明白为什么我的路径归纳没有正确地进行类型检查.当提到 C (refl x) 时，它说C x 应该是一个函数类型，但它不是".也许我对 refl 的定义是错误的，或者我的 {} 和 () 有什么问题?

I can't figure out why my path induction isn't type checking correctly. It says "C x should be a function type, but it isn't" when referring to C (refl x). Perhaps my definition of refl is wrong or is there something wrong with my {}'s and ()'s?

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

推荐答案

refl 不是函数.这是您需要的定义:

refl is not a function. Here is the definition you need:

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 与 _≡_ 的这个定义一起正常工作:

Also, your pathInd works properly with this definition of _≡_:

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

这篇关于获得路径归纳以在 Agda 中工作的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！