當兩者都具有相同的標準形式---我認爲---和命題相等僅僅是定義相等的數據類型表示時， - 我認爲---;那麼不應該在命題上平等是可以確定的嗎？也就是說，我們可以編寫一個鍵入的函數似乎是合理的，我們可以編寫一個函數命題等式的可判定性
∀{A : Set} → (x y : A) → Dec(x ≡ y)。
因爲我們無法在參數上進行模式匹配，所以我不能寫這樣的函數，但我覺得它應該是可能的：再次，減少到正常形式並檢查語法標識。
任何見解都會有所幫助！在AGDA
兩個術語說是definitionally正好相等時 它們都具有相同的正常形態
最多αη轉換。
和命題平等僅僅是定義性平等的數據類型的表示
命題平等說「你實例一些自由變量後，這兩個詞將成爲definitionally平等」（「一些」可以爲0或者全部）（「實例化」也可以改變）。
E.g.
double-double : (n : ℕ) -> n + n ≡ 2 * n
清楚，n + n在語法上不等於2 * n，但對於任何規範n（0, 1, 2...）的n + n結果在語法上是相等的2 * n結果 - 這就是double-double說。而對於任何規範的「n」部分，我們通過歸納來證明double-double（儘管在更復雜的系統中，定義相等基於超級編譯或者存在內置證明者，n + n定義上等於2 * n）。
但有時候，歸納假設應該如何看起來不那麼明顯。當你需要推廣一個方程。正如你所預料的那樣，「這個隨意的東西是可證明的嗎？」沒有任何決定性的程序。因此命題平等是不可判定的。此外，你不能既不證明也不反駁像
(λ n -> 1 + n) ≡ (λ n -> n + 1)
沒有額外的公設。
但是你真的可以檢查語法平等：
_≟_ : ∀ {α} {A : Set α} -> (x y : A) -> Maybe (x ≡ y)
它說：「如果兩個術語在語法上是平等的，那麼他們是平等的propositionally，否則我們不知道他們是否相等propositionally與否」 。但Agda沒有這樣的內置功能。