Generic Filter

なんか、やっと Agda で構成できたんだけど、

　　生成手順のしょうもないミスでした

三週間くらい無駄にしてしまった。いや、元にしてる公理的集合論のタイポがな...

林先生の本を見て、やっと気がついた。できないはずだよ。

いやでもフィルターのあたりは学部1年でやってたはずで、

　　簡単じゃん

とか思った記憶があるんだよな。その時はイデアルの双対とか知らなかったわけですが。

できたあとで、そんなのを思い出しました。

やっと Agda で集合論を扱えるようになってきた感じ。