これでオシマイにします。シリーズ記事をすべてリストしたい場合は、「モノイド閉圏の事例：」で検索すればいいでしょう。 シリーズ記事を検索 記事の推敲・リライト、再編成などは（当初は多少やるつもりでいたが）やる気はありません。明らかな間違い（誤…

ボックス積 (-□-) を Box:SG×SG→SG とも書く。ボックス積が双関手性を持つとは、直積圏からの関手であることだから： Box( (f, f');(g, g') ) = Box( (f, f') );Box( (g, g') ) （結合の保存） Box( (A, B)^ ) = Box( (A, B) )^ （単位の保存） 中置演算子形…

(ΦX,A,Y(f)□A^);ev = f ΦX,A,Y(f) = Φ(f) = F と置いて、(ΦX,A,Y(f)□A^) = F□A^ を計算する。 F□A^ : X□A→hom(A, Y)□A = [ λ0(x, a)∈A□A.( (F(x), a) ∈hom(A, Y)□A ) ALSO λ1(x→x', a)∈A□A.( (F(x→x'), a) ∈hom(A, Y)□A ) OR λ1(x, a→a')∈A□A.( (F(x), a→a')…

反カリー化を定義して、カリー化の逆写像であることを計算で直接的に示してみる。念のために、カリー化の定義を再掲： ΦA,B,C : Hom(A□B, C)→Hom(A, hom(B, C)) := λf∈Hom(A□B, C).( [ λ0a∈A.( [λ0b∈B.( f(a, b) ∈C) ALSO λ1b→b'∈B.( f(a, b→b') ∈C) ] ∈hom(…

ここまで計算してきて感じたこと： 図（ストリング図）のワイヤーにラベルがないのは分かりにくい。横着せずにワイヤーにラベル（対象の名前）を書いたほうがいい。悪い例は↓ 写像ブロックとデータブロックを区別して書く必要はないかも。「写像ブロック←→デ…

前の記事の続き。後でひとつの記事にまとめるかも。 真っすぐなスライディング ΦX,A,Y'( f;q ) = ΦX,A,Y(f);hom(A, q) : X→hom(A,Y') 左辺： Φ( f;q ) : X→hom(A,Y') = [ λ0x∈X.( [ λ0a∈A.( q(f(x, a)) ∈Y') ALSO λ1a→a'∈A.( q(f(x, a→a')) ∈Y') ] ∈Hom(X, Y…