在 Agda 中研究 Peano Axioms 并遇到了一些症结
PA6 : ∀{m n} -> m ≡ n -> n ≡ m
是我试图解决和支持的公理，我尝试使用 cong （来自核心库），但是 cong 构造函数遇到麻烦，
PA6 = cong
我无处可去，我知道对于 cong，我需要提供相等的 refl 和一种类型，但我不确定我应该提供什么类型。有想法吗？
这是大学的一项小作业，所以我宁愿有人证明我错过了什么，而不是写出实际的答案，但我会感谢任何程度的支持。
PA6 : ∀{m n} -> m ≡ n -> n ≡ m
is the axiom I am trying to solve and support, I've tried using a cong (from the core library) but am having troubles with the cong constructor
PA6 = cong
gets me nowhere, I know for cong I am required to supply a refl for equality and a type, but I'm, not sure what type I'm supposed to supply. Ideas?
This is for a small assignment at University, so I'd rather someone demonstrate what I've missed rather than write the acutual answer, but I'd appreciate any degree of support.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
您的 PA6 表示 ≡ 是对称的。
这可以在 Relation.Binary.PropositionalEquality 模块的标准库中找到。
（这个问题已经很老了，但我发布这个问题是为了将来偶然发现它的读者的利益。）
Your PA6 says that ≡ is symmetric.
This can be found in the standard library from the Relation.Binary.PropositionalEquality module.
(This question is pretty old, but I'm posting for the benefit of future readers that stumble upon it.)
根据我创建的系统的性质，我必须意识到我有两个等价，因此需要使用等价方法 refl
从而满足我接受的类型签名 agda：
PA6 refl = refl希望帮助
By the nature of the system that I had created, I had to realise I had two equivalences and thus needed to use the equivalence method refl
Thus to satisfy my type signature agda accepted:
PA6 refl = reflhope that helps