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

diff -r 0a8b6bb9652c -r 905311ffe7ec src/generic-filter.agda
--- a/src/generic-filter.agda	Thu Mar 23 11:22:43 2023 +0900
+++ b/src/generic-filter.agda	Sun Mar 26 17:18:45 2023 +0900
@@ -177,7 +177,7 @@
 ----
 --  Generic Filter on L ⊆ Power P from HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. ℕ → P → Set )
 --
---  p 0 ≡ ∅
+--  p 0 ≡ p0
 --  p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q  (by axiom of choice) ( q =  * ( ctl→ n ) )
 ---             else p n
 
@@ -336,49 +336,37 @@
 --
 
 --
--- in D, we have V ≠ L
+-- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
+--
+--  We can define the valuation, but to use this, we need V=L, which makes things complicated.
 --
-
-val< : {x y p : Ordinal} → odef (* x) ( & < * y , * p >  ) → y o< x
-val< {x} {y} {p} xyp = osucprev ( begin
-    osuc y ≤⟨ osucc (odef< (subst (λ k → odef (* y , * y)  k) &iso (v00 _  _ ) )) ⟩
-    & (* y , * y) <⟨ c<→o< (v01 _ _)  ⟩
-    & < * y , * p > <⟨ odef< xyp ⟩
-    & (* x) ≡⟨ &iso ⟩
-    x ∎ ) where
-       v00 : (x y : HOD) → odef (x , y) (& x)
-       v00 _ _ = case1 refl
-       v01 : (x y : HOD) → < x , y > ∋ (x , x)
-       v01 _ _ = case1 refl
-       open o≤-Reasoning O
-
-record valS (G : HOD) (x z : Ordinal) (val : (y : Ordinal) → y o< x → HOD): Set n where
-   field
-     y p : Ordinal
-     G∋p : odef G p
-     is-val : odef (* x) ( & < * y , * p >  )
-     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 : HOD) →  (G : HOD) →  HOD
+-- val x G = TransFinite {λ x → HOD } ind (& x) where
+--   ind : (x : Ordinal) → (valy : (y : Ordinal) → y o< x → HOD) → HOD
+--   ind x valy = record { od = record { def = λ z → valS G x z  valy  } ; odmax = x ; <odmax = v02 } where
+--       v02 : {z : Ordinal} → valS G x z valy → z o< x
+--       v02 {z} lt = valS.z<x lt
 
 --
---   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
+-- What we nedd
+--   M[G] : HOD
+--     M ⊆ M[G]
+--     M[G] ∋ G
+--     M[G] ∋ ∪G
+--     L of M ≡ L of M[G]
+--     L is a countable subset of Power ω i.e. Power ω ∩ M
 --
-val : (x : HOD) →  (G : HOD) →  HOD
-val x G = TransFinite {λ x → HOD } ind (& x) where
-  ind : (x : Ordinal) → (valy : (y : Ordinal) → y o< x → HOD) → HOD
-  ind x valy = record { od = record { def = λ z → valS G x z  valy  } ; odmax = x ; <odmax = v02 } where
-      v02 : {z : Ordinal} → valS G x z valy → z o< x
-      v02 {z} lt = valS.z<x lt
+--  Generic Filter is a countable sequence of element of M
+--    Mg is set of all elementns of M which contains an element of G
+--
+--  Mg : HOD
+--  Mg 
+
+record Mg {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) (x : Ordinal) : Set n where
+    field
+       gi : Ordinal
+       G∋gi : odef (⊆-Ideal.ideal (genf G)) gi
+       x∋gi : odef (* x) gi
 
 TCS : (G : HOD) → Set (Level.suc n)
 TCS G = {x y : HOD} → G ∋ x → x ∋ y → G ∋ y
@@ -387,20 +375,3 @@
       → (C : CountableModel ) → HOD
 GH P L p0 LPP Lp0 C = ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))
 
--- M ∋ x ∧ val x G ∋ val y G → M ∋ y
-
-lemma233 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
-      → (C : CountableModel ) 
-      → {x y : HOD } → ctl-M C ∋ x
-      → val x (GH P L p0 LPP Lp0 C) ∋ val y (GH P L p0 LPP Lp0 C)
-      → ctl-M C ∋  y
-lemma233 P L p0 LPP Lp0 C {x} {y} Mx vx∋vy  = ? where
-    M = ctl-M C
-    G = ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))
-    pind :  (x : Ordinal) → ((z : Ordinal) →
-             z o< x → odef M z → odef (val (* z) G) (& (val y G)) → M ∋ y) →
-            odef M x → odef (val (* x) G) (& (val y G)) → M ∋ y
-    pind  x prev Mx vxvy = ?
-    lm00 : (x : Ordinal) → odef M x → odef (val (* x) G) (& (val y G)) → M ∋ y
-    lm00 x Mx vgvy = TransFinite0 {λ x → odef M x → odef (val (* x) G) (& (val y G)) → M ∋ y} pind x Mx vgvy
-