Kozen圏のスターとトレース

Kozen圏で、f:A+X→B+X のトレースは次のように表現できる。（ιは入射、πは射影、ブラケットは特に意味はなく単なる括弧）

• ι¹_A,B,X;[(π¹_A,B+X);f;(ι²_A,B+X)]^*;π²_A,B,X

なんか複雑だが、この形は絵算の“次元解析”で容易に得られる。

fの正方化R(f)を次のように定義する。

• R(f) = (π¹_A,B+X);f;(ι²_A,B+X)

これを何で「正方化」と呼ぶかというと、行列（二部グラフ）を使って書くとわかる。

ようするに、domainとcodomainを一致させたもの。トレースは、R(f)のスターを適当な入射／射影ではさんだ形をしている。

スターを使ったトレースはけっこう複雑なので、中間にConway不動点をはさんで扱ったほうがよさそうだ。