Bernstein 解決篇

可算版もかなり面白かったんですが、集合の方も割と迷走

二つの injection map

　　f : A → B
　　g : B → A

があるなら bijection があるというやつですが、まず、

　　A \ Img g から始めて、g・ f の閉包を取る

なんだが、ZFっぽくない。普通にやると、recursive record とか文句を言ってくる。

こういう時は、順序数方程式にしてやると良い。HODでやるときの定番だな。

　　　data gfImage :　(x : Ordinal) → Set n where
　　　　　a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage　x
　　　　　next-gf : {x : Ordinal} → (ix : IsImage a a gf x) → (gfiy : gfImage (IsImage.y ix) ) → gfImage　x

リスト構造みたいなものね。

これで、UC が定義てきたので、割と簡単に UC と UCのfの像f(UC)との Bijection 、そして、A \ UC と g⁻¹ の像との Bijection
が得られるわけですが、この場合分けの写像を作ろうとすると全然できない。

　　cca : (A ∋x) → C x ∨ ¬ C x
　　h : (A ∋ x) → cca ax → B
　　h ac (case1 cc) = h1 ac
　　h ac (case2 cc) = h2 ac

とかするんだが、h⁻¹ と組み合わせると、gfImage is not strongly positive とか言ってくる。

要するに、hの後に、さらに C x で場合分けするのが許されないらしい。

で、Aを分割してマーク付けるかとか起き抜けに考えてたんですが...

　　bi-∪　: {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D )　
　　　　　 → HODBijection (A ∪ C) (B ∪ D)

があるのに気がついた。

　 A ≡ UC ∪ A \ UC
　 B ≡ f(UC) ∪ B \ f(UC)

で書いたら、超簡単に。まぁ、そうだよな。h の場合分けは hの構成的な定義によってきまるわけじゃない。

非構成的(排中律)な場合分けだから、h から切り分けられない。そういう直観主義論理から見たら無理がある関数になってる。

可算の場合も、

　ℕ ⇆ A → B → C ⇆ ℕ

Bは

　 Aから指されててCにいる奴
　 指されてない奴

の二つにわかれてるので対応があって面白い。堪能しました。

https://shinji-kono.github.io/zf-in-agda/html/cardinal.html