東京 short visit

既に帰ってきました。 母も歳なので、たまに長くいるよりも短くして、頻繁に行った方が良いかと思って。

でも、週末だけってのは「酒飲んで終わってしまう」なぁ...

　- * - * - * -

ついでに Agda も少しいじってました。初期の頃にやった equalizer と product から limit を作るという課題。Sets の Limit をやって、やっぱり少しおかしいことに気が付きました。

少し自力でやってみたがうまくいかず、Categories for Working Mathematician を見直すわけですが、

　　お前、前に読んだ時に何を読んでいたんだ?!

ってくらいに違うことが書いてあって。まぁ、でも、大筋は合ってたんだけど。一部の等式を、仮定を強力にして安易な証明ですませたらしい。だめだな。いや、おかしいとは思ったんだけど。Sets Completeness の時に使えなくて気がついた。

元の証明に Product 二つ足して東京にいる間にできたみたいです。

あと何やるのかは、まぁ、やっても良いものはたくさんあるが、Kan Extension とか、Cartesian Closed Category の一連とか。ZFC やってみるのも良いかな。

　- * - * - * -

なんか、xterm が勝手に focus 外れるんだよな。もう使ってる人はほとんどいないと思われるので誰にも聞けないところがつらい。