Universal mapping

なんか、意外に早く終わった。って、朝の四時までやってれば解けるさみたいな。380行ぐらいでした。

Universal mapping から Adjoint Functor って圏論の初期の壁だと思うんだけど、

＊　やさしい部分と難しい部分が混在している

感じ。と言っても、数学者に言わせれば、まだやさしい方なんだろう。

Agda の証明は紙で書いて、textで書いて TeX で書いての延長だけど、Adjoint Functor から Universal mapping を出す部分で、解の一意性を出すのを忘れたいたのを見つけました。

逆方向の証明をする時に解の一意性を使うわけだけど、その定義を Universal mapping を表す record に記述すると、Adjoint から導出する時に、その部分も証明しろと言ってくる。

で、すごすご証明し始めると、解の存在の方では Uε○ηU = 1 しか使わなかったのに、一意性で、Adjointのもう一つの条件 εF○Fη = 1 を使うことになって、なるほどそういう対応かと理解しました。確かに片方しか使わないのは変だと思っていたんだよな。

C-C C-A とすると、? を自動的に埋めてくれるらしいんですが、

＊　まったく役に立ちません

Agda 潔くて良いよ。まるで証明の手書きツールのようです。

＊　＊　＊

近所のライトビルのお店、待夢は、あのビルにしては長い営業だったのですが、今週で締めてしまうらしい。なので、今週は三千円飲放題だそうです。特に思い入れがあるわけではありませんが、たまに寄ってました。