# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1647498984 -32400
# Node ID 9207b0c3cfe9f2427a506b9f93e85f32196300d2
# Parent  d5909d3c725a46ec42d6b8baeee75f410940de1b
fix filter on subset of Power P

diff -r d5909d3c725a -r 9207b0c3cfe9 src/filter.agda
--- a/src/filter.agda	Thu Mar 17 14:04:25 2022 +0900
+++ b/src/filter.agda	Thu Mar 17 15:36:24 2022 +0900
@@ -38,27 +38,28 @@
 -- Kunen p.76 and p.53, we use ⊆
 record Filter  ( L : HOD  ) : Set (suc n) where
    field
-       filter : HOD   
-       f⊆PL :  filter ⊆ Power L 
-       filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+       filter  : HOD   
+       f⊆L     : filter ⊆ L
+       filter1 : { p q : HOD } →  L ∋ q → filter ∋ p →  p ⊆ q  → filter ∋ q
        filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
 
 open Filter
 
-record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
+record prime-filter { L : HOD } (F : Filter L) : Set (suc (suc n)) where
    field
-       proper  : ¬ (filter P ∋ od∅)
-       prime   : {p q : HOD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+       proper  : ¬ (filter F ∋ od∅)
+       prime   : {p q : HOD } →  filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
 
-record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
+record ultra-filter { L : HOD } (P : HOD ) (F : Filter L) : Set (suc (suc n)) where
    field
-       proper  : ¬ (filter P ∋ od∅)
-       ultra   : {p : HOD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
+       L⊆PP :  L ⊆ Power P
+       proper  : ¬ (filter F ∋ od∅)
+       ultra   : {p : HOD } → L ∋ p →  ( filter F ∋ p ) ∨ (  filter F ∋ ( P ＼ p) )
 
 open _⊆_
 
-∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
-∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
+∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p 
+∈-filter {L} {p} F lt = {!!} -- power→⊆ L p ( incl ? 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) }
@@ -76,15 +77,15 @@
 --  ultra filter is prime
 --
 
-filter-lemma1 :  {L : HOD} → (P : Filter L)  → ∀ {p q : HOD } → ultra-filter P  → prime-filter P 
-filter-lemma1 {L} P u = record {
+filter-lemma1 :  {P L : HOD} → (F : Filter L)  → ∀ {p q : HOD } → ultra-filter P F  → prime-filter F 
+filter-lemma1 {P} {L} F u = record {
          proper = ultra-filter.proper u
        ; prime = lemma3
     } where
-  lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
-  lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
+  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
-  ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
+  ... | 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  ⟫
        ;  eq← = λ {x} lt → ⟪  case2 (proj1 lt) , proj2 lt ⟫
@@ -93,10 +94,10 @@
          lemma4 x lt with proj1 lt
          lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
          lemma4 x lt | case2 qx = qx
-    lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
-    lemma6 = filter2 P lt ¬p∈P
-    lemma7 : filter P ∋ (q ∩ (L ＼ p))
-    lemma7 =  subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
+    lemma6 : filter F ∋ ((p ∪ q ) ∩ (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
     lemma8 = q∩q⊆q
 
@@ -105,10 +106,11 @@
 --  if Filter contains L, prime filter is ultra
 --
 
-filter-lemma2 :  {L : HOD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
-filter-lemma2 {L} P f∋L prime = record {
-         proper = prime-filter.proper prime
-       ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
+filter-lemma2 :  {P L : HOD} → (F : Filter L)  → filter F ∋ L → prime-filter F → ultra-filter P F
+filter-lemma2 {P} {L} F f∋L prime = record {
+         L⊆PP = {!!}
+       ; proper = prime-filter.proper prime
+       ; ultra = λ {p}  p⊆L → prime-filter.prime prime {!!} -- (lemma p  p⊆L)
    } where
         open _==_
         p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 
@@ -117,22 +119,22 @@
         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 L 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
-        lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
-        lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
+        lemma : (p : HOD) → p ⊆ L   →  filter F ∋ (p ∪ (P ＼ p))
+        lemma p p⊆L = {!!} -- subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
 
-record Dense  (P : HOD ) : Set (suc n) where
+record Dense  (L : HOD )  : Set (suc n) where
    field
        dense : HOD
-       d⊆P :  dense ⊆ Power P 
-       dense-f : {p : HOD} → p ⊆ P → HOD
-       dense-d :  { p : HOD} → (lt : p ⊆ P) → dense ∋ dense-f lt
-       dense-p :  { p : HOD} → (lt : p ⊆ P) → (dense-f lt) ⊆ p  
+       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 : HOD  ) : Set (suc n) where
    field
        ideal : HOD   
-       i⊆PL :  ideal ⊆ Power L 
-       ideal1 : { p q : HOD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
+       i⊆L :  ideal ⊆ L 
+       ideal1 : { p q : HOD } →  L ∋ q  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
        ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
 
 open Ideal
@@ -143,65 +145,9 @@
 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
-----
---
--- Filter/Ideal without ZF 
---     L have to be a Latice
---
-
-record IsPOder  {n : Level} (P : Set n) (_p≤_ : P → P → Set n) (1p : P) : Set n where
-   field
-     1p-max : { x : P } → x p≤ 1p
-     p<trans : { x y z : P } → x p≤ y → y p≤ z → x p≤ z 
-     p<refl : { x  : P } → x p≤ x 
-
-record POder {n : Level} (P : Set n) : Set (suc n) where
-   field
-     _p≤_ : P → P → Set n
-     1p : P 
-     isPOder : IsPOder P _p≤_ 1p
-
-record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-   field
-       filter : L → Set n
-       f⊆P :  PL filter 
-       filter1 : { p q : L } → PL (λ x → q ⊆ x )  → filter p →  p ⊆ q  → filter q
-       filter2 : { p q : L } → filter p →  filter q  → filter (p ∩ q)
 
-Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
-Filter-is-F {L} f = record {
-       filter = λ x → Lift (suc n) ((filter f) ∋ x)
-     ; f⊆P = λ x f∋x →  power→⊆ _ _ (incl ( f⊆PL f  ) (lower f∋x ))
-     ; filter1 = λ {p} {q} q⊆L f∋p  p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q)
-     ; filter2 = λ {p} {q} f∋p f∋q  → lift ( filter2 f (lower f∋p) (lower f∋q)) 
-    }
-
-record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-   field
-       dense : L → Set n
-       d⊆P :  PL dense 
-       dense-f : {p : L}  → PL (λ x → p ⊆ x ) → L 
-       dense-d :  { p : L} → (lt : PL (λ x → p ⊆ x )) → dense ( dense-f lt  )
-       dense-p :  { p : L} → (lt : PL (λ x → p ⊆ x )) → (dense-f lt) ⊆ p
+record GenericFilter (L : HOD) : Set (suc n) where
+    field
+       genf : Filter L
+       generic : (D : Dense L ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
 
-Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
-Dense-is-F {L} f = record {
-       dense =  λ x → Lift (suc n) ((dense f) ∋ x)
-    ;  d⊆P = λ x f∋x →  power→⊆ _ _ (incl ( d⊆P f  ) (lower f∋x ))
-    ;  dense-f = λ {p} lt → dense-f f (lt _ record { incl = λ x → x} ) 
-    ;  dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) )
-    ;  dense-p = λ {p} d → dense-p f (d p refl-⊆) 
-  } where open Dense
-
-       
-record GenericFilter (P : HOD) : Set (suc n) where
-    field
-       genf : Filter P
-       generic : (D : Dense P ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
-
-record F-GenericFilter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-    field
-       GFilter : F-Filter L PL _⊆_ _∩_
-       Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x →  L
-       Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) →  F-Filter.filter GFilter (Intersection D y )
-