Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff HOD.agda @ 144:3ba37037faf4
Union again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Jul 2019 13:21:14 +0900 |
| parents | 21b9e78e9359 |
| children | f0fa9a755513 |
line wrap: on
line diff
--- a/HOD.agda Mon Jul 08 12:34:08 2019 +0900 +++ b/HOD.agda Mon Jul 08 13:21:14 2019 +0900 @@ -292,22 +292,22 @@ ; infinite = Ord omega ; isZF = isZF } where + ZFSet = OD {suc n} Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n} Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } _,_ : OD {suc n} → OD {suc n} → OD {suc n} x , y = Ord (omax (od→ord x) (od→ord y)) + _∩_ : ( A B : ZFSet ) → ZFSet + A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) Union : OD {suc n} → OD {suc n} - Union U = cseq U + Union U = Replace ( record { def = λ x → osuc x o< od→ord U } ) ( λ x → U ∩ x ) -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) - ZFSet = OD {suc n} _∈_ : ( A B : ZFSet ) → Set (suc n) A ∈ B = B ∋ A _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) _⊆_ A B {x} = A ∋ x → B ∋ x - _∩_ : ( A B : ZFSet ) → ZFSet - A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) Power : OD {suc n} → OD {suc n} Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) -- _∪_ : ( A B : ZFSet ) → ZFSet @@ -346,6 +346,48 @@ empty x (case1 ()) empty x (case2 ()) + union-lemma : {n : Level } {X z u : OD {suc n} } → (X ∋ u) → (u ∋ z) → osuc ( od→ord z ) o< od→ord u → X ∋ Ord (osuc ( od→ord z ) ) + union-lemma = {!!} + union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} + union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) + union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z + union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z )) + union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) + union→ X z u xx | tri< a ¬b ¬c | () + union→ X z u xx | tri≈ ¬a b ¬c = {!!} + union→ X z u xx | tri> ¬a ¬b c = {!!} --- osuc ( od→ord z )) o< od→ord u o< od→ord X + -- def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (union-lemma {n} {X} {z} {u} (proj1 xx) (proj2 xx) c ) refl (sym ord-Ord) + union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z ) + union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where + lemma : X ∋ union-u {X} {z} X∋z + lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} {!!} refl ord-Ord + + ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y + ψiso {ψ} t refl = t + selection : {ψ : OD → Set (suc n)} {X y : OD} → ((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 } + } + replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x + replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; 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 (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } )) + replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) + replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where + lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y)))) + → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord 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 y))) → (ord→od (od→ord x) == ψ (Ord y)) + lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq ) + lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) ) + lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso ( proj2 not2 )) + + --- + --- Power Set + --- + --- First consider ordinals in OD --- --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A @@ -409,42 +451,9 @@ lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) lemma = sup-o< - union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} - union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) - union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z - union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z )) - union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) - union→ X z u xx | tri< a ¬b ¬c | () - union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b - union→ X z u xx | tri> ¬a ¬b c = {!!} --- osuc ( od→ord z )) o< od→ord u o< od→ord X - - union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z ) - union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where - lemma : X ∋ union-u {X} {z} X∋z - lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord - - ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y - ψiso {ψ} t refl = t - selection : {ψ : OD → Set (suc n)} {X y : OD} → ((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 } - } - replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x - replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; 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 (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } )) - replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) - replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where - lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y)))) - → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord 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 y))) → (ord→od (od→ord x) == ψ (Ord y)) - lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq ) - lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) ) - lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso ( proj2 not2 )) - + -- + -- Every set in OD is a subset of Ordinals + -- -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x power→ A t P∋t {x} t∋x = TransFiniteExists {suc n} {λ y → (t == (A ∩ ord→od y))} @@ -499,7 +508,7 @@ lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) lemma {y} = let open ≡-Reasoning in begin def (Union (x , (x , x))) y - ≡⟨⟩ + ≡⟨ {!!} ⟩ def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y ) ≡⟨⟩ osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) )