工作在阿格達Peano公理和打一點的關鍵點

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

PA6 = cong

讓我無處，我知道聰我要求您提供REFL平等和類型，但我，不知道我應該什麼類型的供應。想法？

這是在大學的一個小任務，所以我寧願有人證明我錯過了什麼，而不是寫出相應的答案，但我會很感激任何程度的支持。

通過我已創建的系統的性質，我不得不實現我有兩個等價，因此需要使用等效方法REFL

因此滿足我類型簽名AGDA接受：PA6 refl = refl

希望有幫助

2010-04-05 07:03:33 Schroedinger

請發表多一點的解決方案，因此它可以幫助別人誰擁有類似的問題（至少你定義了ℕ和_≡_，或者lib版本和模塊名稱，如果它們來自庫）。 Upvote將遵循:) – fishlips 2010-04-05 09:14:31

您的PA6表示≡是對稱。

這可以在Relation.Binary.PropositionalEquality模塊的標準庫中找到。

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

（這個問題是很老，但我張貼用於在認爲絆倒未來的讀者的利益。）

2010-11-07 19:48:35 glguy

回答