# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1679538163 -32400
# Node ID 0a8b6bb9652c95e731f76d01512965840c3426dd
# Parent  5bf3923b818b7b3b9377eaa44bc4d93a4add193f
...

diff -r 5bf3923b818b -r 0a8b6bb9652c src/generic-filter.agda
--- 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 > }
 --