haskell - 在 Agda 中研究 Peano Axioms 并遇到了一些症结

PA6 : ∀{m n} -> m ≡ n -> n ≡ m

是我试图解决和支持的公理，我试过使用 cong(来自核心库)但在 cong 构造函数上遇到了麻烦

PA6 = cong

让我无处可去，我知道 cong 我需要提供平等和类型的 refl，但我不确定我应该提供什么类型。想法？

这是大学的一个小任务，所以我宁愿有人证明我错过了什么，而不是写下实际答案，但我很感激任何程度的支持。

最佳答案

你的 PA6 说 ≡ 是对称的。

这可以在 Relation.Binary.PropositionalEquality 模块的标准库中找到。

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

(这个问题已经很老了，但我发帖是为了将来偶然发现它的读者。)

关于haskell - 在 Agda 中研究 Peano Axioms 并遇到了一些症结，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/2576870/