少し追記。 型コンテキストを型判断と呼ぶ用語法は採用しない。 型シーケント $`\Gamma \vdash M:\sigma`$ を型判断〈typing judgement〉と呼ぶのは許容しよう。 型判断の意味はセマンティック・デカルト閉圏の射になる。特に集合圏では単なる写像。型コンテ…