「トレース付き対称モノイド圏とはこんなモノ」で、長谷川真人さんの "Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi (1997)" http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.52.31 からコピーした絵を載せました。
法則（公理）はバニッシング、タイトニング、スライディング、スーパーポージング、ヤンキングの5つ、バニッシングとタイトニングが2つに分かれているので、それも勘定すると７つの法則です。
上記1997年論文よりもっと新しい論文 "On Traced Monoidal Closed Categories", MASAHITO HASEGAWA, 28 November 2007 だと法則が減っています*1。
バニッシングとスライディングがなくなって、代わりにエクスチェンジが入っています。セリンガーもこのスタイルを採用してました。エクスチェンジは、対称（またはブレイド）をスライディングするのと同じなので、以前の公理から導出できます。
問題は、新しい公理系からバニッシングとスライディングが導出できるかです。もちろん、できるはずなんですが、僕はできませんでした。エクスチェンジからバニッシングとスライディングが出ることは、アラン・ジェフリイ（Alan Jeffrey）が発見したようです（たぶん、確証はない）。
熱心に探したわけじゃないですが、エクスチェンジからバニッシングとスライディングを出す計算が見つかりません。10年くらいは7つの公理でやっていたので、それを減らすのはなんかトリッキーな発想が必要なんでしょうか？
[追記]
id:oto-oto-otoさんのつぶやきから、引用したまさにその論文 "On Traced Monoidal Closed Categories" の付録に、スライディングとバニッシングの導出法が出ていることを知りました（Appendix A. Derivation of Sliding and Vanishing）。
ヤンキングでわざと輪っこを作って引き伸ばして細工するのか。これは思いつかん。難しいなー。
[/追記]
