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

Question

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

是我试图解决和支持的公理，我尝试使用 cong (来自核心库)，但在使用 cong 构造函数时遇到问题

PA6 = cong

让我无处可去，我知道对于 cong，我需要提供相等性和类型的反射，但我不确定我应该提供什么类型。有想法吗？

这是大学的一项小作业，所以我宁愿有人展示我错过的内容，而不是写出实际的答案，但我会感谢任何程度的支持。

Answer 1

你的 PA6 说 ≡ 是对称的。

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

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

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