圏論

入門の復習をやっているわけですが、だいたい片付いた気もする。

Introduction to higher order categorical logic
http://books.google.co.jp/books/about/Introduction_to_Higher_Order_Categorical.html?id=6PY_emBeGjUC&redir_esc=y

を使っているんですが、(いや、他の本も)、Section 0 が圏論の復習だけど「知ってる人は読むな」、そうでない人も教科書の補助ぐらいにしとけとか書いてある。でも、短くて、logic に必要な部分が書いてあるので、これを使ってます。

この本は意図的に選択公理とかを避けてる。それはありだと思うな。去年、結構、勉強したけど、選択公理は「集合ってのは順々に定義されていることにしようよ」ってぐらいなものなので、あんまりこだわるものではないと思う。Agda では、Set 0, Set 1, Set 2 ... とあって、Set 0 全体を扱う変数は Set 1 にするみたいな感じ。それで良いよね。

数学は結局は「検算」の山であって、自分で計算してみるしかない。手を動かして理解する感じ。なので、板書が一概にダメだとは思わない。でも、書き写すのとは少し違うかも。

＊　本の余白に書き込み
＊　式を vi で
＊　LaTeX で清書

あたりで、それなりにバグが見つかったり、理解が深まったり。できれば、Aggda で検算したいところだが、

＊　めんどくさいんだよ

超めんどくさいです。関数の結合 g f で、

__ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
(f : {x : A}(y : B x) -> C x y)
(g : (x : A) -> B x) (x : A) -> C x (g x)
(f g) x = f (g x)

は、ないっでしょ? わざとは思うけどさ。値域を制限すれば、もっと簡単になるとは思うんだけど。

でも、形式的証明は、そういうめんどくさいもの。それを確認した感じかな。圏論を今年、どこまでやるかは謎だけど、ここまででも結構面白かったです。