やっとわかった！デカルト圏

セリンガーが、「対角を持つ圏に、複製可能性と破棄可能性を入れたらデカルト圏だ」と言っていた。「そんなことはフォークロアだ」とも。が、僕はどうしていいものか方針が掴めなかった。

ランベックの定式化（演繹系としてのデカルト圏）をあいだにはさむと、結果は自明になる。次のような圏は同じものだ。

1. 有限離散完備な圏（有限完備ではない！）
2. 終対象と二項直積（binary product）を持つ圏
3. 任意のA, Bに対して、A, Bを足に持つスパン(Y, p1:Y→A, p2:Y→B)で、スパンによる射の分解Hom(X, C)→Hom(X, A)×Hom(X, B)が双射となるものが存在する。
4. ランベック流の定式化による(a la Lambek)デカルト圏
5. セリンガー流の定式化による(a la Selinger)デカルト圏

標準的定義は「終対象＋二項直積」だろう。これからランベック流は難しくないが、スパンによる分解を中継すると自然に出来る。ランベック流とセリンガー流の同値性は、ひたすら計算すればいい。

モノイド単位1が終対象であることも：

• f:A→1があるとき、f= f;id₁ = f;!₁ = !_A

として等式的に出る。

Hom(X, C)≒Hom(X, A)×Hom(X, B) とか、次の最も基本的事実が効いていることがよくわかった。

• f = g ⇔ f;πⁱ = g;πⁱ for all i's

直積のup to isoでの一意性も、これから出るし。