Π 型（依存関数型）

定義 3.1（「依存型理論」§3）

\frac{\Gamma\vdash A\ \mathsf{type}\quad \Gamma,x{:}A\vdash B(x)\ \mathsf{type}}{\Gamma\vdash\Pi_{(x:A)}B(x)\ \mathsf{type}}\ (\text{形成})\qquad \frac{\Gamma,x{:}A\vdash b(x):B(x)}{\Gamma\vdash\lambda x.b(x):\Pi_{(x:A)}B(x)}\ (\text{導入})

\frac{\Gamma\vdash f:\Pi_{(x:A)}B(x)\quad\Gamma\vdash a:A}{\Gamma\vdash f\,a:B(a)}\ (\text{除去})\qquad (\lambda x.b(x))\,a\equiv b(a)\ (\text{計算}),\qquad f\equiv\lambda x.f\,x\ (\eta)

$B$ が $x$ に依存しないとき $\Pi_{(x:A)}B$ を $A\to B$ と書く。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

証明で明示的に参照している定理は、まだありません。