圏と集合と位相

平成最後の5年くらいははまりまくっていたわけですが、今日は、学生が本をスキャンするための裁断機を使いに来ていて、なに勉強するのと聞いたら

　　圏論だと

なるほど。本を見ると、随伴関手と米田関手、つまりrepresentable functor まで。そうだよね。でも、それだと、

　　なんのために圏論を学ぶのか

は良くわからないかも。一方で、

　　圏論勉強するには集合と位相が...


とか言っている学生もいて。いや、違います。

　　圏論勉強するには集合も位相も不要

位相空間論は微分方程式の解の表現から「実数って一体何」というところに突っ込んでいったところがあって、そこから、

実数は自然数全体の集合から作られるというカントルのアイデアがあったんだけど、

　　選択公理で迷走

ところが、ボレルとか測度論やってる人たちが結局、選択公理に突入。そして、ゲーデル、コーエン先生による

　　選択公理の独立性

つまり、集合から実数の性質には証明では決定できない自由度があるってのが判明していまいます。

その辺で、結局、なにが起きたのかを

　　数学を構築する記号論理を、対象(命題)と射(推論)

から構築するという一種の反省から出てきたのが圏論だと思う。そして、それは、

　　型付きλ計算

と関係がある。なので、プログラミング言語を作る時には圏論が一つの指針になる。そういうことなんじゃないかなと。

型なしλ計算に否定をいれると矛盾するとかを圏論の言葉で明確に記述できるのはわかりやすい。プログラミングの基礎としての圏論を
学ぶなら，その辺が一つの目標かも。もう一つは随伴関手と表裏一体のモナドかな。

所詮は道具だと思うので、さっさと通り過ぎるべきだとも思いますけど Agda 結構面白くて時間かけてます。

元号が変わってもだいたい同じことやっているんじゃないかな〜