トレース分解定理：詳細

定理の記述

Cがトレース付きデカルト圏として、Cにおけるf:A×X→B×YのトレースTr(f)は、次のように分解した形で書ける。

fの第一射影f¹をf_out（出力関数）、fの第二射影f²をf_tran（遷移関数）とすると、Tr(f)は、f_tranの不動点であるf_loopとf_outの和（に近い形）で書ける。

証明

fを、第一射影f_out = o と第二射影f_tran = tに分けて、多少変形しておく。

この状態でトレースを取って、目的の形に変形する。

2番目から3番目への変形を詳細に述べれば：

1. 対角を、スライディングで移動する。
2. X×Xの（リボン状）ループをバニッシングで分割して、内側をタイトニングで縮める。
3. 点線で囲った箱を巻いている部分をほどく。→回ったワイヤーをほどく - 檜山正幸のキマイラ飼育記 メモ編