PA6 : ∀{m n} -> m ≡ n -> n ≡ m
是我要解决和支持的公理，我尝试过使用 cong（来自核心库），但是 cong 构造函数有问题
PA6 = cong
让我无处可去，我知道 cong 我需要提供一个 refl 来表示相等和一个类型，但我不确定我应该提供什么类型。想法？
这是大学的一项小任务，所以我宁愿有人展示我错过的东西，而不是写出准确的答案，但我会感谢任何程度的支持。
问问题
694 次
2 回答
7
你的 PA6 说 ≡ 是对称的。
这可以在 Relation.Binary.PropositionalEquality 模块的标准库中找到。
sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
（这个问题已经很老了，但我发帖是为了让将来偶然发现它的读者受益。）
于 2010-11-07T19:48:35.483 回答
3
根据我创建的系统的性质，我必须意识到我有两个等价，因此需要使用等价方法 refl
因此，为了满足我接受的类型签名 agda：PA6 refl = refl
希望有帮助
于 2010-04-05T07:03:33.317 回答