Agda で書く Generic Filter の続き

いや、なんか、かなり難航してて。

　　順序構造なんだけど、それを集合論のモデルの集合Mのなかに作る必要がある

あぁ、じゃぁ、部分集合の⊂でいいじゃんというわけで、順調だったんですが...

方向が二通りある。そして、大きい方小さい方両方に開いている必要がある。さらに、

　　書き下す時に方向がいりじまってて...

結局、Power P ⊇ L な L でやれば良いってわかったのが、今週になってから。

まぁ、骨子は2年前に書いたもので良かったんですが。で、それは片付いた。めでたい。

なんですが、

　　それを超フィルターに拡大する必要があって
　　すると、¬ G ∈ M が言える
　　それには Zorn の補題が必要

らしいので、まだ少し距離があるみたい。

Zorn の補題は、集合上の二分法みたいな話だというのを発見しました。まだ書いてないけど。

でも一時期みたいに

　　変更点が数十あるのか思いつかない
　　一箇所書くのに午前中潰す

みたいなのはなくなったみたい。でも、少しお休みするべきかもな。来週はコンパイラ読み会だし。