我剛剛學習Agda，但我不明白，當我試圖證明身份超過Addition時，我發現左身份是微不足道的證據。爲什麼留在「加法」身份是微不足道的證據，但正確的身份不是？
left+identity : ∀ n -> (zero + n) ≡ n
left+identity n = refl
但它對於正確的身份不是這樣。
right+identity : ∀ n -> (n + zero) ≡ n
right+identity zero = refl
right+identity (suc n) = cong suc (right+identity n)
我不明白原因。請解釋。謝謝。
問題是依賴類型理論是如何處理平等的。通常，加法的定義是：
_+_ : Nat -> Nat -> Nat
zero + m = m -- (1)
(suc n) + m = suc (n + m) -- (2)
請注意，等式一意味着左身份。當您有：
forall n -> 0 + n = n
Agda的類型檢查器可以使用加法的等式（1）來驗證等式是否成立。請記住，命題平等構造（refl）具有類型
refl : x == x
所以，當你使用refl作爲左身份的證明，阿格達會盡量減少平等（歸他們）的兩側，檢查它們是否確實是平等的。使用加法的定義，通過等式（1），左邊的身份是立即的。
但是對於正確的身份來說，這並不符合定義。需要注意的是，當我們有
n + 0 == n
阿格達的類型檢查，從而無法使用除了公式來檢查這的確平等持有。證明這種平等的唯一方法是使用歸納（或者，如果您願意，遞歸）。
希望這可以幫助你。