たけをさんとピンポン状態になってますが、週末にちょっと計算してみたら、外の圏の構造から論理半環（「個体と世界の関係：圏から論理半環を絞り出す」を参照）を絞り出すことは、ほぼ目論見通りにいきそうです。とはいえ、いくつか疑問は残っています。その状況を以下に記します。
まず、また記法を変えて、テンソル積×の単位対象をI（大文字アイ）にします -- 1（太字のイチ）だと終対象の印象が強いので。Cの対象Aに対して、λAとρAは、モノイド圏の左単位律同型と右単位律同型だとします。
- λA:I×A→A
- ρA:A×I→A
δAは A→A×A という乗法的対角、εA:A→I はδとペアになる余単位だとします。プログラミングとの対応だと、δはデータのクローン、εはデータの破棄です。
さて、論理半環の乗法構造、つまり論理積を考える上で、テンソル積×とその対角δ（あとεも）は非常に重要です。つうか、論理積はテンソル積と対角に由来するので、論理積はテンソル積によって完全に支配されます。それに対して、テンソル積が双積に対して分配的であることは、思ったほど重要じゃないかも知れません。いや、まだハッキリしないけど。
外の圏Cに関する条件として、次のような等式（同型じゃなくてホントの等式）を仮定したくなります。
- ρI = λI
- δI = λI-1
- εI = idI
どれも自明のように思えるのですが、その根拠を突き詰めると、なんだか不安になってきます。いきなり仮定していいもんでしょうか？ 他の、より確実な事実から出るもんでしょうか？ 公理なんだか定理なんだかよくワカラナイですわ。
ともかくも、上に挙げた等式群を仮定すれば、論理積の可換性とベキ等性は出てきます。これはなんか不思議な感じがする。間違いじゃないと思うのだけど、キツネにつままれたような議論なんですよね。テンソル積の対称性も不要で、それでも可換性が出てくる。ウーム、不思議だ。この推論のスジは、たぶん後で公開します。
論理半環の条件で、「a∧b = a ⇔ a∨b = b」は欲しいのですけど、これがワカラナイ。これは順序に関する条件だけど、圏論的な対応物がワカラナイのですよ。外の圏がどんな性質を持ったら、この条件が出てくるんでしょうね？ 束論とかだと、この条件は天下りの公理なので、その起源を詮索することはないしね。∧と∨の相互の関係なので、双積とテンソル積のあいだの法則？ 実は「a∧b = a ⇔ a∨b = b」なんて要らない、てなオチもあるのかな？
まー、そんな感じでして、「a∧b = a ⇔ a∨b = b」はサッパリわからないけど、「足し算も掛け算も可換ベキ等な半環」は作れそうです。
