トレースとラムダが部分的に自然変換であること

トレースを Tr_A,B^X:C(A×X, B×X)→C(A, B)と書くことにして、Xを固定して、A, Bを動かす。すると、Trが、C(-×X, -×X)⇒C(-, -):C^op×C→Setという自然変換になっている。この事実を書き下すと、両側タイトニング公式となる。

同じようにラムダ抽象 Λ_A,B^X:C(A×X, B)→C(A, B^X)は、C(-×X, -)⇒C(-, -^X):C^op×C→Setの自然同型になっている。この事実を書き下すと、デカルト閉圏の公式はすべて出る。