昨日は飲みすぎだった...

まぁ、奥様がご機嫌だったので良かったです。

Agda は、

f
--->
・ ・
--->
g

というのをやっているだけなのだけど、これだとf の逆向きの射はは存在しないわけだよね。適当に辻褄合わせの射を入れれば良いというアプローチだったんですが、圏の結合則とかはともかく、Functor の分配則がだめで、この方針ではダメらしい。

なので、そもそも射がないという性質を持つ圏を作らないとダメなんだよなということに気がついたのが昨日の午後。Agda の Maybe と格闘してました。

＊　Maybe と整合性のある等式公理

があるだというのがわかりました。この辺も未定値⊥を持つプログラム理論とかで勉強していたはずなんですけどね。簡単だよね、ふんふん、とかですませていたが、

＊　自分で等式の反射律とか推移律とかを書くとなると面倒

それがData.Maybeに既に書いてある。やっぱりライブラリは偉大だ。

とはいえ、まだ、終わってないです。この証明「いけそうだ」「だめだ」を何回繰り返したことか。証明自体は簡単なんだがなぁ。

とかやっていて、遅刻しそうになってあわてて家を出たら、奥様が上がってくるところで、結局、そこからさらに遅れて出ましたが、車でいくことになったので、まぁ、なんとか間に合ったみたいです。