# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1647502854 -32400
# Node ID 5f8243d1d41ba465b7de9b0be87dd1e5750a3c37
# Parent  9207b0c3cfe9f2427a506b9f93e85f32196300d2
...

diff -r 9207b0c3cfe9 -r 5f8243d1d41b src/filter.agda
--- a/src/filter.agda	Thu Mar 17 15:36:24 2022 +0900
+++ b/src/filter.agda	Thu Mar 17 16:40:54 2022 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+
 open import Level
 open import Ordinals
 module filter {n : Level } (O : Ordinals {n})   where
@@ -59,7 +61,7 @@
 open _⊆_
 
 ∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p 
-∈-filter {L} {p} F lt = {!!} -- power→⊆ L p ( incl ? lt )
+∈-filter {L} {p} F lt = incl ( f⊆L F) lt 
 
 ∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
@@ -67,6 +69,12 @@
 ∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
 
+∪-lemma3 : {L P p q : HOD } → L ⊆ Power P → L ∋ (p ∪ q)  → L ∋ p
+∪-lemma3 = {!!}
+
+∪-lemma4 : {L P p q : HOD } →  L ⊆ Power P →  L ∋ (p ∪ q)  → L ∋ q
+∪-lemma4 = {!!}
+
 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
@@ -83,8 +91,8 @@
        ; prime = lemma3
     } where
   lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
-  lemma3 {p} {q} lt with ultra-filter.ultra u {!!} -- (∪-lemma1 (∈-filter P lt) )
-  ... | case1 p∈P  = case1 p∈P
+  lemma3 {p} {q} lt with ultra-filter.ultra u (∈-filter F lt) 
+  ... | case1 p∈P  = case1 {!!} -- (∪-lemma3 (ultra-filter.L⊆PP u) ? ) --  : OD.def (od (filter F)) (& p)
   ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where
     lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
     lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
@@ -95,7 +103,7 @@
          lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
          lemma4 x lt | case2 qx = qx
     lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
-    lemma6 = filter2 F lt ¬p∈P
+    lemma6 = {!!} -- filter2 F lt ¬p∈P
     lemma7 : filter F ∋ (q ∩ (L ＼ p))
     lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!}
     lemma8 : (q ∩ (L ＼ p)) ⊆ q
diff -r 9207b0c3cfe9 -r 5f8243d1d41b src/generic-filter.agda
--- a/src/generic-filter.agda	Thu Mar 17 15:36:24 2022 +0900
+++ b/src/generic-filter.agda	Thu Mar 17 16:40:54 2022 +0900
@@ -67,45 +67,45 @@
 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
 -- 
 
--- we expect  P ∈ * ctl-M ∧ G  ⊆ Power P  , ¬ G ∈ * ctl-M, 
+-- we expect  P ∈ * ctl-M ∧ G  ⊆ L ⊆ Power P  , ¬ G ∈ * ctl-M, 
 
 open CountableModel 
 
 ----
 --   a(n) ∈ M
---   ∃ q ∈ Power P → q ∈ a(n) ∧ q ⊆ p(n)    
+--   ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ q ⊆ p(n)    
 --
-PGHOD :  (i : Nat) (P : HOD) (C : CountableModel ) → (p : Ordinal) → HOD
-PGHOD i P C p = record { od = record { def = λ x  →
-       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* x) y →  odef (* p) y ) }
-   ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  
+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 ) }
+   ; odmax = odmax L  ; <odmax = λ {y} lt → <odmax L (proj1 lt) }  
 
 ---
 --   p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
 --  
-find-p :  (P : HOD ) (C : CountableModel )  (i : Nat) → (x : Ordinal) → Ordinal
-find-p P C Zero x = x
-find-p P C (Suc i) x with is-o∅ ( & ( PGHOD i P C (find-p P C i x)) )
-... | yes y  = find-p P C i x
-... | no not  = & (ODC.minimal O ( PGHOD i P C (find-p P C i x)) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
+find-p :  (L : HOD ) (C : CountableModel )  (i : Nat) → (x : Ordinal) → Ordinal
+find-p L C Zero x = x
+find-p L C (Suc i) x with is-o∅ ( & ( PGHOD i L C (find-p L C i x)) )
+... | yes y  = find-p L C i x
+... | 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 ∈ Power P | ∃ n → p(n) ⊆ r }
+-- G = { r ∈ L ⊆ Power P | ∃ n → p(n) ⊆ r }
 --
-record PDN  (P p : HOD ) (C : CountableModel )  (x : Ordinal) : Set n where
+record PDN  (L p : HOD ) (C : CountableModel )  (x : Ordinal) : Set n where
    field
        gr : Nat
-       pn<gr : (y : Ordinal) → odef (* (find-p P C gr (& p))) y → odef (* x) y 
-       x∈PP  : odef (Power P) x
+       pn<gr : (y : Ordinal) → odef (* (find-p L C gr (& p))) y → odef (* x) y 
+       x∈PP  : odef L x
 
 open PDN
 
 ---
 -- G as a HOD
 --
