# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678589935 -32400
# Node ID 5223f0b40d91be87b0daf1fde779599c3d6cbe7b
# Parent  01fe64d3a17a4756d16e908ad09cd0aad5fd207b
...

diff -r 01fe64d3a17a -r 5223f0b40d91 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Thu Mar 09 12:31:32 2023 +0900
+++ b/src/Tychonoff.agda	Sun Mar 12 11:58:55 2023 +0900
@@ -172,7 +172,7 @@
           fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz)
      --
      -- then we have maximum ultra filter ( Zorn lemma )
-     --    to debug this file, commet out to include maaximum filter
+     --    to debug this file, commet out the maximum filter and open import
      --    otherwise the check requires a minute
      --
      maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
diff -r 01fe64d3a17a -r 5223f0b40d91 src/filter.agda
--- a/src/filter.agda	Thu Mar 09 12:31:32 2023 +0900
+++ b/src/filter.agda	Sun Mar 12 11:58:55 2023 +0900
@@ -151,14 +151,6 @@
         lemma : (p : HOD) → p ⊆ P   →  filter F ∋ (p ∪ (P ＼ p))
         lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P 
 
-record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
-   field
-       dense : HOD
-       d⊆P :  dense ⊆ L
-       dense-f : {p : HOD} → L ∋ p  → HOD
-       dense-d :  { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
-       dense-p :  { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p  
-
 record Ideal   {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where
    field
        ideal : HOD   
@@ -176,11 +168,6 @@
 
 open import Relation.Binary.Definitions
 
-record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where
-    field
-       genf : Filter {L} {P} LP
-       generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
-
 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) (F : Filter {L} {P} LP) : Set (suc n) where
     field
        mf : Filter {L} {P} LP
diff -r 01fe64d3a17a -r 5223f0b40d91 src/generic-filter.agda
--- a/src/generic-filter.agda	Thu Mar 09 12:31:32 2023 +0900
+++ b/src/generic-filter.agda	Sun Mar 12 11:58:55 2023 +0900
@@ -74,15 +74,15 @@
 
 ----
 --   a(n) ∈ M
---   ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ q ⊆ p(n)    
+--   ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ p(n) ⊆ q
 --
 PGHOD :  (i : Nat) (L : HOD) (C : CountableModel ) → (p : Ordinal) → HOD
 PGHOD i L C p = record { od = record { def = λ x  →
-       odef L x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* x) y →  odef (* p) y ) }
+       odef L x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
    ; odmax = odmax L  ; <odmax = λ {y} lt → <odmax L (proj1 lt) }  
 
 ---
---   p(n+1) = if ({q | q ∈ a(n) ∧ q ⊆ p(n))} != ∅ then q otherwise p(n)
+--   p(n+1) = if ({q | q ∈ a(n) ∧ p(n) ⊆ q)} != ∅ then q otherwise p(n)
 --  
 find-p :  (L : HOD ) (C : CountableModel )  (i : Nat) → (x : Ordinal) → Ordinal
 find-p L C Zero x = x
@@ -91,12 +91,12 @@
 ... | no not  = & (ODC.minimal O ( PGHOD i L C (find-p L C i x)) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
 
 ---
--- G = { r ∈ L ⊆ Power P | ∃ n → p(n) ⊆ r }
+-- G = { r ∈ L ⊆ Power P | ∃ n → r ⊆ p(n) }
 --
 record PDN  (L p : HOD ) (C : CountableModel )  (x : Ordinal) : Set n where
    field
        gr : Nat
-       pn<gr : (y : Ordinal) → odef (* (find-p L C gr (& p))) y → odef (* x) y 
+       pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p L C gr (& p))) y 
        x∈PP  : odef L x
 
 open PDN
@@ -130,7 +130,7 @@
 p-monotonic1 :  (L p : HOD ) (C : CountableModel  ) → {n : Nat} → (* (find-p L C (Suc n) (& p))) ⊆ (* (find-p L C n (& p)))
 p-monotonic1 L p C {n} {x} with is-o∅ (& (PGHOD n L C (find-p L C n (& p))))
 ... | yes y =  refl-⊆ {* (find-p L C n (& p))}
