--- a/ordinal-definable.agda	Sun Jun 09 19:41:53 2019 +0900
+++ b/ordinal-definable.agda	Mon Jun 10 00:29:20 2019 +0900
@@ -54,7 +54,10 @@
   oiso   : {n : Level} {x : OD {n}}      → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   sup-o  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
-  sup-o< : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ∀ {x : Ordinal {n}} →  ψ x  o<  sup-o ψ 
+  sup-o< : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → ∀ {x : Ordinal {n}} →  ψ x  o<  sup-o ψ 
+  sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
+  sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
+  -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
 
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
@@ -73,7 +76,7 @@
 
 sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x ))
 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {sup-od ψ} {od→ord ( ψ x )}
-        ( o<→c< ( sup-o< ( λ y → od→ord (ψ (ord→od y ))) {od→ord x } )) refl (cong ( λ k → od→ord (ψ k) ) oiso)
+        ( o<→c< sup-o< ) refl (cong ( λ k → od→ord (ψ k) ) oiso)
 
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
@@ -131,6 +134,9 @@
 =-iso : {n : Level } {x y : OD {suc n} } → (x == y) ≡ (ord→od (od→ord x) == y)
 =-iso {_} {_} {y} = cong ( λ k → k == y ) (sym oiso)
 
+=>-iso : {n : Level } {x y z : OD {suc n} } → (x == y) → def z (od→ord x ) → def z (od→ord y )
+=>-iso {n} {x} {y} {z} eq z>x = {!!}
+
 ord→== : {n : Level} →  { x y : OD {n} } → od→ord x ≡  od→ord y →  x == y
 ord→== {n} {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
    lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
@@ -266,24 +272,6 @@
 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 }) )) }
 
--- L∋ord : {n : Level} → (x :  Ordinal {suc n} ) → L (osuc x) ∋ ord→od x
--- L∋ord {n} record { lv = Zero ; ord = (Φ .0) } = {!!}
--- L∋ord {n} record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } = {!!}
--- L∋ord {n} record { lv = lv ; ord = (OSuc .(lv) ord₁) } = {!!}
-
---  X ⊆ OD → (P X ∩ OD ) ⊆ L (supP X) ∈  OD
-
-ord-of : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n} → Ordinal {suc n}
-ord-of {n} A x with def A x
-... | t = x
-
-supP : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n}
-supP A = sup-o ( ord-of A )
-
-L→P : {n : Level} → (A x : OD {suc n} ) → L {n}  (supP A) ∋ ZFSubset A x
-L→P {n} A x with sup-o< (ord-of A) {{!!}}
-... | lt = {!!}
-
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -350,20 +338,23 @@
          --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
          power→ A t P∋t {x} t∋x = proj1 lemma-s where
-              lemma-t : ZFSubset A {!!} ∋ csuc t
-              lemma-t = record { proj1 = {!!} ; proj2 = {!!} }
-              lemma-s : ZFSubset A {!!} ∋ x
-              lemma-s = {!!} -- transitive {!!} t∋x
-              lemma : od→ord (ZFSubset A (ord→od (od→ord (csuc t))) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
-              lemma = sup-o< {suc n} (  λ x → od→ord ( ZFSubset A (ord→od x ))) 
+              minsup :  OD
+              minsup =  csuc (ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) )
+              lemma-t : minsup ∋ t
+              lemma-t = o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) {!!} {!!} )) {!!} {!!} ) 
+              lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
+              lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) {!!} {!!} )
+              lemma-s | case1 eq = {!!}
+              lemma-s | case2 lt = {!!}
+              -- = {!!} -- transitive {!!} t∋x
          power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A  = {!!} where
+         power← A t t→A  = def-subst ( o<→c< lemma ) {!!} {!!} where
               lemma-eq :  ZFSubset A t == t
               eq→ lemma-eq {z} w = proj2 w 
               eq← lemma-eq {z} w = record { proj2 = w  ;
                  proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
               lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
-              lemma = sup-o< {suc n} (  λ x → od→ord ( ZFSubset A (ord→od x ))) 
+              lemma = sup-o<   
          union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z
          union-lemma-u {X} {z} U>z = lemma <-osuc where
              lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz