層圏トポス

大学で読み会したのが79年くらいなんじゃないかなぁ。初版が出たばかり。この時は買ってないので図書館で借りたか...

その後、買ったと信じていたんですが、実家では発掘できず。結局、古書で買いました。

当時でも米田関手までは読んだはずです。この本は Hihger order categorical logic のかなりの部分をcoverしているのだと再発見しました。

直観主義論理の完全性まで入ってるし。ただ、証明は「明らか」とかが多くてなぁ。嘘つき... MacLane がその点は細かく書いてあるので素晴らしいです。

3刷ですが、後書きがかなり追加されてる。これは1.3版でしょうね。Bool代数とTopsの関係とか半ページでさらっと追加してあったり。

さすがに、ここ数年圏論やりまくったので、ふんふんと言う感じで読めました。いや、まだToposに手を付けてないんだけど。

Topos での coequalizer の証明はToposでは難しいが直観主義論理でやると簡単と書いてあって、実際そこに来ると「それはなんでもない」せ、先生...

圏の本を見るとHom Setが集合(small)かどうかがしつこく書いてあったりするんですが、さすが竹内先生で「そのあたりはこだわらないのが良い」とばっさり。

ちょっと前に少し locally smallって何って話を書いたけど、その辺の話ですね。Limitをfiniteで片付けてるのはそのせいだな。正しい判断だと思います。

今なら、圏論と直観主義論理を平行して読むのが良いんじゃないかな。でも、

　　証明の省略がひどい

のはどうしようもない。この本だけでは絶対無理。そこを Agda で補いながらか?

古書だけど、レシートが挟まってて。名古屋の丸善だ。なんと一緒に買った本がISBNからわかる。メタマス、オメガの冒険。不完全性定理とかの話の本でした。