圏論番外：横着者のための型なし圏論（ただしフォーマル） - 檜山正幸のキマイラ飼育記 (はてなBlog)

対象aに対する恒等射は普通id_aと書きますが、僕はしばしばid_aもaと書いてしまいます。これは単に、横着者の略記に過ぎないのですが、合理化しようと思えばできなくもない。で、やってみる。ただし、こういう定式化が特に良いというわけではないです。

まえおき

圏論をフォーマルに展開するときは、通常、等式的な一階述語論理を枠組みに使います。このとき、ソート（型）を2つ準備します。つまり、対象を表すつもりのObjと射を表すつもりのMorです。例えば基本的な関数記号の“型”（プロファイル）は：



 dom:Mor→Obj

 cod:Mor→Obj

 id:Obj→Mor

 comp:Mor, Mor→Mor

この標準的な方法をやめて、ソート（型）なしでやってみます。つまり、対象と射の区別はしません。すべてが射だといってもいいでしょう。二項関数記号compと二項述語記号composableを使いますが、comp(f, g)をf;g、composable(f, g)をf↓gで略記します。f↓g のインフォーマルな意味は「fとgはこの順で結合可能、つまりf;gをちゃんと作れる」ことです。

圏を定義するには、「『;』が、結合的（associative）かつ単位的（unital）な部分演算だよ」と述べればいいのですね。以下、そういう意味の主張を半フォーマルに書き下してみます。含意記号は「⊃」を使います（記号の選択に特に意味はない）。

結合律

結合可能性に関して、次を要請します。

[C1] ∀f.∀g.∀h.[f↓g ∧ g↓h ⊃ (f;g)↓h]
[C2] ∀f.∀g.∀h.[f↓g ∧ g↓h ⊃ f↓(g;h)]
[C3] ∀f.∀g.∀h.[f↓g ∧ (f;g)↓h ⊃ g↓h]
[C4] ∀f.∀g.∀h.[g↓h ∧ f↓(g;h) ⊃ f↓g]

なんかゴチャゴチャした印象*1ですが、結合律を述べるために（たぶん）必要です。

さて、問題の結合律：

[A] ∀f.∀g.∀h.[f↓g ∧ g↓h ⊃ (f;g);h = f;(g;h)]

[A]の前提部分（⊃の左側）から、[C1], [C2]を考慮すれば、f↓(g;h) と (f;g)↓h は出ます。これにより、[A]の結合律等式に出現する4つの「;」が全て有効であることが保証されます。

単位律

「aが左単位である」という内容を次のように定義します。

left_unit(a) ≡ ∀f.[a↓f ⊃ a;f = f]

同様に右単位：

right_unit(a) ≡ ∀f.[f↓a ⊃ f;a = f]

左単位かつ右単位なら単位：

unit(a) ≡ left_unit(a) ∧ right_unit(a)

これで準備できたので、単位律を以下に：

[U1] ∀f.∃a.[a↓f ∧ unit(a)]
[U2] ∀f.∃b.[f↓b ∧ unit(b)]

単位の一意性

[U1]により、fに対してa↓fとなる単位aの存在は保証されますが、そんなaがイッパイあるかもしれません。仮にaとa'が、a↓f、a'↓f となる単位だとして、a = a' を示しましょう。

aとa'がfに対する左単位となっているので、a↓(a';f)（a';f = f だから、a↓f と同じこと）と a'↓f（最初から仮定されている）がいえます。[C4]を使うと、a↓a' が導けます。同様に、a'↓(a;f) と a↓f から[C3]を使って a'↓a も導けます。

aもa'も単位（右単位かつ左単位）だったので、a;a' = a（a'の右単位性）、a;a' = a'（aの左単位性）、したがって a = a'。

これで結局、fに対してa↓fとなる単位aは存在し、しかも一意的（ただ一つ）だとわかりました。同様に、fに対してf↓bとなる単位bも一意的です。一般的に、「任意のxに対して、P(x, y)であるyは一意的に存在する」が示せれば、Pに対応する関数記号Fを導入して P(x, y) を y = F(x) に書き換えてもいいので、「fに対してa↓fとなる単位a」をdom(f)と書きます。同様に、「fに対してf↓bとなる単位b」をcod(f)と書きます。

以上のことを完全にフォーマルに書き下すことができます。つまり、最初に提示したcomp（;と略記）しか関数記号を持たない体系と、dom, codを持っている体系は同値です。dom, codを使って書いた単位律は、∀f.unit(dom(f)) と ∀f.unit(cod(f)) になります。これは、dom, codの値が単位であることを意味します。また、aが単位なら dom(a) = a, cod(a) = a もいえます。

結合可能性

型なし圏論の中でdom, codが再現できました。結合可能性f↓gをdom, codで書いてみます。予想される形は、f↓g ⇔ cod(f) = dom(g) です。dom, cod を消去して少し変形すれば、次の形です。

[T1] f↓g ∧ f↓b ∧ unit(b) ∧ c↓g ∧ unit(c) ⊃ b = c
[T2] f↓b ∧ unit(b) ∧ c↓g ∧ unit(c) ∧ b = c ⊃ f↓g

まず、[T1]の前提部分から b↓c を示す略式の証明図を描くと：



   f↓g (仮定)

 -----------[g = c;g なので]

   f↓(c;g)    c↓g (仮定)

 --------------------------[C4]

         f↓c

    --------------[f = f;b なので]

        (f;b)↓c     f↓b (仮定)

       --------------------------[C3]

                b↓c

b↓c がわかれば、b;c = c（bの右単位性）、b;c = b（cの左単位制）、よって b = c。これで[T1]が示せました。

[T2]に関しては、b = c から仮定は f↓b ∧ b↓g ∧ unit(b) だとしてかまいません。f↓b ∧ b↓g に[C1]を使えば (f;b)↓g が言えますが、f;b = f なので f↓g、これでもうOKです。