-PDHOD :  (P p : HOD ) (C : CountableModel  ) → HOD
-PDHOD P p C  = record { od = record { def = λ x →  PDN P p C x }
-    ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  } 
+PDHOD :  (L p : HOD ) (C : CountableModel  ) → HOD
+PDHOD L p C  = record { od = record { def = λ x →  PDN L p C x }
+    ; odmax = odmax L ; <odmax = λ {y} lt → <odmax L {y} (PDN.x∈PP lt)  } 
 
 open PDN
 
@@ -127,49 +127,54 @@
 open import nat
 open _⊆_
 
-p-monotonic1 :  (P p : HOD ) (C : CountableModel  ) → {n : Nat} → (* (find-p P C (Suc n) (& p))) ⊆ (* (find-p P C n (& p)))
-p-monotonic1 P p C {n} with is-o∅ (& (PGHOD n P C (find-p P C n (& p))))
+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} with is-o∅ (& (PGHOD n L C (find-p L C n (& p))))
 ... | yes y =   refl-⊆
 ... | no not = record { incl = λ {x} lt → proj2 (proj2 fmin∈PGHOD) (& x) lt  } where
     fmin : HOD
-    fmin = ODC.minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
-    fmin∈PGHOD : PGHOD n P C (find-p P C n (& p)) ∋ fmin
-    fmin∈PGHOD = ODC.x∋minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
+    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
+    fmin∈PGHOD = ODC.x∋minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
 
-p-monotonic :  (P p : HOD ) (C : CountableModel  ) → {n m : Nat} → n ≤ m → (* (find-p P C m (& p))) ⊆ (* (find-p P C n (& p)))
-p-monotonic P p C {Zero} {Zero} n≤m = refl-⊆
-p-monotonic P p C {Zero} {Suc m} z≤n = trans-⊆ (p-monotonic1 P p C {m} )  (p-monotonic P p C {Zero} {m} z≤n ) 
-p-monotonic P p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m
-... | tri< a ¬b ¬c = trans-⊆ (p-monotonic1 P p C {m}) (p-monotonic P p C {Suc n} {m} a)   
+p-monotonic :  (L p : HOD ) (C : CountableModel  ) → {n m : Nat} → n ≤ m → (* (find-p L C m (& p))) ⊆ (* (find-p L C n (& p)))
+p-monotonic L p C {Zero} {Zero} n≤m = refl-⊆
+p-monotonic L p C {Zero} {Suc m} z≤n = trans-⊆ (p-monotonic1 L p C {m} )  (p-monotonic L p C {Zero} {m} z≤n ) 
+p-monotonic L p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m
+... | tri< a ¬b ¬c = trans-⊆ (p-monotonic1 L p C {m}) (p-monotonic L p C {Suc n} {m} a)   
 ... | tri≈ ¬a refl ¬c = refl-⊆
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
-P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel ) → GenericFilter P
-P-GenericFilter P p0 Pp0 C = record {
-      genf = record { filter = PDHOD P p0 C ; f⊆PL =  f⊆PL ; filter1 = f1 ; filter2 = f2 }
-    ; generic = fdense
+P-GenericFilter : (P L p0 : HOD ) → L ⊆ Power P → L ∋ p0 → (C : CountableModel ) → GenericFilter L
+P-GenericFilter P L p0 L⊆PP Lp0 C = record {
+      genf = record { filter = PDHOD L p0 C ; f⊆PL =  f⊆PL ; filter1 = {!!} ; filter2 = {!!}  }
+    ; generic = {!!}
    } where
-        PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  PGHOD i P C x ⊆ Power P
-        PGHOD∈PL i x = record { incl = λ {x} p → proj1 p }
-        f⊆PL :  PDHOD P p0 C ⊆ Power P
-        f⊆PL = record { incl = λ {x} lt →  x∈PP lt  }
+        PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  PGHOD i L C x ⊆ Power P
+        PGHOD∈PL i x = record { incl = λ {x} p → {!!}  }
+        Pp0 : p0 ∈ Power P
+        Pp0 = {!!}
+        f⊆PL :  PDHOD L p0 C ⊆ Power P
+        f⊆PL = record { incl = λ {x} lt →  {!!} } -- x∈PP lt  }
         f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q
-        f1 {p} {q}  q⊆P PD∋p p⊆q =  record { gr = gr PD∋p ;  pn<gr = f04 ; x∈PP = power←  _ _ (incl q⊆P) } where
+        f1 {p} {q}  q⊆P PD∋p p⊆q =  record { gr = gr PD∋p ;  pn<gr = f04 ; x∈PP = {!!} } where -- power←  _ _ (incl q⊆P) } where
            f04 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
            f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (incl 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 P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q)
         f2 {p} {q} PD∋p PD∋q 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 = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
