トレースの表記を少し拡張
f:A1+X+A2→B1+X+B2に対して、TrXA1,A2;B1,B2(f)を、TrXA1+A2,B1+B2(σA2,X;f;σX,B2)とすると、クロスが減るので表記が単純になることがある。
f;A→B+X, g:X+C→Dのとき、f;Xg:A+C→B+Dを、(f + C);(B + g)と定義すると、これも表記が単純化することがある。
シークエントなら:
A1, X, A2 ⇒ B1, X, B2
---------------------
A1, A2 ⇒ B1, B2A ⇒ B, X X, C ⇒ D
----------------------
A, C ⇒ B, D
やっぱり、トレース付き多圏とかコンパクト閉多圏とかを考える必然性はあるな。