--- a/HOD.agda	Mon Jul 08 19:35:23 2019 +0900
+++ b/HOD.agda	Mon Jul 08 19:45:59 2019 +0900
@@ -163,13 +163,7 @@
          t : (od→ord x) o< (od→ord a)
          t = c<→o< {suc n} {x} {a} lt 
 
-o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
-o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
-o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
-    lemma :  o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
-    lemma lt = {!!}
-o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
-o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
+-- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
 
 o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
@@ -201,11 +195,8 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
-csuc :  {n : Level} →  OD {suc n} → OD {suc n}
-csuc x = Ord ( osuc ( od→ord x ))
-
 in-codomain : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n}
-in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))  }
+in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
 
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
@@ -342,9 +333,9 @@
          replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
              lemma : def (in-codomain X ψ) (od→ord (ψ x))
              lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
-                 (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso {!!} )) } ))
+                 {!!} } ))
          replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+         replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where
             lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
                     → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
             lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
@@ -451,7 +442,7 @@
                   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 = lemma4 }) ) where
+              lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = {!!} }) ) where
 
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Todo	Mon Jul 08 19:45:59 2019 +0900
@@ -0,0 +1,6 @@
+Mon Jul  8 19:43:37 JST 2019
+
+    ordinal-definable.agda assumes all ZF Set are ordinals, that it too restrictive
+
+    remove ord-Ord  and prove with some assuption in HOD.agda
+        union, power set, replace, inifinite