判断

文脈 $\Gamma=x_1{:}A_1,\ldots,x_n{:}A_n$（各 $A_i$ は前の変数に依存してよい）のもとで、次の 4 種類の判断を考える。

• $\Gamma\vdash A\ \mathsf{type}$：$A$ は型である。
• $\Gamma\vdash a:A$：$a$ は型 $A$ の項である。
• $\Gamma\vdash A\equiv B$：型 $A$ と $B$ は定義的に等しい。
• $\Gamma\vdash a\equiv b:A$：項 $a$ と $b$ は型 $A$ の項として定義的に等しい。

定義的等しさは、定義の展開と計算（β 簡約など）で互いに移り合うことを表す。$\Gamma\vdash a:A$ かつ $\Gamma\vdash A\equiv B$ なら $\Gamma\vdash a:B$ とする（変換規則）。