--- a/constructible-set.agda	Sun May 19 15:30:04 2019 +0900
+++ b/constructible-set.agda	Sun May 19 18:13:42 2019 +0900
@@ -190,8 +190,8 @@
 open import Data.Unit
 
 postulate      -- this is proved by Godel numbering of def
-   _c<_ : {n : Level } → (x y : OD {n} ) → Set n
-   ODpre : {n : Level} →  IsPreorder {suc n} {suc n} {n} _≡_ _c<_ 
+   _c<_ : {n : Level } → (x y : OD {n} ) → Set (suc n)
+   ODpre : {n : Level} →  IsPreorder {suc n} {suc n} {suc n} _≡_ _c<_ 
 
 -- o∋  : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
 -- o∋ a x x<A  = def a x x<A
@@ -207,10 +207,40 @@
 -- 
 --     u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
 --
---    HOD = {x | TC x ⊆ OD }  ⊆ OD
+-- Heritic Ordinal Definable
+--
+--    ( HOD = {x | TC x ⊆ OD } ) ⊆ OD
 -- 
 
-record HOD {n : Level}  : Set (suc n) where
-  field
-      hod : OD {n}
-      tc : ?
+HOD = OD
+
+c∅ : {n : Level} → HOD {n}
+c∅ {n} = record { α  = o∅ ; def = λ x y → Lift n ⊥ }
+
+HOD→ZF : {n : Level} → ZF {suc n} {suc n}
+HOD→ZF {n}  = record { 
+    ZFSet = HOD 
+    ; _∋_ = λ a b → b c< a
+    ; _≈_ = _≡_ 
+    ; ∅  = c∅
+    ; _,_ = _,_
+    ; Union = Union
+    ; Power = {!!}
+    ; Select = Select
+    ; Replace = Replace
+    ; infinite = {!!}
+    ; isZF = {!!}
+ } where
+    Select : (X : HOD {n}) → (HOD {n} → Set (suc n)) → HOD {n}
+    Select X ψ = record { α = α X ; def = λ x →  {!!} } where 
+       select : Ordinal → Set n
+       select x with  ψ (record { α = x ; def = λ x → {!!} })
+       ... | t = Lift n ⊤
+    Replace : (X : HOD {n} ) → (HOD → HOD) → HOD
+    Replace X ψ  = record { α = {!!} ; def = λ x → {!!} }  
+    _,_ : HOD {n} → HOD → HOD
+    a , b  = record { α = maxα (α a) (α b) ; def = λ x x<ab → (   ) }  where
+       a∨b : Ordinal {suc n} → Set n
+       a∨b = {!!}
+    Union : HOD → HOD
+    Union a = {!!}