在Agda中研究Peano公理，并遇到了一点症结

Question

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

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

PA6 = cong

无处可寻，我知道对于cong，我需要提供一个用于相等的refl和一个类型，但我不确定我应该提供什么类型。想法？

这是在大学里的一个小任务，所以我宁愿有人证明我错过了什么，而不是写出实际的答案，但我希望得到任何程度的支持。

Answer 1

根据我创建的系统的性质，我必须意识到我有两个等价方法，因此需要使用等价方法refl

因此，为了满足我接受的类型签名agda：PA6 refl = refl

希望这能有所帮助

Answer 2

你的PA6说≡是对称的。

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

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

(这个问题很老了，但我把它贴出来是为了给偶然发现它的未来读者带来好处。)