-... | no not = λ  lt →   proj2 (proj2 fmin∈PGHOD) _ lt   where
+... | no not = ? where -- λ  lt →   proj2 (proj2 fmin∈PGHOD) _ ?   where
     fmin : HOD
     fmin = ODC.minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
     fmin∈PGHOD : PGHOD n L C (find-p L C n (& p)) ∋ fmin
@@ -144,85 +144,40 @@
 ... | tri≈ ¬a refl ¬c = λ x → x
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
+record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
+   field
+       dense : HOD
+       d⊆P :  dense ⊆ L
+       dense-f : {p : HOD} → L ∋ p  → HOD
+       dense-d :  { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
+       dense-p :  { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p  
+
+record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where
+    field
+       genf : Filter {L} {P} LP
+       generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Replace (Filter.filter genf) (λ x → P ＼ x )) ≡ od∅ )
+    rgen : HOD
+    rgen = Replace (Filter.filter genf) (λ x → P ＼ x )
+
 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
 P-GenericFilter P L p0 L⊆PP Lp0 C = record {
-      genf = record { filter = PDHOD L p0 C ; f⊆L =  f⊆PL ; filter1 = λ L∋q PD∋p p⊆q → f1 L∋q PD∋p p⊆q ; filter2 = f2 }
-    ; generic = fdense
+      genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x)  ; f⊆L =  ? ; filter1 = ? ; filter2 = ? }
+    ; generic = ?
    } where
         f⊆PL :  PDHOD L p0 C ⊆ L 
         f⊆PL lt = x∈PP lt  
         f1 : {p q : HOD} → L ∋  q → PDHOD L p0 C ∋ p → p ⊆ q → PDHOD L p0 C ∋ q
-        f1 {p} {q} L∋q PD∋p p⊆q =  record { gr = gr PD∋p ;  pn<gr = f04 ; x∈PP = L∋q } where
-           f04 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (* (& q)) y
-           f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y lt1 )))
-               -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
-        f2 : {p q : HOD} → PDHOD L p0 C ∋ p → PDHOD L p0 C ∋ q → L ∋ (p ∩ q) → PDHOD L p0 C ∋ (p ∩ q)
+        f1 {p} {q} L∋q PD∋p p⊆q =  ?
+        f2 : {p q : HOD} → ? ∋ p → ? ∋ q → L ∋ (p ∩ q) → ? ∋ (p ∩ q)
         f2 {p} {q} PD∋p PD∋q L∋pq with <-cmp (gr PD∋q) (gr PD∋p)
