もう少し集合論

Agda に safe というのがあるのを発見して。postulate で仮定したり、Heterogenious Eqaulity や
Functional Extensinality を使わないってやつらしい

関数外延性はかけ算の議論でも出てきて、関数の実装は一つで ≡ で扱えるってのなんですが、

　　確かに良くないかも

その代わり、関数は入力と出力の組が等しいというのを関係として使えばよいわけね

集合も要素が同じなら、集合として同じなんですが、それは、そういう関係なんだよな

順序数なアドレスは、集合としては一つ。それでつじつま合うと。10月ぐらいに思いついて放っておいたんですが

　　年末年始プログラミングにちょうど良いか

で、ZFの公理まではできました。

去年はトポロジーやってたみたいね。その辺も修正はいるけど、できるはず。ただ量多いのがな

いろいろすっきりしてよい。safe 自体が主導原理になる感じ