フィルターの続き

元ネタは田中先生の公理論的集合論で、例題は

　　set of finite partial function from ω to 2

ですが、いろいろ苦労して書けたんだが、集合論でやるの面倒くさすぎる。Filterの定義もわかったので、

　　Agda でやる方が良いんじゃないか?

そもそも、強制法で使う filter は別にZFの中でやる必要はないわけで... で書いていったんですが、

　　なんか教科書と合わない

そもそもフィルターの定義がタイポしてるし。「x < y なんだが集合だと x ⊇ y 」とか書いてあって、

　　小さい方が拡大な

とか書いてるあるんですが、自分でばっちり間違えてるし。しかも、例題の方も! どうりでできないはずだ。ぷんぷん。

いや、たぶん。後の方の版ならなおってるんじゃないかな。

でも、がんばって集合論書いたけど、はっきり Agda で直接やる方が楽。L の集合は L → Set で良いらしい。

Power Set は (L → Set ) → Set だな。

この本、20年以上読んでるんだけど、今頃、気がつくのは問題ありだな。