diff HOD.agda @ 152:996a67042f50

power set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Jul 2019 17:46:45 +0900
parents b5a337fb7a6d
children f1801c4735d3
line wrap: on
line diff
--- a/HOD.agda	Tue Jul 09 09:56:38 2019 +0900
+++ b/HOD.agda	Tue Jul 09 17:46:45 2019 +0900
@@ -373,20 +373,20 @@
             eq→ = λ {x} x<a → record { proj2 = x<a ;
                  proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
             eq← = λ {x} x<a∩b → proj2 x<a∩b }
-         ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x
-         ord-power→ a t P∋t {x} t∋x with osuc-≡<  (sup-lb  P∋t )
-         ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )  
-         ... | case2 lt = lemma3 where
-              sp =  sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
-              minsup :  OD
-              minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
-              Ltx :   {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
-              Ltx {n} {x} {t} lt = c<→o< lt
-              -- lemma1 hold because a subset of ordinals is ordinal
-              lemma1 : od→ord t o< od→ord minsup → minsup ∋ Ord (od→ord t)
-              lemma1 lt = {!!}
-              lemma3 : od→ord x o< a
-              lemma3 = otrans (proj1 (lemma1 lt)) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) )
+         -- ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x
+         -- ord-power→ a t P∋t {x} t∋x with osuc-≡<  (sup-lb  P∋t )
+         -- ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )  
+         -- ... | case2 lt = lemma3 where
+         --      sp =  sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
+         --      minsup :  OD
+         --      minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
+         --      Ltx :   {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
+         --      Ltx {n} {x} {t} lt = c<→o< lt
+         --      -- lemma1 hold because a subset of ordinals is ordinal
+         --      lemma1 : od→ord t o< od→ord minsup → minsup ∋ Ord (od→ord t)
+         --      lemma1 lt = {!!}
+         --      lemma3 : od→ord x o< a
+         --      lemma3 = otrans (proj1 (lemma1 lt)) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) )
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
@@ -428,13 +428,19 @@
               lemma0 {x} t∋x = c<→o< (t→A t∋x)
               lemma3 : Def (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
-              lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
-              lemma4 = {!!}
+              lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x))
+              lt1 = sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
+              lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
+              lemma4 = let open ≡-Reasoning in begin
+                    A ∩ ord→od (od→ord t)
+                 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
+                    A ∩ t
+                 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
+                    t
+                 ∎
               lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
-              lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
-              ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
-                  lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
-                  lemma5 = cong (λ k → od→ord (A ∩ k )) {!!}
+              lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x)))
+                  lemma4 (sup-o< {suc n} {λ 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))