恒等型

形成：$\Gamma\vdash a:A$ と $\Gamma\vdash b:A$ から $\Gamma\vdash\mathrm{Id}_A(a,b)\ \mathsf{type}$。$a=_Ab$ とも書く。

導入：$\Gamma\vdash a:A$ から $\Gamma\vdash\mathsf{refl}_a:\mathrm{Id}_A(a,a)$。

除去（J 規則）：型族 $\Gamma,x{:}A,y{:}A,p{:}\mathrm{Id}_A(x,y)\vdash C(x,y,p)\ \mathsf{type}$ と、$\Gamma,z{:}A\vdash d(z):C(z,z,\mathsf{refl}_z)$ が与えられたとき、$\Gamma\vdash a,b:A$ と $\Gamma\vdash q:\mathrm{Id}_A(a,b)$ に対して $\Gamma\vdash J(d,a,b,q):C(a,b,q)$。

計算：$J(d,a,a,\mathsf{refl}_a)\equiv d(a)$。