昨日の「弱いラムダ計算の根拠とか」にて：
Λ-1:C([A, B], [A, B])→C(A×B, B) という随伴を与える同型が自然変換（の成分）であることから、自然性を（適当なセッティングで）露骨に書き下すと、先の等式が得られる。…中略… 興味あるかたは、適切な練習問題ですからやってみてください。
こんな感じでしょう→落書きみたいだが：
C(-×A, -)とC(-, [A, -])が集合圏への反変／共変・双関手であることと、Λ-1がこれらの双関手のあいだの可逆な自然変換＝自然同値であることから、(Λ(f)×idA);ev = f という関係を導く手順。
[追記]アレッ、間違っているわ(苦笑)。
上の「一般的に」のほうで、(v×A);Λ-1(k) = Λ-1(v;k;[A, w]) で左辺にwが抜けている。つまり、(v×A);Λ-1(k);w = Λ-1(v;k;[A, w])。
あと、念のために言っておけば、しばしばidAを単にAと書いてます。
一番下のほうで、w = idA のつもりで、w = ＝ とワケワカラン書きかたしているけど、まー、そういうことです（わかるよね）。[/追記]
