--- a/constructible-set.agda	Sat May 18 16:03:10 2019 +0900
+++ b/constructible-set.agda	Sat May 18 16:28:10 2019 +0900
@@ -182,11 +182,12 @@
 c∅ : {n : Level} → ConstructibleSet
 c∅ {n} = record {α = o∅ ; constructible = λ x → Lift n ⊥ }
 
-record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m  ) (ψ : S → S ) (X : S) : Set (n ⊔ m)  where
+record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m  ) (ψ : S → S ) (X : S) : Set ((suc n) ⊔ m)  where
   field
     sup : S
     smax  : ∀ { x : S } → x ≤ X  → ψ x ≤ sup 
     suniq : {max : S} → ( ∀ { x :  S } → x ≤ X  → ψ x ≤ max ) → max ≤ sup 
+    repl : ( x : Ordinal {n} ) → Set n
 
 open SupR
 
@@ -200,6 +201,7 @@
 sup  (Sup {n} ψ X ) = suptraverse X (c∅ {n}) ψ 
 smax (Sup ψ X ) = {!!} 
 suniq (Sup ψ X ) = {!!}
+repl (Sup ψ X ) = {!!}
      
 open import Data.Unit
 open SupR
@@ -214,25 +216,26 @@
     ; Union = Union
     ; Power = {!!}
     ; Select = Select
-    ; Replace = {!!}
+    ; Replace = Replace
     ; infinite = {!!}
     ; isZF = {!!}
  } where
-    conv : {n : Level} → (ConstructibleSet {n} → Set (suc (suc n))) → ConstructibleSet → Set (suc n)
-    conv {n} ψ x with ψ x
-    ... | t =  Lift ( suc n ) ⊤
     Select : (X : ConstructibleSet {n}) → (ConstructibleSet  {n} → Set (suc n)) → ConstructibleSet {n}
-    Select X ψ = record { α = α X ; constructible = λ x →  {!!} } -- ψ (record { α = x ; constructible = λ x → constructible X x }  ) }
+    Select X ψ = record { α = α X ; constructible = λ x →  select x } where 
+       select : Ordinal → Set n
+       select x with  ψ (record { α = x ; constructible = λ x → constructible X x })
+       ... | t = Lift n ⊤
     Replace : (X : ConstructibleSet {n} ) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
-    Replace X ψ  = record { α = α (sup supψ)  ; constructible = λ x →  {!!}   }  where
-          supψ : SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
-          supψ = Sup ψ X
-          repl : Ordinal {n} → Set (suc n)
-          repl x = {!!}
-    conv1 : (Ordinal {n} → Set n) → Ordinal {n} → Set n
-    conv1 ψ x with ψ 
-    ... | t =  Lift  n ⊤
+    Replace X ψ  = record { α = α (sup supψ)  ; constructible = λ x → repl1 x }  where
+       supψ : SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
+       supψ = Sup ψ X
+       repl1 : Ordinal {suc n} → Set n
+       repl1 x with repl supψ x
+       ... | t = Lift n  ⊤
     _,_ : ConstructibleSet {n} → ConstructibleSet → ConstructibleSet
-    a , b  = record { α = maxα (α a) (α b) ; constructible = λ x → {!!} } -- ((x ≡ α a ) ∨ ( x ≡ α b )) }
+    a , b  = record { α = maxα (α a) (α b) ; constructible =  a∨b }  where
+       a∨b : Ordinal {suc n} → Set n
+       a∨b x with (x ≡ α a ) ∨ ( x ≡ α b )
+       ... | t = Lift n  ⊤
     Union : ConstructibleSet → ConstructibleSet
     Union a = {!!}