余ElgotオペレータとConwayオペレータ

トレースのある余デカルト圏では、Elgotオペレータは、f:X→A+Xに対して Tr[(X+f);(σ+X)(A+∇)]:X→A となる。双対的に余Elgotオペレータは、Tr[(A×Δ);(σ×X);(X×f)]:A→X である。

ところが、余Elgotオペレータを変形すると、Tr(f;Δ)となり、Conway不動点オペレータとなる。つまり、トレース付きデカルト圏では「余Elgotオペレータ = Conwayオペレータ」となる。双対的に、トレース付き余デカルト圏では「Elgotオペレータ = 余Conwayオペレータ」。