ZF集合論 on Agda

順序数を作って、OD (Ordinal Definable Set)を作って、集合論の公理を満たすところまではできたんですが...

どうも全部の集合が順序数になってしまう。record { def = λ x → x o< y } という形が順序数なんですが、

どの集合も、どれかの順序数に一致してしまうらしい。教科書には OD は順序数と順序同型だと書いてはあるんですが、これだと、

　すべての空でない集合がΦ(空集合)を含むことになる ( 0 o< x だから)

いくつかの仮定を削ると避けられるようですけど、結構、証明できない公理が... でも、うっかり仮定を増やすと空集合を含んでしまう。

まぁ、ここまでかな。