-        ... | tri< a ¬b ¬c = record { gr = gr PD∋p ;  pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt ) ; x∈PP = L∋pq } where
-            f3 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
-            f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y (f5 lt)) ⟫ where
-               f5 : odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (* (find-p L C (gr PD∋q) (& p0))) y
-               f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋q) (& p0))) k ) &iso ( (p-monotonic L p0 C {gr PD∋q} {gr PD∋p} (<to≤ a))
-                   (subst (λ k → odef (* (find-p L C (gr PD∋p) (& p0))) k ) (sym &iso) lt) )
-        ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ;  pn<gr =  λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt) ; x∈PP = L∋pq } where
-            f4 : (y : Ordinal) → odef (* (find-p L C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
-            f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ 
-        ... | tri> ¬a ¬b c = record { gr = gr PD∋q ;  pn<gr =  λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt) ; x∈PP = L∋pq } where 
-            f3 : (y : Ordinal) → odef (* (find-p L C (gr PD∋q) (& p0))) y → odef (p ∩ q) y
-            f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y (f5 lt)), subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ where
-               f5 : odef (* (find-p L C (gr PD∋q) (& p0))) y → odef (* (find-p L C (gr PD∋p) (& p0))) y
-               f5 lt = subst (λ k → odef (* (find-p L C (gr PD∋p) (& p0))) k ) &iso ( (p-monotonic L p0 C {gr PD∋p} {gr PD∋q} (<to≤ c))
-                   (subst (λ k → odef (* (find-p L C (gr PD∋q) (& p0))) k ) (sym &iso) lt) )
-        fdense : (D : Dense L⊆PP ) → (ctl-M C ) ∋ Dense.dense D  → ¬ (filter.Dense.dense D ∩ PDHOD L p0 C) ≡ od∅
-        fdense D MD eq0  = ⊥-elim (  ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a eq ¬c = ?
+        ... | tri> ¬a ¬b c = ? 
+        gf : HOD
+        gf  = Replace (Replace (PDHOD L p0 C) (λ x → P ＼ x)) (_＼_ P)
+        fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D  → ¬ (Dense.dense D ∩ gf ) ≡ od∅
+        fdense D MD eq0  = ? where
            open Dense
-           fd09 : (i : Nat ) → odef L (find-p L C i (& p0))
-           fd09 Zero = Lp0
-           fd09 (Suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
-           ... | yes _ = fd09 i
-           ... | no not = fd17 where
-              fd19 =  ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))  
-              fd18 : PGHOD i L C (find-p L C i (& p0)) ∋ fd19
-              fd18 = ODC.x∋minimal O (PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))
-              fd17 :  odef L ( & (ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)))  )
-              fd17 = proj1 fd18 
-           an :  Nat
-           an = ctl← C (& (dense D)) MD  
-           pn : Ordinal
-           pn = find-p L C an (& p0)
-           pn+1 : Ordinal
-           pn+1 = find-p L C (Suc an) (& p0)
-           d=an : dense D ≡ * (ctl→ C an) 
-           d=an = begin dense D ≡⟨ sym *iso ⟩
-                    * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→  C MD )) ⟩
-                    * (ctl→ C an) ∎  where open ≡-Reasoning
-           fd07 : odef (dense D) pn+1
-           fd07 with is-o∅ ( & ( PGHOD an L C (find-p L C an (& p0))) )
-           ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 ⟪ fd13 , ⟪ fd14 , fd15 ⟫ ⟫ ) ) where
-              fd12 : L ∋ * (find-p L C an (& p0))
-              fd12 = subst (λ k → odef L k) (sym &iso) (fd09 an )
-              fd11 : Ordinal
-              fd11 = & ( dense-f D fd12 )
-              fd13 : L ∋ ( dense-f D fd12 )
-              fd13 = (d⊆P D) (  dense-d D fd12 )
-              fd14 : (* (ctl→ C an)) ∋ ( dense-f D fd12 )
-              fd14 = subst (λ k → odef k (& ( dense-f D fd12 ) )) d=an (  dense-d D fd12 ) 
-              fd15 :  (y : Ordinal) → odef (* (& (dense-f D fd12))) y → odef (* (find-p L C an (& p0))) y
-              fd15 y lt = subst (λ k → odef  (* (find-p L C an (& p0)))  k ) &iso ( (dense-p D  fd12 ) fd16  ) where
-                  fd16 : odef (dense-f D fd12) (& ( * y))
-                  fd16 = subst₂ (λ j k → odef j k ) (*iso) (sym &iso) lt
-              fd10 :  PGHOD an L C (find-p L C an (& p0)) =h= od∅
-              fd10 = ≡o∅→=od∅ y
-           ... | no not = fd27 where
-              fd29 =  ODC.minimal O ( PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq))
-              fd28 : PGHOD an L C (find-p L C an (& p0)) ∋ fd29
-              fd28 = ODC.x∋minimal O (PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq))
-              fd27 :  odef (dense D) (& fd29)
-              fd27 = subst (λ k → odef k (& fd29)) (sym d=an) (proj1 (proj2 fd28)) 
-           fd03 : odef (PDHOD L p0 C) pn+1
-           fd03 = record { gr = Suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (Suc an)} 
-           fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1)
-           fd01 = ⟪ subst (λ k → odef (dense D)  k ) (sym &iso) fd07 , subst (λ k → odef  (PDHOD L p0 C) k) (sym &iso) fd03 ⟫  
 
 open GenericFilter
 open Filter
@@ -236,7 +191,7 @@
 lemma232 : (P L p : HOD ) (C : CountableModel ) 
     →  (LP : L ⊆ Power P ) →  (Lp0 : L ∋ p  )
     →  ( {q : HOD} → (Lq : L ∋ q ) → NonAtomic L q Lq )
-    →  ¬ ( (ctl-M C) ∋ filter ( genf ( P-GenericFilter P L p LP Lp0  C )) )
+    →  ¬ ( (ctl-M C) ∋  rgen ( P-GenericFilter P L p LP Lp0  C )) 
 lemma232 P L p C LP Lp0 NA MG = {!!} where
     D : HOD  -- P - G
     D = ?