--- a/src/generic-filter.agda	Wed Mar 22 12:48:06 2023 +0900
+++ b/src/generic-filter.agda	Thu Mar 23 11:22:43 2023 +0900
@@ -360,6 +360,16 @@
      z=valy : z ≡ & (val y (val< is-val))
      z<x : z o< x
 
+record valT (G : HOD) (z : Ordinal) : Set n where
+   field
+     val : Ordinal → Ordinal
+     is-val : {x y p : Ordinal } → x o< z → odef G p → odef (* x) (& ( < * y , * p > )) → odef (* (val x)) (val y)
+
+valZ : (G M : HOD) → valT G (& M)
+valZ G M = TransFinite0 {λ x → valT G x} pind (& M) where
+   pind : (x : Ordinal) → ((y : Ordinal) → y o< x → valT G y) → valT G x
+   pind x prev = record { val = ? ; is-val = ? }
+
 --
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --