証明.
任意に豊穣 Freyd 圏 (;,J) をとる。
まず、 型の解釈を、
[A,B]=[A,B]
と定める。
記号が同じなので少し分かりづらいが、 左辺の括弧は Arrow に定められた型構築子で、 右辺の括弧は の射対象である。
それ以外の場合についてはラムダ計算の標準的な解釈の通りとする。
次に、 項の解釈を以下のように定める。
型割り当て Γ⊢M:A⇀B に対し、
arrM=❲ΓA⇀B[A,B]MJ❲
とする。
次に、 型割り当て Γ⊢F:[A,B] および Γ⊢G:[B,C] に対し、
F⋙G=❲Γ[A,B]×[B,C][A,C](F,G)c❲
とする。
なお、 c は の合成を定める射である。
最後に、 型割り当て Γ⊢F:[A,B] に対し、
firstF=❲Γ[A,B][A×C,B×C]F-⋉C❲
とする。
ここで、 J がバイノイダル構造を保つことから、 のバイノイダル演算は の直積で与えられることに注意すること。
これ以外の場合についてはラムダ計算の標準的な解釈の通りとする。
以上により、 Arrow の (;,J) における解釈が定まった。
以降、 定義 1.4 で定められた Arrow における 9 つの等式が、 の射としても成り立つことを順に示す。
等式 1:型割り当て Γ⊢F:[A,B] に対し、
arrid⋙F=F
を示す。
そのためには、 図式
Γ1×Γ1×[A,B](A⇀A)×[A,B][A,A]×[A,B][A,B]id×Fid×idJ×idcF
の外側が可換であることを示せば良い。
id:1→A⇀A は (-豊穣圏としての) の恒等射を与える射であるから、 J の関手性によって J∘id は の恒等射を与える射である。
したがって、 左下の三角形部分は可換である。
加えて、 右上の曲がった三角形部分は明らかに可換であるから、 全体も可換となって示したいことが示された。
等式 2, 3, 4:等式 2 は等式 1 と全く同様に証明できる。
等式 3 は の合成の結合性を保証する可換図式を用いれば良い。
等式 4 は J が合成を保つことを保証する可換図式を用いれば良い。
いずれの式も素直に示すことができるので、 ここでは証明の詳細は省略する。
等式 5:型割り当て Γ⊢M:A⇀B に対し、
first(arrM)=arr(M×id)
を示す。
そのためには、 図式
ΓA⇀B[A,B]A×C⇀B×C[A×C,B×C]M-×C-⋉CJJ
の全体が可換であることを示せば良いが、 この右側の長方形部分は J がバイノイダル構造を保つことから可換であるので、 示された。
等式 6:型割り当て Γ⊢F:[A,B] および Γ⊢M:C⇀D に対し、
firstF⋙arr(id×M)=arr(id×M)⋙firstF
を示す。
Γ[A,B]×(C⇀D)(C⇀D)×[A,B][A,B]×(B×C⇀B×D)[A,B]×[C,D][C,D]×[A,B](A×C⇀A×D)×[A,B][A,B]×[B×C,B×D][A×C,A×D]×[A,B][A×C,B×C]×[B×C,B×D][A×C,A×D]×[A×D,B×D][A×C,B×D](F,M)(M,F)id×JJ×idid×(B×-)(A×-)×idid×(B⋊-)(A⋊-)×idid×JJ×id(-⋉C)×idid×(-⋉D)cc
の外側が可換であることを示せば良い。
左右の三角形部分は J がバイノイダル構造を保つことから可換であり、 上の三角形部分は明らかに可換である。
また、 中央は J の中心性によって可換である。
以上により、 全体も可換となって示したいことが示された。
等式 7, 9:等式 7 は関手 -⋉D の関手性から従い、 等式 9 は のバイノイダル演算の結合性を保証する自然変換の自然性から従う。
いずれも用意なので、 証明は省略する。
等式 8:豊穣圏ではない普通の圏の場合でも少し工夫が必要で素直には示せないので、 豊穣圏の場合ではそれなりに大変である。
証明を書き下すと複雑な図式をいくつも書くことになるので、 ここでは省略する。
実際に手を動かして確かめてみよう!
以上で、 命題が示された。
これによって、 アローの形式化について、 型システム側で等式が成り立てば圏論側でも成り立つこと (健全性) が示された。
次回はこの逆を示す。