トレースを TrA,BX:C(A×X, B×X)→C(A, B)と書くことにして、Xを固定して、A, Bを動かす。すると、Trが、C(-×X, -×X)⇒C(-, -):Cop×C→Setという自然変換になっている。この事実を書き下すと、両側タイトニング公式となる。同じようにラムダ抽象 ΛA,BX:C(A×X, B)…