# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562633798 -32400
# Node ID b5a337fb7a6db30b4377b771bdcb7710b307d670
# Parent  ebcbfd9d9c8ef988cfe3fa1fe91195860d4eb8ce
recovering...

diff -r ebcbfd9d9c8e -r b5a337fb7a6d HOD.agda
--- a/HOD.agda	Mon Jul 08 22:37:10 2019 +0900
+++ b/HOD.agda	Tue Jul 09 09:56:38 2019 +0900
@@ -311,6 +311,9 @@
          empty x (case1 ())
          empty x (case2 ())
 
+         ord-⊆ : ( t x : OD {suc n} ) → _⊆_ t (Ord (od→ord t )) {x}
+         ord-⊆ t x lt = c<→o< lt
+
          union-d : (X : OD {suc n}) → OD {suc n}
          union-d X = record { def = λ y → def X (osuc y) }
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
@@ -363,45 +366,27 @@
          --
          --  if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t 
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
-         --    In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity
+         --    In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity of Ordinals
          --
-         POrd : {a : Ordinal } {t : OD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
-         POrd {a} {t} P∋t = {!!}
          ∩-≡ :  { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
          ∩-≡ {a} {b} inc = record {
             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  (POrd P∋t))
-         ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )  where
-              Ltx :   {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
-              Ltx {n} {x} {t} lt = c<→o< lt
+         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 minsup is Ord (minα a sp) 
-              lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
-              lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))
-              ... | eq with subst ( λ k →  ZFSubset (Ord a) k ≡ Ord (minα a sp)) {!!} eq
-              ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} {!!} lemma2 {!!} where
-                  lemma2 : Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡ minsup
-                  lemma2 =  let open ≡-Reasoning in begin
-                      Ord (od→ord (ZFSubset (Ord a) (ord→od sp)))
-                    ≡⟨ cong (λ k → Ord (od→ord k)) eq1 ⟩
-                      Ord (od→ord (Ord (minα a sp))) 
-                    ≡⟨ cong (λ k → Ord (od→ord k)) {!!}  ⟩
-                      Ord (od→ord (ord→od (minα a sp))) 
-                    ≡⟨ cong (λ k → Ord k) diso ⟩
-                      Ord (minα a sp)
-                    ≡⟨ sym eq1 ⟩
-                      minsup
-                    ∎
+              -- 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) )
+              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
@@ -444,14 +429,16 @@
               lemma3 : Def (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
               lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
-              lemma4 = cong ( λ k → od→ord k ) ( ==→o≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} ))
+              lemma4 = {!!}
               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 )) {!!}
               lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
-              lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = {!!} }) ) where
+              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 == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
 
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq