コンパクトシーケントと従順多圏とモノイド圏

まず、コンパクトシーケントとは、コンパクト論理のシーケントで、左辺と右辺のカンマの解釈が同じもの。古典論理のシーケントとは違う。次のような規則を使う。

  Γ ⇒ Δ,Δ'   Δ',Ψ ⇒ Φ

  ----------------------------[右Cut]

    Γ,Ψ ⇒ Δ,Φ

  Γ ⇒ Δ',Δ   Ψ,Δ' ⇒ Φ

  ----------------------------[左Cut]

    Ψ,Γ ⇒ Φ,Δ
 

  Γ,A ⇒ B

  ---------------[右o--導入]

  Γ ⇒ A o-- B
  A, Γ ⇒ B

  ---------------[右--o導入]

  Γ ⇒ A --o B
  A, B ⇒ Δ

  -----------[左∧導入]

  A∧B ⇒ Δ
  Γ ⇒ A, B

  -----------[右∧導入]

  Γ ⇒ A∧B

他にも規則はあるが、とりあえず先に進む。

このシーケント計算のモデルとして、扱いやすい多圏を導入する。従順多圏と呼ぶことにする。Oが基本対象の集合、O^* がOから作った列の集合として、O^*の元は Γ, Δなどで書く。Oの元はA, Bなど。圏と同様に、dom, cod, idを持つ。そして、右cutと左cutが2つの結合を与える。並置が標準的なモノイド積となる。

従順多圏には標準的に圏が含まれる。長さ1の多対象をdom, codにする多射だけを考えると、これは圏となる。これを従順多圏のコア圏と呼ぶことにする。コア圏に、対称とは限らないモノイド積と2つの指数が与えられているとき、従順閉多圏と呼ぶことにする。コア圏は右自立かつ左自立なので自立圏となる。

さらに、コア圏に、A^** = A、(A×B)^* = B^*×A^*、(A o-- B)^* = (B^* --o A^*)、(A --o B)^* = (B^* o-- B^*) を満たすようなスターオペレータがあるとすると面白い。このスターオペレータに関して、AとA^*を結ぶ τ_A : A→A^* があって、τ_A;τ_A* = A となってほしい。τはハーフツイスト射になる。

この状況で示せる典型的な公式として、軸反転（pivoting）公式がある。X_A,Bを対称ブレイディング（クロス）、τをハーフツイスト、LΛとRΛをそれぞれ左抽象、右抽象とすると：

• LΛ(X_A,B;f);τ = RΛ(f)

が示せる、つうか示せるように定式化すべき。