--- a/src/generic-filter.agda	Tue Feb 22 22:08:44 2022 +0900
+++ b/src/generic-filter.agda	Tue Feb 22 23:37:07 2022 +0900
@@ -207,18 +207,23 @@
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
 
+record valR (x : HOD) {P : HOD} (G : GenericFilter P) : Set (suc n) where
+   field
+     valx : HOD
 
-record valR (x y P : HOD) (G : GenericFilter P) : Set (suc n) where
+record valS (ox oy oG : Ordinal) : Set n where
    field
-     p : HOD
-     p∈G : filter (genf G) ∋ p 
-     is-val : x ∋ < y , p > 
+     op : Ordinal
+     p∈G : odef (* oG) op 
+     is-val : odef (* ox) ( & < * oy , * op >  )
 
-val : (x : HOD) (P : HOD ) 
+val : (x : HOD) {P : HOD }
     →  (G : GenericFilter P)
     →  HOD
-val x P G = record { od = record { odef = ε-induction { λ y → (z : Ordinal) → odef y (& z) → {!!}  } (λ {z} Prev → {!!} ) }
-    ; odmax = {!!} ; <odmax = {!!} }
+val x G = TransFinite {λ x → HOD } ind (& x) where
+  ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
+  ind x valy = {!!}
+
 
 --
 --   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }

--- a/src/zf.agda	Tue Feb 22 22:08:44 2022 +0900
+++ b/src/zf.agda	Tue Feb 22 23:37:07 2022 +0900
@@ -49,7 +49,7 @@
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
      -- regularity without minimum
-     ε-induction : { ψ : ZFSet → Set (suc m)}
+     ε-induction : { ψ : ZFSet → Set (suc m Level.⊔ n)}
               → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
               → (x : ZFSet ) → ψ x
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )