Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 365:7f919d6b045b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 Jul 2020 12:29:38 +0900 |
| parents | 67580311cc8e |
| children | 1a8ca713bc32 |
| files | LEMC.agda OD.agda ODC.agda OPair.agda filter.agda |
| diffstat | 5 files changed, 363 insertions(+), 366 deletions(-) [+] |
line wrap: on
line diff
--- a/LEMC.agda Sat Jul 18 11:38:33 2020 +0900 +++ b/LEMC.agda Sat Jul 18 12:29:38 2020 +0900 @@ -31,8 +31,6 @@ is-in : X ∋ a-choice open HOD -_=h=_ : (x y : HOD) → Set n -x =h= y = od x == od y open choiced
--- a/OD.agda Sat Jul 18 11:38:33 2020 +0900 +++ b/OD.agda Sat Jul 18 12:29:38 2020 +0900 @@ -327,357 +327,353 @@ ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy +Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD +Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } +Replace : HOD → (HOD → HOD) → HOD +Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x } + ; odmax = rmax ; <odmax = rmax<} where + rmax : Ordinal + rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) + rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax + rmax< lt = proj1 lt +Union : HOD → HOD +Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } + ; odmax = osuc (od→ord U) ; <odmax = umax< } where + umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) + umax< {y} not = lemma (FExists _ lemma1 not ) where + lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x + lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y)) + lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U + lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U)) + lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y) + lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) ) + lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U) + lemma not with trio< y (od→ord 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) +_∈_ : ( A B : HOD ) → Set n +A ∈ B = B ∋ A + +OPwr : (A : HOD ) → HOD +OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) ) + +Power : HOD → HOD +Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) +-- ｛_｝ : ZFSet → ZFSet +-- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly + +data infinite-d : ( x : Ordinal ) → Set n where + iφ : infinite-d o∅ + isuc : {x : Ordinal } → infinite-d x → + infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) + +-- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. +-- We simply assumes infinite-d y has a maximum. +-- +-- This means that many of OD may not be HODs because of the od→ord mapping divergence. +-- We should have some axioms to prevent this such as od→ord x o< next (odmax x). +-- +postulate + ωmax : Ordinal + <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax + +infinite : HOD +infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } + +infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD +infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where + u : (y : Ordinal ) → HOD + u y = Union (ord→od y , (ord→od y , ord→od y)) + -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z + lemma8 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y)) + lemma8 = ho< + --- (x,y) < next (omax x y) < next (osuc y) = next y + lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y) + lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< ) + lemma81 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y)) + lemma81 {y} = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) + lemma9 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y)) + lemma9 = lemmaa (c<→o< (case1 refl)) + lemma71 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y)) + lemma71 = next< lemma81 lemma9 + lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) + lemma1 = ho< + --- main recursion + lemma : {y : Ordinal} → infinite-d y → y o< next o∅ + lemma {o∅} iφ = x<nx + lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1)) + +ω<next-o∅ : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅ +ω<next-o∅ ho< {y} lt = <odmax (infinite' ho<) lt + +nat→ω : Nat → HOD +nat→ω Zero = od∅ +nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) + +ω→nat : (n : HOD) → infinite ∋ n → Nat +ω→nat n = lemma where + lemma : {y : Ordinal} → infinite-d y → Nat + lemma iφ = Zero + lemma (isuc lt) = Suc (lemma lt) + +ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n)) +ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ +ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n})) + +_=h=_ : (x y : HOD) → Set n +x =h= y = od x == od y + +infixr 200 _∈_ +-- infixr 230 _∩_ _∪_ + +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 ) oiso oiso (o≡→== t≡x )) +pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y )) + +pair← : ( x y t : HOD ) → ( t =h= x ) ∨ ( t =h= y ) → (x , y) ∋ t +pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x)) +pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y)) + +empty : (x : HOD ) → ¬ (od∅ ∋ x) +empty x = ¬x<0 + +o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) +o<→c< lt = record { incl = λ z → ordtrans z lt } + +⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y +⊆→o< {x} {y} lt with trio< x y +⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc +⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc +⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) +... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) + +union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z +union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx + ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (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 (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + +ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y +ψiso {ψ} t refl = t +selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) +selection {ψ} {X} {y} = record { + proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } + ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } + } +sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) +sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt ) +replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x +replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {X} {x} lt ; proj2 = lemma } where + lemma : def (in-codomain X ψ) (od→ord (ψ x)) + lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) +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 ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) + → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y))) + lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where + lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) =h= ψ (ord→od y)) + lemma3 {y} eq = subst (λ k → ord→od (od→ord x) =h= k ) oiso (o≡→== eq ) + lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) ) + lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso ( proj2 not2 )) + +--- +--- Power Set +--- +--- First consider ordinals in HOD +--- +--- A ∩ x = record { def = λ y → odef A y ∧ odef x y } subset of A +-- +-- +∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a ) +∩-≡ {a} {b} inc = record { + eq→ = λ {x} x<a → record { proj2 = x<a ; + proj1 = odef-subst {_} {_} {b} {x} (inc (odef-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; + 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 → od→ord ( A ∩ (ord→od x )) ) ) +-- +ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t +ord-power← a t t→A = odef-subst {_} {_} {OPwr (Ord a)} {od→ord t} + lemma refl (lemma1 lemma-eq )where + lemma-eq : ((Ord a) ∩ t) =h= t + eq→ lemma-eq {z} w = proj2 w + eq← lemma-eq {z} w = record { proj2 = w ; + proj1 = odef-subst {_} {_} {(Ord a)} {z} + ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } + lemma1 : {a : Ordinal } { t : HOD } + → (eq : ((Ord a) ∩ t) =h= t) → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t + lemma1 {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) + lemma2 : (od→ord t) o< (osuc (od→ord (Ord a))) + lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) + lemma : od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x))) + lemma = sup-o< _ lemma2 + +-- +-- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first +-- then replace of all elements of the Power set by A ∩ y +-- +-- Power A = Replace (OPwr (Ord (od→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 = od→ord A + lemma2 : ¬ ( (y : HOD) → ¬ (t =h= (A ∩ y))) + lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→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 ∩ ord→od y))) + lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 )) + lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) → ¬ ¬ (odef A (od→ord x)) + lemma5 {y} eq not = (lemma3 (ord→od y) eq) not + +power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t +power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where + a = od→ord 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 ∩ ord→od (od→ord t)) ≡ t + lemma4 = let open ≡-Reasoning in begin + A ∩ ord→od (od→ord t) + ≡⟨ cong (λ k → A ∩ k) oiso ⟩ + A ∩ t + ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩ + t + ∎ + sup1 : Ordinal + sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x))) + lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) + lemma9 = <-osuc + lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 + lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 + lemmad : Ord (osuc (od→ord A)) ∋ t + lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) + lemmac : ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A) + lemmac = record { eq→ = lemmaf ; eq← = lemmag } where + lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x + lemmaf {x} lt = proj1 lt + lemmag : {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x + lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } + lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) + lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac) + lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord 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≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where + lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x + lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t)) + diso + (c<→o< (subst₂ (λ j k → def (od j) k) oiso (sym diso) lt ))) + lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where + lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t + lemmai = let open ≡-Reasoning in begin + od→ord (Ord (od→ord A)) + ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩ + od→ord (Ord (od→ord t)) + ≡⟨ sym diso ⟩ + od→ord (ord→od (od→ord (Ord (od→ord t)))) + ≡⟨ sym eq1 ⟩ + od→ord (ord→od (od→ord t)) + ≡⟨ diso ⟩ + od→ord t + ∎ + lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where + lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A)) + lemmak = let open ≡-Reasoning in begin + od→ord (ord→od (od→ord (Ord (od→ord t)))) + ≡⟨ diso ⟩ + od→ord (Ord (od→ord t)) + ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩ + od→ord (Ord (od→ord A)) + ∎ + lemmaj : od→ord t o< od→ord (Ord (od→ord A)) + lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt + lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) + lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) + lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) + lemma2 : def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) + lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where + lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) + lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A ))) + + +ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) +ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where + lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y + lemma lt y<x with osuc-≡< lt + lemma lt y<x | case1 refl = c<→o< y<x + lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a + +continuum-hyphotheis : (a : Ordinal) → Set (suc n) +continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc 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 diso) (proj1 (eq (ord→od x))) d +eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d + +extensionality : {A B w : HOD } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) +proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d +proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d + +infinity∅ : infinite ∋ od∅ +infinity∅ = odef-subst {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where + lemma : o∅ ≡ od→ord od∅ + lemma = let open ≡-Reasoning in begin + o∅ + ≡⟨ sym diso ⟩ + od→ord ( ord→od o∅ ) + ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩ + od→ord od∅ + ∎ +infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) +infinity x lt = odef-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where + lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x)))) + ≡ od→ord (Union (x , (x , x))) + lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso + +isZF : IsZF (HOD ) _∋_ _=h=_ od∅ _,_ Union Power Select Replace infinite +isZF = record { + isEquivalence = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans } + ; pair→ = pair→ + ; pair← = pair← + ; union→ = union→ + ; union← = union← + ; empty = empty + ; power→ = power→ + ; power← = power← + ; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} + ; ε-induction = ε-induction + ; infinity∅ = infinity∅ + ; infinity = infinity + ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} + ; replacement← = replacement← + ; replacement→ = λ {ψ} → replacement→ {ψ} + -- ; choice-func = choice-func + -- ; choice = choice + } + HOD→ZF : ZF HOD→ZF = record { ZFSet = HOD ; _∋_ = _∋_ - ; _≈_ = hod→zf._=h=_ + ; _≈_ = _=h=_ ; ∅ = od∅ ; _,_ = _,_ - ; Union = hod→zf.Union - ; Power = hod→zf.Power - ; Select = hod→zf.Select - ; Replace = hod→zf.Replace - ; infinite = hod→zf.infinite - ; isZF = hod→zf.isZF - } where - module hod→zf where - ZFSet = HOD -- is less than Ords because of maxod - Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD - Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } - Replace : HOD → (HOD → HOD) → HOD - Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x } - ; odmax = rmax ; <odmax = rmax<} where - rmax : Ordinal - rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) - rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax - rmax< lt = proj1 lt - Union : HOD → HOD - Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } - ; odmax = osuc (od→ord U) ; <odmax = umax< } where - umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) - umax< {y} not = lemma (FExists _ lemma1 not ) where - lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x - lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y)) - lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U - lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U)) - lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y) - lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) ) - lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U) - lemma not with trio< y (od→ord 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) - _∈_ : ( A B : ZFSet ) → Set n - A ∈ B = B ∋ A - - OPwr : (A : HOD ) → HOD - OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) ) - - Power : HOD → HOD - Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) - -- ｛_｝ : ZFSet → ZFSet - -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly - - data infinite-d : ( x : Ordinal ) → Set n where - iφ : infinite-d o∅ - isuc : {x : Ordinal } → infinite-d x → - infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) - - -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. - -- We simply assumes infinite-d y has a maximum. - -- - -- This means that many of OD may not be HODs because of the od→ord mapping divergence. - -- We should have some axioms to prevent this such as od→ord x o< next (odmax x). - -- - postulate - ωmax : Ordinal - <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax - - infinite : HOD - infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } - - infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD - infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where - u : (y : Ordinal ) → HOD - u y = Union (ord→od y , (ord→od y , ord→od y)) - -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z - lemma8 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y)) - lemma8 = ho< - --- (x,y) < next (omax x y) < next (osuc y) = next y - lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y) - lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< ) - lemma81 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y)) - lemma81 {y} = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) - lemma9 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y)) - lemma9 = lemmaa (c<→o< (case1 refl)) - lemma71 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y)) - lemma71 = next< lemma81 lemma9 - lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) - lemma1 = ho< - --- main recursion - lemma : {y : Ordinal} → infinite-d y → y o< next o∅ - lemma {o∅} iφ = x<nx - lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1)) - - nat→ω : Nat → HOD - nat→ω Zero = od∅ - nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) - - ω→nat : (n : HOD) → infinite ∋ n → Nat - ω→nat n = lemma where - lemma : {y : Ordinal} → infinite-d y → Nat - lemma iφ = Zero - lemma (isuc lt) = Suc (lemma lt) - - ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n)) - ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ - ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n})) - - _=h=_ : (x y : HOD) → Set n - x =h= y = od x == od y - - infixr 200 _∈_ - -- infixr 230 _∩_ _∪_ - isZF : IsZF (HOD ) _∋_ _=h=_ od∅ _,_ Union Power Select Replace infinite - isZF = record { - isEquivalence = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans } - ; pair→ = pair→ - ; pair← = pair← - ; union→ = union→ - ; union← = union← - ; empty = empty - ; power→ = power→ - ; power← = power← - ; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} - ; ε-induction = ε-induction - ; infinity∅ = infinity∅ - ; infinity = infinity - ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} - ; replacement← = replacement← - ; replacement→ = λ {ψ} → replacement→ {ψ} - -- ; choice-func = choice-func - -- ; choice = choice - } where - - pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) - pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x )) - pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y )) - - pair← : ( x y t : ZFSet ) → ( t =h= x ) ∨ ( t =h= y ) → (x , y) ∋ t - pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x)) - pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y)) - - empty : (x : HOD ) → ¬ (od∅ ∋ x) - empty x = ¬x<0 - - o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) - o<→c< lt = record { incl = λ z → ordtrans z lt } - - ⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y - ⊆→o< {x} {y} lt with trio< x y - ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc - ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc - ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) - ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) - - union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z - union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx - ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (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 (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) - lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + ; Union = Union + ; Power = Power + ; Select = Select + ; Replace = Replace + ; infinite = infinite + ; isZF = isZF + } + - ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y - ψiso {ψ} t refl = t - selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) - selection {ψ} {X} {y} = record { - proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } - ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } - } - sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) - sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt ) - replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x - replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {X} {x} lt ; proj2 = lemma } where - lemma : def (in-codomain X ψ) (od→ord (ψ x)) - lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) - 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 ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) - → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y))) - lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where - lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) =h= ψ (ord→od y)) - lemma3 {y} eq = subst (λ k → ord→od (od→ord x) =h= k ) oiso (o≡→== eq ) - lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) ) - lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso ( proj2 not2 )) - - --- - --- Power Set - --- - --- First consider ordinals in HOD - --- - --- A ∩ x = record { def = λ y → odef A y ∧ odef x y } subset of A - -- - -- - ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a ) - ∩-≡ {a} {b} inc = record { - eq→ = λ {x} x<a → record { proj2 = x<a ; - proj1 = odef-subst {_} {_} {b} {x} (inc (odef-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; - 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 → od→ord ( A ∩ (ord→od x )) ) ) - -- - ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t - ord-power← a t t→A = odef-subst {_} {_} {OPwr (Ord a)} {od→ord t} - lemma refl (lemma1 lemma-eq )where - lemma-eq : ((Ord a) ∩ t) =h= t - eq→ lemma-eq {z} w = proj2 w - eq← lemma-eq {z} w = record { proj2 = w ; - proj1 = odef-subst {_} {_} {(Ord a)} {z} - ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } - lemma1 : {a : Ordinal } { t : HOD } - → (eq : ((Ord a) ∩ t) =h= t) → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t - lemma1 {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) - lemma2 : (od→ord t) o< (osuc (od→ord (Ord a))) - lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) - lemma : od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x))) - lemma = sup-o< _ lemma2 - - -- - -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first - -- then replace of all elements of the Power set by A ∩ y - -- - -- Power A = Replace (OPwr (Ord (od→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 = od→ord A - lemma2 : ¬ ( (y : HOD) → ¬ (t =h= (A ∩ y))) - lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→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 ∩ ord→od y))) - lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 )) - lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) → ¬ ¬ (odef A (od→ord x)) - lemma5 {y} eq not = (lemma3 (ord→od y) eq) not - - power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t - power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where - a = od→ord 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 ∩ ord→od (od→ord t)) ≡ t - lemma4 = let open ≡-Reasoning in begin - A ∩ ord→od (od→ord t) - ≡⟨ cong (λ k → A ∩ k) oiso ⟩ - A ∩ t - ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩ - t - ∎ - sup1 : Ordinal - sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x))) - lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) - lemma9 = <-osuc - lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 - lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 - lemmad : Ord (osuc (od→ord A)) ∋ t - lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) - lemmac : ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A) - lemmac = record { eq→ = lemmaf ; eq← = lemmag } where - lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x - lemmaf {x} lt = proj1 lt - lemmag : {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x - lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } - lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) - lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac) - lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord 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≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where - lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x - lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t)) - diso - (c<→o< (subst₂ (λ j k → def (od j) k) oiso (sym diso) lt ))) - lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where - lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t - lemmai = let open ≡-Reasoning in begin - od→ord (Ord (od→ord A)) - ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩ - od→ord (Ord (od→ord t)) - ≡⟨ sym diso ⟩ - od→ord (ord→od (od→ord (Ord (od→ord t)))) - ≡⟨ sym eq1 ⟩ - od→ord (ord→od (od→ord t)) - ≡⟨ diso ⟩ - od→ord t - ∎ - lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where - lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A)) - lemmak = let open ≡-Reasoning in begin - od→ord (ord→od (od→ord (Ord (od→ord t)))) - ≡⟨ diso ⟩ - od→ord (Ord (od→ord t)) - ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩ - od→ord (Ord (od→ord A)) - ∎ - lemmaj : od→ord t o< od→ord (Ord (od→ord A)) - lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt - lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) - lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) - lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) - lemma2 : def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) - lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where - lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) - lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A ))) - - - ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) - ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where - lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y - lemma lt y<x with osuc-≡< lt - lemma lt y<x | case1 refl = c<→o< y<x - lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a - - continuum-hyphotheis : (a : Ordinal) → Set (suc n) - continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc 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 diso) (proj1 (eq (ord→od x))) d - eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d - - extensionality : {A B w : HOD } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) - proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d - proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d - - infinity∅ : infinite ∋ od∅ - infinity∅ = odef-subst {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where - lemma : o∅ ≡ od→ord od∅ - lemma = let open ≡-Reasoning in begin - o∅ - ≡⟨ sym diso ⟩ - od→ord ( ord→od o∅ ) - ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩ - od→ord od∅ - ∎ - infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) - infinity x lt = odef-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where - lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x)))) - ≡ od→ord (Union (x , (x , x))) - lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso - - -Union = ZF.Union HOD→ZF -Power = ZF.Power HOD→ZF -Select = ZF.Select HOD→ZF -Replace = ZF.Replace HOD→ZF -infinite = ZF.infinite HOD→ZF -isZF = ZF.isZF HOD→ZF -
--- a/ODC.agda Sat Jul 18 11:38:33 2020 +0900 +++ b/ODC.agda Sat Jul 18 12:29:38 2020 +0900 @@ -25,9 +25,6 @@ open _∧_ -_=h=_ : (x y : HOD) → Set n -x =h= y = od x == od y - postulate -- mimimul and x∋minimal is an Axiom of choice minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
--- a/OPair.agda Sat Jul 18 11:38:33 2020 +0900 +++ b/OPair.agda Sat Jul 18 12:29:38 2020 +0900 @@ -28,9 +28,6 @@ open _==_ -_=h=_ : (x y : HOD) → Set n -x =h= y = od x == od y - <_,_> : (x y : HOD) → HOD < x , y > = (x , x ) , (x , y )
--- a/filter.agda Sat Jul 18 11:38:33 2020 +0900 +++ b/filter.agda Sat Jul 18 12:29:38 2020 +0900 @@ -71,8 +71,6 @@ q∩q⊆q = record { incl = λ lt → proj1 lt } open HOD -_=h=_ : (x y : HOD) → Set n -x =h= y = od x == od y ----- -- @@ -157,16 +155,9 @@ ODSuc : (y : HOD) → infinite ∋ y → HOD ODSuc y lt = Union (y , (y , y)) -nat→ω : Nat → HOD -nat→ω Zero = od∅ -nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) +postulate + ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) -postulate -- we have proved in other module - ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n)) - ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ - -postulate - ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) data Hω2 : ( x : Ordinal ) → Set n where hφ : Hω2 o∅ @@ -179,6 +170,8 @@ HODω2 : HOD HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where + ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ + ω<next = ω<next-o∅ ho< lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n → od→ord < ord→od n , ord→od y > o< next y lemma0 {n} {y} hw2 inf = nexto=n {!!} odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅ @@ -187,6 +180,22 @@ odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {1} ))) odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {2} ))) +HODω2-Filter : Filter HODω2 +HODω2-Filter = record { + filter = {!!} + ; f⊆PL = {!!} + ; filter1 = {!!} + ; filter2 = {!!} + } where + filter0 : HOD + filter0 = {!!} + f⊆PL1 : filter0 ⊆ Power HODω2 + f⊆PL1 = {!!} + filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q + filter11 = {!!} + filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) + filter12 = {!!} + -- the set of finite partial functions from ω to 2 data Two : Set n where