相关疑难解决方法(0)

这是使路径归纳在Agda中起作用的后续问题

我想知道这个结构何时可能更具表现力.在我看来,我们总是这样表达:

f : forall {A} -> {x y : A} -> x == y -> "some type"
f refl = instance of "some type" for p == refl

在这里,Agda将根据c : (x : A) -> C refl与该问题相同的示例进行路径归纳:

pathInd : forall {A} -> (C : {x y : A} -> x == y -> Set)
                     -> (c : (x : A) -> C refl)
                     -> {x y : A} -> (p : x == y) -> C …