Agda の圏論の証明

まぁ、やってるのが圏論だってのが特殊ではあるんですけどね。

　極めてパズル的

帰納法とかほとんど出てこない。なので、

　証明の穴に適当に推論を当てはめる

ということになりがち。そして、それで、結構通る。それで終わってしまうのが普通。

もともと圏論が General Abstract Nonsense だからってのもあるんだろうけど。

Monad も面白いんですが、一生懸命証明したものが、

　メタ計算も関数の結合法則に従う

というだけだと、ちょっとさびしいんじゃないかなぁ。

でも、一方で、

　プログラムはちゃんと型的に穴が埋まっていれば動くんじゃないの?

とも思います。

数学や物理の理論を理解するには、数式や論理式の裏にある

　モデル

を理解することだと思う。圏論はモデルと論理式が一体になっている特殊な例なのかな。

　視覚化できるモデルとかたいしたことない

とも思うのですが、視覚化には「気づき」みたいなところがあるからな。