### changeset 317:57df07b63cae

Power done
author Shinji KONO Fri, 03 Jul 2020 18:29:51 +0900 c030a9655e79 9e0c97ab3a4a OD.agda 1 files changed, 40 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- 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 = ⊆→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 | 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))