# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1647614723 -32400
# Node ID 3d84389cc43ff56ba87eff55f275d60d8cabdff0
# Parent  882c24efdc3f151fbda58b6bc37875fb72a919a6
...

diff -r 882c24efdc3f -r 3d84389cc43f src/filter.agda
--- a/src/filter.agda	Fri Mar 18 20:36:42 2022 +0900
+++ b/src/filter.agda	Fri Mar 18 23:45:23 2022 +0900
@@ -55,7 +55,7 @@
 record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter LP) : Set (suc (suc n)) where
    field
        proper  : ¬ (filter F ∋ od∅)
-       ultra   : {p : HOD } → L ∋ p →  ( filter F ∋ p ) ∨ (  filter F ∋ ( P ＼ p) )
+       ultra   : {p : HOD } → L ∋ p → ( filter F ∋ p ) ∨ (  filter F ∋ ( P ＼ p) )
 
 open _⊆_
 
@@ -81,13 +81,13 @@
 --  ultra filter is prime
 --
 
-filter-lemma1 :  {P L : HOD} → (LP : L ⊆ Power P)  → (F : Filter LP)  → ∀ {p q : HOD } → ultra-filter F  → prime-filter F 
+filter-lemma1 :  {P L : HOD} → (LP : L ⊆ Power P)  → (F : Filter LP)  → ultra-filter F  → prime-filter F 
 filter-lemma1 {P} {L} LP F u = record {
          proper = ultra-filter.proper u
        ; prime = lemma3
     } where
   lemma3 : {p q : HOD} → L ∋ p → L ∋ q  → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
-  lemma3 {p} {q} Lp Lq lt with ultra-filter.ultra u Lp
+  lemma3 {p} {q} Lp Lq lt with ultra-filter.ultra u Lp 
   ... | case1 p∈P  = case1 p∈P 
   ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P ＼ p)} Lq lemma7 lemma8) where
     lemma5 : ((p ∪ q ) ∩ (P ＼ p)) =h=  (q ∩ (P ＼ p))
@@ -110,28 +110,31 @@
 --  if Filter contains L, prime filter is ultra
 --
 
-filter-lemma2 :  {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP)  → filter F ∋ L → prime-filter F → ultra-filter F
-filter-lemma2 {P} {L} LP F f∋L prime = record {
+filter-lemma2 :  {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))
+         → (F : Filter LP)  → filter F ∋ P → prime-filter F → ultra-filter F
+filter-lemma2 {P} {L} LP Lm F f∋P prime = record {
          proper = prime-filter.proper prime
-       ; ultra = λ {p}  p⊆L → prime-filter.prime prime {!!} {!!} {!!} -- (lemma p  p⊆L)
+       ; ultra = λ {p}  L∋p → prime-filter.prime prime L∋p (Lm  L∋p) (lemma p (p⊆L  L∋p ))  
    } where
         open _==_
-        p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P ＼ p)) 
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
-        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
-        eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
+        p⊆L : {p : HOD} → L ∋ p  → p ⊆ P
+        p⊆L {p} lt = power→⊆ P p ( incl LP lt )
+        p+1-p=1 : {p : HOD} → p ⊆ P  → P =h= (p ∪ (P ＼ p)) 
+        eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x)
+        eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x
+        eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
+        eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (incl p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
+        eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p  ) = proj1 ¬p
         lemma : (p : HOD) → p ⊆ P   →  filter F ∋ (p ∪ (P ＼ p))
-        lemma p p⊆L = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) {!!} -- f∋L
+        lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P 
 
 -----
 --
 --  if there is a filter , there is a ultra filter under the axiom of choise
 --
 
-filter→ultra :  {P L : HOD} → (LP : L ⊆ Power P) → (F : Filter LP)  → ultra-filter F
-filter→ultra {P} {L} LP F = ?
+-- filter→ultra :  {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (F : Filter LP)  → ultra-filter F
+-- filter→ultra {P} {L} LP Lm F = {!!}
 
 record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
    field
diff -r 882c24efdc3f -r 3d84389cc43f src/generic-filter.agda
--- a/src/generic-filter.agda	Fri Mar 18 20:36:42 2022 +0900
+++ b/src/generic-filter.agda	Fri Mar 18 23:45:23 2022 +0900
@@ -144,16 +144,16 @@
 ... | tri≈ ¬a refl ¬c = refl-⊆
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
-P-GenericFilter : (P L p0 : HOD ) → L ⊆ Power P → L ∋ p0 → (C : CountableModel ) → GenericFilter L
+P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter LP
 P-GenericFilter P L p0 L⊆PP Lp0 C = record {
-      genf = record { filter = PDHOD L p0 C ; f⊆PL =  f⊆PL ; filter1 = {!!} ; filter2 = {!!}  }
+      genf = record { filter = PDHOD L p0 C ; f⊆L =  f⊆PL ; filter1 = {!!} ; filter2 = {!!}  }
     ; generic = {!!}
    } where
         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 :  PDHOD L p0 C ⊆ L -- 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 = {!!} } where -- power←  _ _ (incl q⊆P) } where
@@ -180,10 +180,10 @@
                f5 : odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (* (find-p P C (gr PD∋p) (& p0))) y
                f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋p} {gr PD∋q} (<to≤ c))
                    (subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) (sym &iso) lt) )
-        fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
+        fdense : (D : Dense L⊆PP ) → ¬ (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 : P ∋ p0 
+           p0⊆P : L ∋ p0 
            p0⊆P = {!!}
            fd : HOD
            fd = dense-f D p0⊆P
@@ -246,7 +246,7 @@
     df-p {x} lt with ODC.∋-p O G ( Incompatible.r (I x lt) )
     ... | yes _ = Incompatible.p⊆q (I x lt) 
     ... | no _ = Incompatible.p⊆r (I x lt) 
-    D-Dense : Dense P
+    D-Dense : Dense {!!}
     D-Dense = record {
            dense = D
        ;   d⊆P = record { incl = λ {x} lt → {!!} }
@@ -277,7 +277,7 @@
 --   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
+record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (G : GenericFilter LP) : Set (suc n) where
    field
      valx : HOD
 
@@ -287,8 +287,8 @@
      p∈G : odef (* oG) op 
      is-val : odef (* ox) ( & < * oy , * op >  )
 
-val : (x : HOD) {P : HOD }
-    →  (G : GenericFilter P)
+val : (x : HOD) {P L : HOD } {LP : L ⊆ Power P}
+    →  (G : GenericFilter LP)
     →  HOD
 val x G = TransFinite {λ x → HOD } ind (& x) where
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD