# HG changeset patch # User Shinji KONO # Date 1563182816 -32400 # Node ID 4c704b7a62e47d886bb7f5765cc93be1fe4740f0 # Parent ebac6fa116fab90542331765c32a441fc7367abd ininite done diff -r ebac6fa116fa -r 4c704b7a62e4 HOD.agda --- a/HOD.agda Mon Jul 15 15:54:59 2019 +0900 +++ b/HOD.agda Mon Jul 15 18:26:56 2019 +0900 @@ -247,9 +247,6 @@ omega : { n : Level } → Ordinal {n} omega = record { lv = Suc Zero ; ord = Φ 1 } -od-infinite : {n : Level} → OD {suc n} -od-infinite = record { def = λ x → x o< sup-o ( λ y → od→ord (Ord y)) } - OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} OD→ZF {n} = record { ZFSet = OD {suc n} @@ -261,7 +258,7 @@ ; Power = Power ; Select = Select ; Replace = Replace - ; infinite = od-infinite + ; infinite = infinite ; isZF = isZF } where ZFSet = OD {suc n} @@ -284,10 +281,18 @@ ｛_｝ : ZFSet → ZFSet ｛ x ｝ = ( x , x ) + data infinite-d : ( x : Ordinal {suc n} ) → Set (suc n) where + iφ : infinite-d o∅ + isuc : {x : Ordinal {suc n} } → infinite-d x → + infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) + + infinite : OD {suc n} + infinite = record { def = λ x → infinite-d x } + infixr 200 _∈_ -- infixr 230 _∩_ _∪_ infixr 220 _⊆_ - isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace od-infinite + isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite isZF = record { isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } ; pair = pair @@ -465,47 +470,23 @@ eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d - uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) ) - uxxx-ord {x} {y} = subst (λ k → def (Union (k , (k , k))) y ⇔ ( y o< osuc (od→ord x) ) ) oiso lemma where - ordΦ : {lx : Nat } → Ordinal {suc n} - ordΦ {lx} = record { lv = lx ; ord = Φ lx } - odΦ : {lx : Nat } → OD {suc n} - odΦ {lx} = ord→od ordΦ - xord : {lx : Nat } → { ox : OrdinalD {suc n} lx } → Ordinal {suc n} - xord {lx} {ox} = record { lv = lx ; ord = ox } - xod : {lx : Nat } → { ox : OrdinalD {suc n} lx } → OD {suc n} - xod {lx} {ox} = ord→od (xord {lx} {ox}) - lemmaφ : (lx : Nat) → def (Union (odΦ {lx} , (odΦ {lx} , odΦ {lx} ))) y ⇔ (y o< osuc (record { lv = lx ; ord = Φ lx })) - proj1 (lemmaφ lx) df = TransFiniteExists _ df lemma where - lemma : {y1 : Ordinal} → def (odΦ {lx} , (odΦ {lx} , odΦ {lx} )) y1 ∧ def (ord→od y1) y → y o< xord {lx} {OSuc lx (Φ lx)} - lemma {y1} xx with proj1 xx | c<→o< {suc n} {ord→od y} {ord→od y1} (def-subst {suc n} {ord→od y1} {y} (proj2 xx) refl (sym diso)) - -- x : lv y1 < lx , x₁ : lv (od→ord (ord→od y) < lv y1 -> lv y < lx - lemma {y1} xx | case1 x | case1 x₁ = - case1 ( <-trans (subst (λ k → lv k < lv (od→ord (ord→od y1))) diso x₁) (subst (λ k → lv k < lx ) (sym diso) {!!}) ) - lemma {y1} xx | case1 x | case2 x₁ with d<→lv x₁ - ... | eq = case1 {!!} - lemma {y1} xx | case2 x | lt = {!!} - proj2 (lemmaφ lx) lt not = not (ordΦ {lx}){!!} - lemma-suc : (lx : Nat) (ox : OrdinalD lx) → - def (Union (xod {lx} {ox} , (xod {lx} {ox} , xod {lx} {ox} ))) y ⇔ (y o< osuc (xord {lx} {ox})) → - def (Union (xod {lx} {OSuc lx ox} , (xod {lx} {OSuc lx ox} , xod {lx} {OSuc lx ox} ))) y - ⇔ (y o< osuc (xord {lx} {OSuc lx ox})) - proj1 (lemma-suc lx ox prev) df = TransFiniteExists _ df {!!} - proj2 (lemma-suc lx ox prev) lt not = not (xord {lx} {ox}) {!!} - lemma = TransFinite {suc n} {λ ox → def (Union (ord→od ox , (ord→od ox , ord→od ox))) y ⇔ ( y o< osuc ox ) } - lemmaφ lemma-suc (od→ord x) where - infinity∅ : od-infinite ∋ od∅ {suc n} - infinity∅ = {!!} -- o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl - infinity : (x : OD) → od-infinite ∋ x → od-infinite ∋ Union (x , (x , x )) - infinity x lt = {!!} where - lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega - lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n) - lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n) - lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ())) - lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ())) - lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2 - lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl + infinity∅ : infinite ∋ od∅ {suc n} + infinity∅ = def-subst {suc n} {_} {_} {infinite} {od→ord (od∅ {suc n})} 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 : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) + infinity x lt = def-subst {suc n} {_} {_} {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 + -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] -- this form is no good since X is a transitive set -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ] record Choice (z : OD {suc n}) : Set (suc (suc n)) where