いたずら書きを清書

圏論の本に書き散らした証明(随伴関手とUniversal Mappingの対応)を text に書きなおしたんだけど、

＊　そもそも思い出せない
＊　間違っているような気がする

ので、結局、もう一度証明しているような感じ。で、再度証明が終わると、

＊　確かに、あの時の証明は正しかった

ってなんだよぉぉぉぉ。ASCII art な可換図で320行ぐらいなので、そんなに長くはないです。元の本では3行だがな。

Saundaer Mc Lane の本がやっぱり丁寧に書いてあることを再確認しました。そこでは4ページぐらい使っているので。

これを、Agda で書きなおせば良いんですが、これを、うちの学生にやらせるのはちょっとなぁ。

さて、終わったので飲みに行くか。