この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した. 写像の定義を _⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる. x ∈ A を像の方に押し込めて _⟶…