# HG changeset patch # User Shinji KONO # Date 1593768591 -32400 # Node ID 57df07b63cae4a6771768da168655196da2c9149 # Parent c030a9655e79df04f0153c58985187b147bb286a Power done diff -r c030a9655e79 -r 57df07b63cae OD.agda --- a/OD.agda Fri Jul 03 16:51:44 2020 +0900 +++ b/OD.agda Fri Jul 03 18:29:51 2020 +0900 @@ -311,7 +311,7 @@ ; infinity = infinity ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} ; replacement← = replacement← - ; replacement→ = replacement→ + ; replacement→ = λ {ψ} → replacement→ {ψ} -- ; choice-func = choice-func -- ; choice = choice } where @@ -415,7 +415,7 @@ 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→ (OPwr (Ord (od→ord A))) t P∋t + 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))) @@ -435,34 +435,64 @@ A ∩ ord→od (od→ord t) ≡⟨ cong (λ k → A ∩ k) oiso ⟩ A ∩ t - ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ + ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩ t ∎ - --- (od→ord t) o< (sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x)))) + sup1 : Ordinal sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (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 (ZFSubset (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 = {!!} + lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A) - lemmac = record { eq→ = {!!} ; eq← = {!!} } + lemmac = record { eq→ = lemmaf ; eq← = lemmag } where + lemmaf : {x : Ordinal} → def (od (ZFSubset (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 (ZFSubset (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 (ZFSubset (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 → {!!} )) - lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae {!!}) lemmab -- od→ord (Ord (od→ord A)) ≡ od→ord t - lemma7 | case1 eq | case2 lt = ordtrans {!!} (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 : odef (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 ))) + 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))