--- a/OD.agda	Sat Jul 18 18:11:13 2020 +0900
+++ b/OD.agda	Sun Jul 19 00:26:55 2020 +0900
@@ -103,6 +103,9 @@
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
+-- possible order restriction
+  ho< : {x : HOD} → od→ord x o< next (odmax x)
+
 
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
@@ -117,10 +120,6 @@
 odmaxmin : Set (suc n)
 odmaxmin = (y : HOD) (z : Ordinal) → ((x : Ordinal)→ def (od y) x → x o< z) → odmax y o< osuc z
 
--- possible order restriction
-hod-ord< :  {x : HOD } → Set n
-hod-ord< {x} =  od→ord x o< next (odmax x)
-
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
 ¬OD-order : ( od→ord : OD  → Ordinal ) → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
@@ -374,15 +373,15 @@
 -- This means that many of OD may not be HODs because of the od→ord mapping divergence.
 -- We should have some axioms to prevent this such as od→ord x o< next (odmax x).
 -- 
-postulate
-    ωmax : Ordinal
-    <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+-- postulate
+--     ωmax : Ordinal
+--     <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+-- 
+-- infinite : HOD 
+-- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
 
 infinite : HOD 
-infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
-
-infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 
-infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
+infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
     u : (y : Ordinal ) → HOD
     u y = Union (ord→od y , (ord→od y , ord→od y))
     --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
@@ -405,7 +404,7 @@
     lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
 
 ω<next-o∅ : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
-ω<next-o∅ ho< {y} lt = <odmax (infinite' ho<) lt
+ω<next-o∅ ho< {y} lt = <odmax infinite lt
 
 nat→ω : Nat → HOD
 nat→ω Zero = od∅
@@ -418,8 +417,10 @@
     lemma (isuc lt) = Suc (lemma lt)
 
 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
-ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ
-ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n}))
+ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
+ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
+    lemma :  od→ord (Union (ord→od (od→ord (nat→ω n)) , (ord→od (od→ord (nat→ω n)) , ord→od (od→ord (nat→ω n))))) ≡ od→ord (nat→ω (Suc n))
+    lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl
 
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y