定義的同値

カーネルの定義的同値 $\equiv$ は、次の簡約で互いに移り合うことを中心に生成される同値関係である。

• β：$(\mathsf{fun}\ x\Rightarrow b)\,a\equiv b[x:=a]$。
• δ：定義された定数をその定義で置き換える。
• ι：再帰子を構成子に適用したものを計算する（例：Nat.rec z s (n+1) ≡ s n (Nat.rec z s n)）。Quot.lift の計算規則もこれに含める。
• ζ：let x := v; b $\equiv b[x:=v]$。
• η：$f\equiv(\mathsf{fun}\ x\Rightarrow f\,x)$。構造体については、各射影から組み直したものともとの項を同一視する（構造体 η）。
• 証明の無関係性：$P:\mathsf{Prop}$ のとき、$h_1,h_2:P$ はつねに $h_1\equiv h_2$。