型宣言とカリー／ハワード対応、上江州アタッチメント

項tに対する型宣言 t:A を、「tはA（のひとつ）を具体的に構成する方法である」と読むと、構成的な感じがする。さらに、「tはAという命題の具体的な証明である」と読めば、証明論的な真偽解釈（に関する主張）だとも思える。

型環境（変数の型宣言のリスト）Δにより、Δ⇒t:A と書ける型判断は、「Δを仮定すれば、tによりAの証明が与えられる」というメタ論理的な主張の形式化と捉えられる。

一方、上江州計算（上江州式ラムダ計算）では、型環境Δは、上江州アタッチメントだと解釈できる。tの自由変数がVar(Δ)に含まれるなら、tの意味は上江州拡張C[Δ]のなかで解釈できる。Var(Δ)を x₁, ..., x_n とすると、t: x₁, ..., x_n ⇒A と書ける、これは x₁, ..., x_nの変域からAへの射（C[Δ]内）である。

ついでに書いておくと、上江州アタッチメント（添加）は、圏Cをいったん反射的グラフと考えて、頂点集合Vを直和で加え、Vから|C|への辺、逆向きの辺、恒等（同一）辺を加えて新しいグラフを作る。x:[x]→Aとx':A→[x]に関して、x;x' = [x], x';x = A という関係を入れて圏を生成する。自由生成と関係で商を作る手順となる。