集合論の続き

OS研究会の時にうっかり手をつけてしまって。もうずいぶん長いんですけどね。

今回のお題は、sup の公理を落として、置換公理を外す。集合の上限の仮定は最小限に。

ところが、そこで直積の定義に問題があることに気がついてなおしたんだが、

　　これで射影が簡単になるんじゃないか?

と気がついて、あさっての方向に。確かにかなり簡単になって、フィルターの直積の射影とか直積の交換とか簡単に。

と思ったんだが、

　　P x Q 上のフィルターを Q x P に変換して射影を取って使おうとすると Agda が無限ループに

おっとと。で、結局、P側とQ側は二つコピペで書くことに。まぁ、簡単になったからいいかな。

いろいろ、寄り道したが、とりあえず、そっちは諦め。