Getting inducted to work at Agda
I can't figure out why my path induction is wrong. It says "C x should be a function type, but it is not" when it refers to C (refl x). Perhaps my refl definition is wrong, or is there something wrong with my {} and () '?
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
+2
source to share
1 answer
refl
is not a function. Here's a definition:
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
Also, yours pathInd
works correctly with this definition _≡_
:
data _≡_ {A : Set} : A → A → Set where
refl : ∀ a -> a ≡ a
+5
source to share