一日、家にいました

Ingressにはまってからは珍しい。皆勤賞とか子供の頃から縁がないものだったけど、一応、Sojourna Medal は取りましたけどね。

鼻水とくしゃみで、咳ではないので、それほど、きつくはないんだが、外に出ても社会の迷惑なだけだからなぁ。プロシンにティッシュを箱ごともっていったこともあったっけ。

久しぶりに Agdaも触りましたが、あんまり成果はなく。

＊　Limit から Equalizer を導く

という比較的簡単なお題なのだが(そして、それがFlyod Adjoint Functor Theoremに必要なわけなんだけど)、何か、うまくいきませんです。

Equalizerの要件(fe=geとか)を、自然変換の可換性で表してやればよいのだけど、

＊　関手の行き先が f : a->b

みたいなことができないらしい。関手の FMap の行き先の型は Hom A a b ではなくて、Hom A (FObj F x) (FObj F y) だからなぁ。a = (FObj F x) なのでつじつまは合ってるわけなんだけど、型がその場で一致してないとだめなので「値は同じなんだよ」と主張しても、Agda は許してくれないわけね。cast みたいなことをすれば逃げられるようではあるが。

まぁ、それでも、2(要素が2個しかない圏)とかの圏の書き方はなんとなくわかりました。Sum type との同型写像で場合分けしまくる感じ。そのままがんばればできそうな気もしたが、あまりに汚くなったので、諦めました。

きっとAgda的に画期的な解決方法があるんじゃないかな〜