型と論理

型と論理(Types and Logic)

$ \begin{array}{c|c|c|c} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) & 集合(\mathrm{Sets}) & ホモトピー \\ \hline A & 命題 & 集合 & 空間 \\ a: A & 証明 & 元 & 点 \\ B(x) & 述語 & 集合の族 & ファイブレーション \\ b(x) : B(x) & \mathrm{条件付き証明} & 元の族 & \mathrm{切断} \\ \bm{0, 1} & \bot , \top & \varnothing , \{ \varnothing \} & \varnothing, * \\ A + B & A \lor B & \mathrm{非交和} & 余直積 \\ A \times B & A \land B & 組の集合 & 積の空間 \\ A \to B & A \implies B & 関数の集合 & 関数空間 \\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) & \mathrm{直和} & \mathrm{全空間} \\ \prod_{(x:A)}B(x) & \forall_{x:A} B(x) & 積 & 切断の空間 \\ \mathrm{Id}_A & 等号\ = & \lbrace (x, x) | x \in A \rbrace & 道空間A^I \end{array}

ref: "Homotopy Type Theory Univalent Foundations of Mathematics" Table 1: Comparing points of view on type-thoretic operations (P11)

$ \begin{array}{c|c} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) \\ \hline A & 命題 \\ a: A & 証明 & \\ B(x) & 述語 \\ b(x) : B(x) & \mathrm{条件付き証明} \\ \bm{0} & \bot \\ \bm{1} & \top \\ A + B & A \lor B \\ A \times B & A \land B \\ A \to B & A \implies B\\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) \\ \prod_{(x:A)}B(x) & \forall_{x:A} B(x) \\ \mathrm{Id}_A & 等号\ = \end{array}

確認用

Q. 型と論理

参考

調査用

Wikipedia.icon

Wikipedia.icon