# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1561631205 -32400
# Node ID 453ef0d4ee8a3e252c5bcc7cc6e476feb2f74e81
# Parent  ac214eab1c3cf92ec664413c6b95c345fbf189bb
...

diff -r ac214eab1c3c -r 453ef0d4ee8a HOD.agda
--- a/HOD.agda	Thu Jun 27 08:34:19 2019 +0900
+++ b/HOD.agda	Thu Jun 27 19:26:45 2019 +0900
@@ -221,17 +221,19 @@
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
-ZFSubset A x =  record { def = λ y → def A y ∧  def x y ; otrans = {!!} }  
+ZFSubset A x =  record { def = λ y → def A y ∧  def x y ; otrans = lemma }   where
+  lemma : {z : Ordinal} → def A z ∧ def x z → {y : Ordinal} → y o< z → def A y ∧ def x y
+  lemma {z} d {y} y<z = record { proj1 = otrans A (proj1 d) y<z ; proj2 = otrans x (proj2 d) y<z }
 
 Def :  {n : Level} → (A :  HOD {suc n}) → HOD {suc n}
-Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
+Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
 -- Constructible Set on α
 L : {n : Level} → (α : Ordinal {suc n}) → HOD {suc n}
 L {n}  record { lv = Zero ; ord = (Φ .0) } = od∅
 L {n}  record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
-    record { def = λ y → osuc y o< (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }) )) ; otrans = {!!} }
+    cseq ( Ord (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }))))
 
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
@@ -318,13 +320,13 @@
          power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
          power→ A t P∋t {x} t∋x = proj1 lemma-s where
               minsup :  HOD
-              minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
+              minsup =  ZFSubset A ( Ord ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
               lemma-t : csuc minsup ∋ t
               lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 
-              lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
+              lemma-s : ZFSubset A ( Ord ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
               lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso  )
-              lemma-s | case1 eq = def-subst {!!} oiso refl
-              lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst {!!} oiso refl ) t∋x
+              lemma-s | case1 eq = {!!}
+              lemma-s | case2 lt = transitive {n} {minsup} {t} {x} {!!} 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