Σ 型（依存対型）

形成：$\Gamma\vdash A\ \mathsf{type}$ と $\Gamma,x{:}A\vdash B(x)\ \mathsf{type}$ から $\Gamma\vdash\Sigma_{(x:A)}B(x)\ \mathsf{type}$。

導入：$\Gamma\vdash a:A$ と $\Gamma\vdash b:B(a)$ から $\Gamma\vdash(a,b):\Sigma_{(x:A)}B(x)$。

除去：$\Gamma,z{:}\Sigma_{(x:A)}B(x)\vdash C(z)\ \mathsf{type}$、$\Gamma,x{:}A,y{:}B(x)\vdash c(x,y):C((x,y))$、$\Gamma\vdash p:\Sigma_{(x:A)}B(x)$ から $\Gamma\vdash\mathrm{split}(c,p):C(p)$。

計算：$\mathrm{split}(c,(a,b))\equiv c(a,b)$。