圏論は2013から

なんか灘高の圏論入門みたいなのを見かけて。そういえば途中だったなで始めたみたい。

最初に触れたのは吉田研の出口さん関係の勉強会だったはずです。層圏トポスで米田関手までだったかな。

最初は本の余白(と言ってもA4にコピーしたので割と広い)でやってたんですが、全然足りない。

今でもそうですが twitter で書きながらなので教えてくれる人とかいて面白い。

で、TeXのtikzとかでやってたんですが、そういえば証明支援系あるよなで、Coq から Agda という流れ。

最近は結構見かける感じ。証明の視認性はCoqよりはAgdaが良いかも。論文とか整理されたAgdaのsiteとか。

ただ、Topos までやってるのは見かけないかな。特に Sets との関連はかなり面倒なのだから。

圏論は集合論の直観で展開している本が多くて、竹内先生のもそうですが、Lambek/Scott は圏論のみにしたいらしい。

けど、それでも一部集合論が出てくる感じ。その辺も寄り道したのでだいぶわかってきたかな。

　2013 クライスリ圏
2017 随伴関手定理
2018 CCC
2019 ZF
2020 Galois
2021 Topos

学生時代にこういう読み方ができると良かったなとも思うけど、今の復習も楽しい。