--- a/constructible-set.agda	Thu May 16 11:40:18 2019 +0900
+++ b/constructible-set.agda	Thu May 16 16:08:34 2019 +0900
@@ -129,13 +129,17 @@
 
 open ConstructibleSet
 
-_∋_  : (ConstructibleSet ) → (ConstructibleSet  ) → Set n
-a ∋ x  =  (α a ≡ α x)  ∨ ( α x o< α a )  
+_∋_  : (ConstructibleSet ) → (ConstructibleSet  ) → Set (suc n)
+a ∋ x  =  ((α a ≡ α x)  ∨ ( α x o< α a ))
+    ∧ constructible a ( α x )
+    
 
 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c
 -- transitiveness  a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c
 -- ... | t1 | t2 = {!!}
 
+open import Data.Unit
+
 ConstructibleSet→ZF : ZF {suc (suc n)} {suc (suc n)}
 ConstructibleSet→ZF   = record { 
     ZFSet = ConstructibleSet 
@@ -145,14 +149,19 @@
     ; _,_ = _,_
     ; Union = Union
     ; Power = {!!}
-    ; Select = {!!}
-    ; Replace = {!!}
+    ; Select = Select
+    ; Replace = Replace
     ; infinite = {!!}
     ; isZF = {!!}
  } where
-    Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc n)) → ConstructibleSet
-    Select X ψ = record { α = α X ; constructible = λ x → ( ψ (record { α = x ; constructible = λ x → constructible X x } ) ) }
+    conv : (ConstructibleSet → Set (suc (suc n))) → ConstructibleSet → Set (suc n)
+    conv ψ x with ψ x
+    ... | t =  Lift ( suc n ) ⊤
+    Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc (suc n))) → ConstructibleSet
+    Select X ψ = record { α = α X ; constructible = λ x → (conv ψ) (record { α = x ; constructible = λ x → constructible X x }  ) }
+    Replace : (X : ConstructibleSet) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
+    Replace X ψ  = record { α = α X ; constructible = λ x →  {!!}  }
     _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet
-    a , b  = Select {!!} {!!}
+    a , b  = record { α = maxα (α a) (α b) ; constructible = λ x → {!!} }
     Union : ConstructibleSet → ConstructibleSet
     Union a = {!!}