Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/generic-filter.agda @ 437:2b5d2072e1af
val
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 22 Feb 2022 23:37:07 +0900 |
parents | 87b5303ceeb5 |
children | 50949196aa88 |
line wrap: on
line diff
--- 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 }