多圏とカット

多圏の定義には、結合であるカットが単一（単純）カット（single/simple cut）と複合カット（multicut）のバージョンがある。

multicutができるときは、f:Γ→Δ1,Θ,Δ2 g:Γ1,Θ,Γ2→Δに対して、cutは、f;_Θg:Γ1,Γ,Γ2 → Δ1,Δ,Δ2 となる。|Θ|≧1の条件が付くが、これを|Θ|=1のしたのがsinglecutの多圏。

多圏では、原子対象Aに対するidentityはあるが、列Γ=(A1, ..., An)に対するidentityはない。これが不便だが、定義に追加していいときもあるだろう。交替律f;_Xg;_Yh = f;_Yh;_Xgも定義に入っていたりいなかったり、、、（多圏は人気がない）

僕としては、基本命題集合（アルファベット）に順序があるとき（アルファベットがDAGのとき）、それを元にした推論ができればいい。A⇒Aだけでなくて、Γ⇒Γも公理に入れていいかもしれない。必要な推論規則は：

  （A≦B）

  ---------[preorder]

    A⇒B
  （|Γ|≧1)

  ----------[multi-id]

    Γ⇒Γ
  Γ⇒Δ  Φ⇒Ψ

  ----------------[monoidal product/sum]

   Γ,Φ⇒Δ,Ψ
  Γ⇒Δ1,Θ,Δ2  Γ1,Θ,Γ2⇒Δ（|Θ|≧1）

  ----------------------------------------[multicut composition]

       Γ1,Γ,Γ2⇒Δ1,Δ,Δ2 
    Γ⇒Δ （σ,τは対称作用）

  -----------------------------[symmetry]

  σΓ⇒τΔ
  Γ1,Θ,Γ2⇒Δ1,Θ,Δ2（|Θ|≧0）

  ---------------------------------[generalized trace]

  Γ1,Γ2⇒Δ1,Δ2