Martin-Löf型理論の記法など

各型について4つの規則がある

形成規則(formation rule)

導入規則(introduction rule)

除去規則(elimination rule)

等号規則(equality rule)

命題を型として書くと以下の表な表記になる。

$ \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}

$ a =_A b : \mathrm{Id}(A a b)

参考