対象aに対する恒等射は普通idaと書きますが、僕はしばしばidaも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です。
それがどうした
対象と射の区別がなくても圏を定義できることはわかりました。これは、圏が部分的演算を持つ代数系でもあることをアピールしますが、モノイド圏や高次圏の取り扱いに適用するのは困難です。やっぱり、「対象は点、射は矢印」という直感を大事にしたほうがいいみたいです。
じゃ何故こんな定式化をしてみたかって？ 単に「面白いかな」と思って。それと、僕は軟弱に半フォーマルでやったけど、完全にフォーマルにやってみるのは形式系（formal system）のいい練習問題でしょう。
*1:f↓g ⊃ (g↓h ⇔ (f;g)↓h)、g↓h ⊃ (f↓g ⇔ f↓(g;h)) と書くと少し短い。
