Martin-Löfの直観主義型理論
直観主義的型理論(ちょっかんしゅぎてきかたりろん、Intuinistic type theory)
命題を型として書くと以下の表な表記になる。
$ \begin{array}{rcl}\bot & = & \varnothing \\ \top & = & 1 \\ A \lor B & = & A + B \\ A \land B & = & A \times B \\ A \supset B & = & A → B \\ \exist x:A.B & = & \Sigma x: A.B \\ \forall A.B & = & \Pi X:A.B \end{array}
$ \Sigma : 直和(disjoint sum) 関連