+        ... | 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 = {!!} } where
+                -- ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
             f3 : (y : Ordinal) → odef (* (find-p P 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 P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y
                f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋q} {gr PD∋p} (<to≤ a))
                    (subst (λ k → odef (* (find-p P 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 = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
+        ... | 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 = {!!} } where
+               -- ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
             f4 : (y : Ordinal) → odef (* (find-p P 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 = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   } where
+        ... | 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 = {!!} } where --
+           -- ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   } where
             f3 : (y : Ordinal) → odef (* (find-p P 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 P C (gr PD∋q) (& p0))) y → odef (* (find-p P C (gr PD∋p) (& p0))) y
@@ -178,16 +183,16 @@
         fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
         fdense D eq0  = ⊥-elim (  ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where
            open Dense
-           p0⊆P : p0 ⊆ P
-           p0⊆P = ODC.power→⊆ O _ _ Pp0
+           p0⊆P : P ∋ p0 
+           p0⊆P = {!!}
            fd : HOD
            fd = dense-f D p0⊆P
            PP∋D : dense D ⊆ Power P
-           PP∋D = d⊆P D
+           PP∋D = {!!} 
            fd00 : PDHOD P p0 C ∋ p0
-           fd00 = record { gr = 0 ; pn<gr = λ y lt → lt ; x∈PP = Pp0 }
-           fd02 : dense D ∋ dense-f D p0⊆P
-           fd02 = dense-d D p0⊆P
+           fd00 = record { gr = 0 ; pn<gr = λ y lt → lt ; x∈PP = {!!}  }
+           fd02 : dense D ∋ dense-f D {!!} -- p0⊆P
+           fd02 = dense-d D {!!}
            fd04 : dense-f D p0⊆P ⊆ P
            fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
            fd03 : PDHOD P p0 C  ∋ dense-f D p0⊆P
@@ -211,11 +216,11 @@
 lemma725 : (P p : HOD ) (C : CountableModel ) 
     →  (PP∋p : Power P ∋ p )
     →  * (ctl-M C) ∋ (Power P ∩  * (ctl-M C))                -- M is a Model of ZF
-    →  * (ctl-M C) ∋ ( (Power P ∩  * (ctl-M C))  ＼ filter ( genf ( P-GenericFilter P p PP∋p C)) )      -- M ∋ G and M is a Model of ZF 
+    →  * (ctl-M C) ∋ {!!} -- ( (Power P ∩  * (ctl-M C))  ＼ filter ( genf ( P-GenericFilter P ? p ?  C ? )) )      -- M ∋ G and M is a Model of ZF 
     →  ((p : HOD) → (PP∋p : p  ⊆ P ) → Incompatible P p PP∋p )
-    → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p PP∋p C )))
+    → ¬ ( * (ctl-M C) ∋ filter {!!} ) -- ( genf ( P-GenericFilter P ? ? p PP∋p C )))
 lemma725 P p C PP∋p M∋PM M∋D I M∋G = D∩G≠∅ D∩G=∅ where
-    G = filter ( genf ( P-GenericFilter P p PP∋p C ))
+    G = filter ( genf ( P-GenericFilter P {!!} p {!!} {!!} C ))
     M = * (ctl-M C)
     D : HOD
     D = Power P ＼ G
@@ -244,15 +249,15 @@
     D-Dense : Dense P
     D-Dense = record {
            dense = D
-       ;   d⊆P = record { incl = λ {x} lt → proj1 lt }
-       ;   dense-f = df
-       ;   dense-d = df-d
+       ;   d⊆P = record { incl = λ {x} lt → {!!} }
+       ;   dense-f = {!!}
+       ;   dense-d = {!!}
        ;   dense-p = {!!}
      }
     D∩G=∅ : ( D ∩ G ) =h= od∅ 
     D∩G=∅ = ≡od∅→=od∅ ([a-b]∩b=0 {Power P} {G})
     D∩G≠∅ : ¬ (( D ∩ G ) =h= od∅ )
-    D∩G≠∅ eq = generic (P-GenericFilter P p PP∋p C) D-Dense ( ==→o≡ eq )
+    D∩G≠∅ eq = generic (P-GenericFilter P {!!} {!!} {!!} {!!} C) D-Dense ( ==→o≡ eq )
 
 open import PFOD O
 
@@ -265,7 +270,7 @@
 lemma725-1 = {!!}
 
 lemma726 :  (C : CountableModel ) 
-    →  Union ( Replace' (Power (ω→2 ＼ HODω2)) (λ p lt → filter ( genf ( P-GenericFilter (ω→2 ＼ HODω2) p lt C )))) =h= ω→2 -- HODω2 ∋ p
+    →  Union ( Replace' (Power (ω→2 ＼ HODω2)) (λ p lt → filter ( genf ( P-GenericFilter {!!} (ω→2 ＼ HODω2) p {!!}  {!!} C )))) =h= ω→2 -- HODω2 ∋ p
 lemma726 = {!!}
 
 --