ハッカーズチャンプルー

行ってきました。今回は、スポンサーちゃんといるので、なんと、

＊　ビーチパーティがただ

ぱちぱちぱちぱち。

長丁場でしたが、僕は、ゆっくり行ったので問題なしです。気持ちの良いビーチパーティでした。

　＊　＊　＊

Agdaでは、Hom(F(-),-)=Hom(-,U(-)) から随伴関手を導くってのに行き詰っていたんですが(逆はすぐにできた)…

あまりにわからないので、
<a href="http://en.wikipedia.org/wiki/Adjoint_functors">英語のWikipedia</a> を見たんですが

＊ Naaturality of Φ imply that

はぁ? そんなの聞いてませんが。で、ハッカーズチャンプルーを抜けだして、The Book (黄色のMacLaneのやつ)を
取ってきてみると、ご丁寧に可換図まで書いてある。つまり、この二日悩んでいた証明は…

＊　問題の仮定だった

らしいです(笑)。確かに、射の対応だけで、あんな複雑な式が出るわけない。その naturality は f = U(f*)○η で、 普遍問題の解そのものだったりするので、ちょっとあきれ気味です。随伴関手ってのは実は自然変換そのものだったのか。