# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557974418 -32400
# Node ID 47995eb521d4d6d5ce976381e1aff36f4da19230
# Parent  627a79e6111672c69e3ac20fddea683ef0db109d
...

diff -r 627a79e61116 -r 47995eb521d4 constructible-set.agda
--- a/constructible-set.agda	Thu May 16 10:55:34 2019 +0900
+++ b/constructible-set.agda	Thu May 16 11:40:18 2019 +0900
@@ -122,10 +122,10 @@
 
 -- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
 
-record ConstructibleSet  : Set (suc n) where
+record ConstructibleSet  : Set (suc (suc n)) where
   field
     α : Ordinal
-    constructible : Ordinal  → Set n 
+    constructible : Ordinal  → Set (suc n)
 
 open ConstructibleSet
 
@@ -136,22 +136,22 @@
 -- transitiveness  a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c
 -- ... | t1 | t2 = {!!}
 
-ConstructibleSet→ZF : ZF {suc n} {suc n}
+ConstructibleSet→ZF : ZF {suc (suc n)} {suc (suc n)}
 ConstructibleSet→ZF   = record { 
     ZFSet = ConstructibleSet 
-    ; _∋_ = λ a b → Lift (suc n) ( a ∋ b )
+    ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b )
     ; _≈_ = _≡_ 
-    ; ∅  = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift n ⊥ }
+    ; ∅  = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift (suc n) ⊥ }
     ; _,_ = _,_
     ; Union = Union
     ; Power = {!!}
-    ; Select = Select
+    ; Select = {!!}
     ; Replace = {!!}
     ; infinite = {!!}
     ; isZF = {!!}
  } where
     Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc n)) → ConstructibleSet
-    Select = {!!}
+    Select X ψ = record { α = α X ; constructible = λ x → ( ψ (record { α = x ; constructible = λ x → constructible X x } ) ) }
     _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet
     a , b  = Select {!!} {!!}
     Union : ConstructibleSet → ConstructibleSet