Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 260:8b85949bde00
sup with limit give up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 05 Sep 2019 10:58:06 +0900 |
| parents | f714fe999102 |
| children | d9d178d1457c |
| files | OD.agda |
| diffstat | 1 files changed, 16 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Thu Sep 05 01:28:52 2019 +0900 +++ b/OD.agda Thu Sep 05 10:58:06 2019 +0900 @@ -75,8 +75,8 @@ -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x -- ord→od x ≡ Ord x results the same -- supermum as Replacement Axiom - sup-o : Ordinal → ( Ordinal → Ordinal ) → Ordinal - sup-o< : {X : Ordinal} → { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → x o< X → ψ x o< sup-o X ψ + sup-o : ( Ordinal → Ordinal ) → Ordinal + sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ -- contra-position of mimimulity of supermum required in Power Set Axiom -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) @@ -106,14 +106,14 @@ def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x def-subst df refl refl = df -sup-od : OD → ( OD → OD ) → OD -sup-od X ψ = Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) ) +sup-od : ( OD → OD ) → OD +sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) -sup-c< : {X : OD } ( ψ : OD → OD ) → ∀ {x : OD } → X ∋ x → def ( sup-od X ψ ) (od→ord ( ψ x )) -sup-c< {X} ψ {x} lt = def-subst {_} {_} {Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )} +sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x )) +sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )} lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where - lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (od→ord X) (λ x → od→ord (ψ (ord→od x))) - lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< (c<→o< lt) ) refl (sym diso) ) + lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) + lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso) ) otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y otrans x<a y<x = ordtrans y<x x<a @@ -337,8 +337,7 @@ ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set Def : (A : OD ) → OD -Def A = Ord ( sup-o (osuc (od→ord A)) ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) - +Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n _⊆_ A B {x} = A ∋ x → B ∋ x @@ -369,7 +368,7 @@ Select : (X : OD ) → ((x : OD ) → Set n ) → OD Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } Replace : OD → (OD → OD ) → OD - Replace X ψ = record { def = λ x → (x o< sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } + Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = record { def = λ x → def A x ∧ def B x } Union : OD → OD @@ -449,7 +448,7 @@ ; 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} lt ; proj2 = lemma } where + 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 oiso)} )) replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) @@ -492,16 +491,8 @@ lemma1 : {a : Ordinal } { t : OD } → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) - lemma3 : {x : OD} → (lt : t ∋ x ) → Ord (od→ord t) ∋ x - lemma3 lt = c<→o< lt - lemma2 : ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → od→ord t o< osuc (od→ord (Ord a)) - lemma2 t→A = lemma5 t→A where - lemma6 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → {x : OD} → Ord (od→ord t) ∋ x → Ord ( od→ord s) ∋ x - lemma6 = {!!} - lemma5 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → od→ord t o< osuc ( od→ord s) - lemma5 t→A = ⊆→o< ( λ z → lemma6 t→A ) - lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (osuc (od→ord (Ord a))) (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) - lemma = sup-o< (lemma2 t→A) + 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< -- -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first @@ -538,11 +529,9 @@ ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ t ∎ - lemma5 : od→ord t o< od→ord (Def (Ord (od→ord A))) - lemma5 = {!!} - lemma1 : od→ord t o< sup-o (od→ord (Def (Ord (od→ord A)))) (λ x → od→ord (A ∩ ord→od x)) - lemma1 = subst (λ k → od→ord k o< sup-o (od→ord (Def (Ord (od→ord A)))) (λ x → od→ord (A ∩ ord→od x))) - lemma4 (sup-o< {od→ord (Def (Ord (od→ord A)))} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} lemma5 ) + lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) + lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x))) + lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t} ) lemma2 : def (in-codomain (Def (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))