Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1095:08b6aa6870d9
OD clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 22 Dec 2022 15:10:31 +0900 |
| parents | 63c1167b2343 |
| children | 55ab5de1ae02 |
| files | src/OD.agda src/cardinal.agda src/zf.agda |
| diffstat | 3 files changed, 115 insertions(+), 179 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OD.agda Tue Dec 20 11:20:52 2022 +0900 +++ b/src/OD.agda Thu Dec 22 15:10:31 2022 +0900 @@ -329,61 +329,91 @@ Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } +_=h=_ : (x y : HOD) → Set n +x =h= y = od x == od y + +record Own (A : HOD) (x : Ordinal) : Set n where + field + owner : Ordinal + ao : odef A owner + ox : odef (* owner) x + +Union : HOD → HOD +Union U = record { od = record { def = λ x → Own U x } ; odmax = osuc (& U) ; <odmax = umax } where + umax : {y : Ordinal} → Own U y → y o< osuc (& U) + umax {y} uy = o<→≤ ( ordtrans (odef< (Own.ox uy)) (subst (λ k → k o< & U) (sym &iso) umax1) ) where + umax1 : Own.owner uy o< & U + umax1 = odef< (Own.ao uy) + +union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z +union→ X z u xx = record { owner = & u ; ao = proj1 xx ; ox = subst (λ k → odef k (& z)) (sym *iso) (proj2 xx) } +union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) +union← X z UX∋z not = ⊥-elim ( not (* (Own.owner UX∋z)) ⟪ subst (λ k → odef X k) (sym &iso) ( Own.ao UX∋z) , Own.ox UX∋z ⟫ ) + +record Replaced (A : HOD) (ψ : Ordinal → Ordinal ) (x : Ordinal ) : Set n where + field + z : Ordinal + az : odef A z + x=ψz : x ≡ ψ z + Replace : HOD → (HOD → HOD) → HOD -Replace X ψ = record { od = record { def = λ x → (x o≤ sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x } - ; odmax = rmax ; <odmax = rmax<} where +Replace X ψ = record { od = record { def = λ x → Replaced X (λ z → & (ψ (* z))) x } ; odmax = rmax ; <odmax = rmax< } where rmax : Ordinal - rmax = osuc ( sup-o X (λ y X∋y → & (ψ (* y)))) - rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax - rmax< lt = proj1 lt + rmax = osuc ( sup-o X (λ y X∋y → & (ψ (* y) )) ) + rmax< : {y : Ordinal} → Replaced X (λ z → & (ψ (* z))) y → y o< rmax + rmax< {y} lt = subst (λ k → k o< rmax) r01 ( sup-o≤ X (Replaced.az lt) ) where + r01 : & (ψ ( * (Replaced.z lt ) )) ≡ y + r01 = sym (Replaced.x=ψz lt ) + +replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x +replacement← {ψ} X x lt = record { z = & x ; az = lt ; x=ψz = cong (λ k → & (ψ k)) (sym *iso) } +replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) +replacement→ {ψ} X x lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) -- -- If we have LEM, Replace' is equivalent to Replace -- -in-codomain' : (X : HOD ) → ((x : HOD) → X ∋ x → HOD) → OD -in-codomain' X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ((lt : odef X y) → x ≡ & (ψ (* y ) (d→∋ X lt) )))) } -Replace' : (X : HOD) → ((x : HOD) → X ∋ x → HOD) → HOD -Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x } - ; odmax = rmax ; <odmax = rmax< } where - rmax : Ordinal - rmax = sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y))) - rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain' X ψ) y → y o< rmax - rmax< lt = proj1 lt + +record Replaced1 (A : HOD) (ψ : (x : Ordinal ) → odef A x → Ordinal ) (x : Ordinal ) : Set n where + field + z : Ordinal + az : odef A z + x=ψz : x ≡ ψ z az -Union : HOD → HOD -Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) } - ; odmax = osuc (& U) ; <odmax = umax< } where - umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (* u)) y) → y o< osuc (& U) - umax< {y} not = lemma (FExists _ lemma1 not ) where - lemma0 : {x : Ordinal} → def (od (* x)) y → y o< x - lemma0 {x} x<y = subst₂ (λ j k → j o< k ) &iso &iso (c<→o< (d→∋ (* x) x<y )) - lemma2 : {x : Ordinal} → def (od U) x → x o< & U - lemma2 {x} x<U = subst (λ k → k o< & U ) &iso (c<→o< (d→∋ U x<U)) - lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (* x)) y → ¬ (& U o< y) - lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) ) - lemma : ¬ ((& U) o< y ) → y o< osuc (& U) - lemma not with trio< y (& U) - lemma not | tri< a ¬b ¬c = ordtrans a <-osuc - lemma not | tri≈ ¬a refl ¬c = <-osuc - lemma not | tri> ¬a ¬b c = ⊥-elim (not c) +Replace' : (X : HOD) → ((x : HOD) → X ∋ x → HOD) → HOD +Replace' X ψ = record { od = record { def = λ x → Replaced1 X (λ z xz → & (ψ (* z) (subst (λ k → odef X k) (sym &iso) xz) )) x } ; odmax = rmax ; <odmax = rmax< } where + rmax : Ordinal + rmax = osuc ( sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y) )) ) + rmax< : {y : Ordinal} → Replaced1 X (λ z xz → & (ψ (* z) (subst (λ k → odef X k) (sym &iso) xz) )) y → y o< rmax + rmax< {y} lt = subst (λ k → k o< rmax) r01 ( sup-o≤ X (Replaced1.az lt) ) where + r01 : & (ψ ( * (Replaced1.z lt ) ) (subst (λ k → odef X k) (sym &iso) (Replaced1.az lt) )) ≡ y + r01 = sym (Replaced1.x=ψz lt ) + +-- replacement←1 : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace1 X ψ ∋ ψ x +-- replacement←1 {ψ} X x lt = record { z = & x ; az = lt ; x=ψz = cong (λ k → & (ψ k)) (sym *iso) } +-- replacement→1 : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace1 X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) +-- replacement→1 {ψ} X x lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) + _∈_ : ( A B : HOD ) → Set n A ∈ B = B ∋ A -OPwr : (A : HOD ) → HOD -OPwr A = Ord ( osuc ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) ) ) +Power : HOD → HOD +Power A = record { od = record { def = λ x → ( ( z : Ordinal) → odef (* x) z → odef A z ) } ; odmax = osuc (& A) + ; <odmax = p00 } where + p00 : {y : Ordinal} → ((z : Ordinal) → odef (* y) z → odef A z) → y o< osuc (& A) + p00 {y} y⊆A = p01 where + p01 : y o≤ & A + p01 = subst (λ k → k o≤ & A) &iso ( ⊆→o≤ (λ {x} yx → y⊆A x yx )) -Power : HOD → HOD -Power A = Replace (OPwr (Ord (& A))) ( λ x → A ∩ x ) +power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x +power→ A t P∋t {x} t∋x = P∋t (& x) (subst (λ k → odef k (& x) ) (sym *iso) t∋x ) + +power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t +power← A t t⊆A z xz = subst (λ k → odef A k ) &iso ( t⊆A (subst₂ (λ j k → odef j k) *iso (sym &iso) xz )) + -- ｛_｝ : ZFSet → ZFSet -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly -union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z -union→ X z u xx not = ⊥-elim ( not (& u) ( ⟪ proj1 xx - , subst ( λ k → odef k (& z)) (sym *iso) (proj2 xx) ⟫ )) -union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) -union← X z UX∋z = FExists _ lemma UX∋z where - lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) - lemma {y} xx not = not (* y) ⟪ d→∋ X (proj1 xx) , proj2 xx ⟫ data infinite-d : ( x : Ordinal ) → Set n where iφ : infinite-d o∅ @@ -429,9 +459,6 @@ empty : (x : HOD ) → ¬ (od∅ ∋ x) empty x = ¬x<0 -_=h=_ : (x y : HOD) → Set n -x =h= y = od x == od y - pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x )) pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡y )) @@ -464,20 +491,6 @@ sup-c≤ : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → & (ψ x) o≤ (sup-o X (λ y X∋y → & (ψ (* y)))) sup-c≤ ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o≤ X lt ) -replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x -replacement← {ψ} X x lt = ⟪ sup-c≤ ψ {X} {x} lt , lemma ⟫ where - lemma : def (in-codomain X ψ) (& (ψ x)) - lemma not = ⊥-elim ( not ( & x ) ⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ ) -replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) -replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where - lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y)))) - → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y))) - lemma2 not not2 = not ( λ y d → not2 y ⟪ proj1 d , lemma3 (proj2 d)⟫) where - lemma3 : {y : Ordinal } → (& x ≡ & (ψ (* y))) → (* (& x) =h= ψ (* y)) - lemma3 {y} eq = subst (λ k → * (& x) =h= k ) *iso (o≡→== eq ) - lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) ) - lemma not y not2 = not (* y) (subst (λ k → k =h= ψ (* y)) *iso ( proj2 not2 )) - --- --- Power Set --- @@ -490,116 +503,6 @@ ∩-≡ {a} {b} inc = record { eq→ = λ {x} x<a → ⟪ (subst (λ k → odef b k ) &iso (inc (d→∋ a x<a))) , x<a ⟫ ; eq← = λ {x} x<a∩b → proj2 x<a∩b } --- --- Transitive Set case --- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t --- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t --- OPwr A = Ord ( sup-o ( λ x → & ( A ∩ (* x )) ) ) --- -ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t -ord-power← a t t→A = subst (λ k → odef (OPwr (Ord a)) k ) (lemma1 lemma-eq) lemma where - lemma-eq : ((Ord a) ∩ t) =h= t - eq→ lemma-eq {z} w = proj2 w - eq← lemma-eq {z} w = ⟪ subst (λ k → odef (Ord a) k ) &iso ( t→A (d→∋ t w)) , w ⟫ - lemma1 : {a : Ordinal } { t : HOD } - → (eq : ((Ord a) ∩ t) =h= t) → & ((Ord a) ∩ (* (& t))) ≡ & t - lemma1 {a} {t} eq = subst (λ k → & ((Ord a) ∩ k) ≡ & t ) (sym *iso) (cong (λ k → & k ) (==→o≡ eq )) - lemma2 : (& t) o< (osuc (& (Ord a))) - lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) &iso (t→A (d→∋ t x<t))) - lemma : & ((Ord a) ∩ (* (& t)) ) o≤ sup-o (Ord (osuc (& (Ord a)))) (λ x lt → & ((Ord a) ∩ (* x))) - lemma = sup-o≤ _ lemma2 - --- --- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (& A)) first --- then replace of all elements of the Power set by A ∩ y --- --- Power A = Replace (OPwr (Ord (& A))) ( λ y → A ∩ y ) - --- we have oly double negation form because of the replacement axiom --- -power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x) -power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where - a = & A - lemma2 : ¬ ( (y : HOD) → ¬ (t =h= (A ∩ y))) - lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (& A))) t P∋t - lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x) - lemma3 y eq not = not (proj1 (eq→ eq t∋x)) - lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ * y))) - lemma4 not = lemma2 ( λ y not1 → not (& y) (subst (λ k → t =h= ( A ∩ k )) (sym *iso) not1 )) - lemma5 : {y : Ordinal} → t =h= (A ∩ * y) → ¬ ¬ (odef A (& x)) - lemma5 {y} eq not = (lemma3 (* y) eq) not - -power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t -power← A t t→A = ⟪ lemma1 , lemma2 ⟫ where - a = & A - lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x - lemma0 {x} t∋x = c<→o< (t→A t∋x) - lemma3 : OPwr (Ord a) ∋ t - lemma3 = ord-power← a t lemma0 - lemma4 : (A ∩ * (& t)) ≡ t - lemma4 = let open ≡-Reasoning in begin - A ∩ * (& t) - ≡⟨ cong (λ k → A ∩ k) *iso ⟩ - A ∩ t - ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩ - t - ∎ - sup1 : Ordinal - sup1 = sup-o (Ord (osuc (& (Ord (& A))))) (λ x A∋x → & ((Ord (& A)) ∩ (* x))) - lemma9 : def (od (Ord (Ordinals.osuc O (& (Ord (& A)))))) (& (Ord (& A))) - lemma9 = <-osuc - lemmab : & ((Ord (& A)) ∩ (* (& (Ord (& A) )))) o≤ sup1 - lemmab = sup-o≤ (Ord (osuc (& (Ord (& A))))) lemma9 - lemmad : Ord (osuc (& A)) ∋ t - lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) &iso (t→A (d→∋ t lt))) - lemmac : ((Ord (& A)) ∩ (* (& (Ord (& A) )))) =h= Ord (& A) - lemmac = record { eq→ = lemmaf ; eq← = lemmag } where - lemmaf : {x : Ordinal} → def (od ((Ord (& A)) ∩ (* (& (Ord (& A)))))) x → def (od (Ord (& A))) x - lemmaf {x} lt = proj1 lt - lemmag : {x : Ordinal} → def (od (Ord (& A))) x → def (od ((Ord (& A)) ∩ (* (& (Ord (& A)))))) x - lemmag {x} lt = ⟪ lt , subst (λ k → def (od k) x) (sym *iso) lt ⟫ - lemmae : & ((Ord (& A)) ∩ (* (& (Ord (& A))))) ≡ & (Ord (& A)) - lemmae = cong (λ k → & k ) ( ==→o≡ lemmac) - lemma7 : def (od (OPwr (Ord (& A)))) (& t) - lemma7 with osuc-≡< lemmad - lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o≤ sup1) lemmae lemmab ) - lemma7 | case1 eq with osuc-≡< (⊆→o≤ {* (& t)} {* (& (Ord (& t)))} (λ {x} lt → lemmah lt )) where - lemmah : {x : Ordinal } → def (od (* (& t))) x → def (od (* (& (Ord (& t))))) x - lemmah {x} lt = subst (λ k → def (od k) x ) (sym *iso) (subst (λ k → k o< (& t)) - &iso - (c<→o< (subst₂ (λ j k → def (od j) k) *iso (sym &iso) lt ))) - lemma7 | case1 eq | case1 eq1 = subst (λ k → k o≤ sup1) (trans lemmae lemmai) lemmab where - lemmai : & (Ord (& A)) ≡ & t - lemmai = let open ≡-Reasoning in begin - & (Ord (& A)) - ≡⟨ sym (cong (λ k → & (Ord k)) eq) ⟩ - & (Ord (& t)) - ≡⟨ sym &iso ⟩ - & (* (& (Ord (& t)))) - ≡⟨ sym eq1 ⟩ - & (* (& t)) - ≡⟨ &iso ⟩ - & t - ∎ - lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o≤ sup1) lemmae lemmab ) where - lemmak : & (* (& (Ord (& t)))) ≡ & (Ord (& A)) - lemmak = let open ≡-Reasoning in begin - & (* (& (Ord (& t)))) - ≡⟨ &iso ⟩ - & (Ord (& t)) - ≡⟨ cong (λ k → & (Ord k)) eq ⟩ - & (Ord (& A)) - ∎ - lemmaj : & t o< & (Ord (& A)) - lemmaj = subst₂ (λ j k → j o< k ) &iso lemmak lt - lemma1 : & t o≤ sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x))) - lemma1 = subst (λ k → & k o≤ sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x)))) - lemma4 (sup-o≤ (OPwr (Ord (& A))) lemma7 ) - lemma2 : def (in-codomain (OPwr (Ord (& A))) (_∩_ A)) (& t) - lemma2 not = ⊥-elim ( not (& t) ⟪ lemma3 , lemma6 ⟫ ) where - lemma6 : & t ≡ & (A ∩ * (& t)) - lemma6 = cong ( λ k → & k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym *iso) ( ∩-≡ {t} {A} t→A ))) - extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym &iso) (proj1 (eq (* x))) d
--- a/src/cardinal.agda Tue Dec 20 11:20:52 2022 +0900 +++ b/src/cardinal.agda Thu Dec 22 15:10:31 2022 +0900 @@ -4,12 +4,14 @@ open import zf open import logic -import OD +-- import OD +import OD hiding ( _⊆_ ) + import ODC import OPair -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Relation.Binary.PropositionalEquality -open import Data.Nat.Properties +open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary open import Relation.Binary @@ -29,6 +31,9 @@ open OrdUtil O open ODUtil O +_⊆_ : ( A B : HOD ) → Set n +_⊆_ A B = {x : Ordinal } → odef A x → odef B x + open _∧_ open _∨_ @@ -42,18 +47,18 @@ Func : OD Func = record { def = λ x → def ZFProduct x - ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) } + ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) } FuncP : ( A B : HOD ) → HOD FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x - ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } + ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) } record Injection (A B : Ordinal ) : Set n where field i→ : (x : Ordinal ) → odef (* A) x → Ordinal iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt ) - iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y + iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y record Bijection (A B : Ordinal ) : Set n where field @@ -63,13 +68,37 @@ funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt ) fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x - -Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b -Bernstein = {!!} + +open Injection +open Bijection + +record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where + field + ax : odef (* a) x + bx : odef (* b) (i→ iab _ ax) + +Image : { a b : Ordinal } → Injection a b → HOD +Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = a ; <odmax = λ lt → ? } + +image=a : ? +image=a = ? _=c=_ : ( A B : HOD ) → Set n A =c= B = Bijection ( & A ) ( & B ) +c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?) +c=→≡ = ? + +≡→c= : {A B : HOD} → A ≡ B → A =c= B +≡→c= = ? + +Bernstein : {a b : Ordinal } → Injection a b → Injection b a → Bijection a b +Bernstein {a} {b} iab iba = {!!} where + a⊆b : * a ⊆ * b + a⊆b ax = subst (λ k → odef (* b) k) ? ( iB iab _ ax ) + b⊆a : * b ⊆ * a + b⊆a bx = ? + _c<_ : ( A B : HOD ) → Set n A c< B = ¬ ( Injection (& A) (& B) ) @@ -82,7 +111,7 @@ ciso : Bijection a card cmax : (x : Ordinal) → card o< x → ¬ Bijection a x -Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t +Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t Cardinal∈ = {!!} Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t ) @@ -93,3 +122,7 @@ Cantor2 : { u : HOD } → ¬ ( u =c= Power u ) Cantor2 = {!!} + + + +
--- a/src/zf.agda Tue Dec 20 11:20:52 2022 +0900 +++ b/src/zf.agda Thu Dec 22 15:10:31 2022 +0900 @@ -44,7 +44,7 @@ field empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) - power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x} + power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → A ∋ x -- _⊆_ t A {x} power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )