# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673650064 -32400
# Node ID 7515d1b0570b1ab82660aaa9ad4d74a33fa9a443
# Parent  4517d0721b59f000ff4c6c4727d857de96150562
...

diff -r 4517d0721b59 -r 7515d1b0570b src/filter.agda
--- a/src/filter.agda	Fri Jan 13 13:16:49 2023 +0900
+++ b/src/filter.agda	Sat Jan 14 07:47:44 2023 +0900
@@ -77,6 +77,20 @@
 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
 q∩q⊆q lt = proj1 lt 
 
+∩→≡1 : {p q : HOD } → p ⊆ q → (q ∩ p) ≡ p
+∩→≡1 {p} {q} p⊆q =  ==→o≡ record { eq→ = c00 ; eq← = c01 } where
+    c00 : {x : Ordinal} → odef (q ∩ p) x → odef p x
+    c00 {x} qpx = proj2 qpx
+    c01 : {x : Ordinal} → odef p x → odef (q ∩ p) x 
+    c01 {x} px = ⟪ p⊆q px , px  ⟫
+
+∩→≡2 : {p q : HOD } → q ⊆ p → (q ∩ p) ≡ q
+∩→≡2 {p} {q} q⊆p =  ==→o≡ record { eq→ = c00 ; eq← = c01 } where
+    c00 : {x : Ordinal} → odef (q ∩ p) x → odef q x
+    c00 {x} qpx = proj1 qpx
+    c01 : {x : Ordinal} → odef q x → odef (q ∩ p) x 
+    c01 {x} qx = ⟪ qx , q⊆p qx  ⟫
+
 open HOD
 
 -----
@@ -174,7 +188,7 @@
        mf : Filter {L} {P} LP
        F⊆mf : filter F ⊆ filter mf
        proper  : ¬ (filter mf ∋ od∅)
-       is-maximum : ( f : Filter {L} {P} LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( filter mf  ⊂ filter f  )
+       is-maximum : ( f : Filter {L} {P} LP ) →  ¬ (filter f ∋ od∅)  → filter F ⊆ filter f →  ¬ ( filter mf  ⊂ filter f  )
 
 record Fp {L P : HOD} (LP : L ⊆ Power P)  (F : Filter {L} {P} LP) (mx : MaximumFilter {L} {P} LP F ) (p x : Ordinal ) : Set n where
     field 
@@ -238,11 +252,12 @@
              mu31 {x} zx with ODC.decp O (odef p x)
              ... | yes px = px
              ... | no npx = ⊥-elim ( ¬x<0 (subst (λ k → odef k x) *iso (z-p⊂x ⟪ zx , (λ px → npx (subst (λ k → odef k x) *iso px) ) ⟫ ) ) )
-         mu40 = (MaximumFilter.is-maximum mx)
+         mu41 : filter F0 ⊆ F
+         mu41 {x} fx = ⟪ f⊆L F0 fx , record { y = ? ; mfy = ? ; y-p⊂x = ? } ⟫
          F=mf : F ≡ filter mf
          F=mf with osuc-≡< ( ⊆→o≤ FisGreater )
          ... | case1 eq = &≡&→≡ (sym eq)
-         ... | case2 lt = ⊥-elim ( MaximumFilter.is-maximum mx FisFilter FisProper ⟪ lt , FisGreater ⟫ )
+         ... | case2 lt = ⊥-elim ( MaximumFilter.is-maximum mx FisFilter FisProper ? ⟪ lt , FisGreater ⟫ )
 
 open _==_
 
@@ -251,8 +266,8 @@
        → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
        → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP U
 ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; F⊆mf = λ x → x ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where 
-  is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → (U⊂F : filter U  ⊂ filter F ) → ⊥
-  is-maximum F Prop ⟪ U<F , U⊆F ⟫   = Prop f0 where
+  is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → filter U ⊆ filter F  → (U⊂F : filter U  ⊂ filter F ) → ⊥
+  is-maximum F Prop F⊆U ⟪ U<F , U⊆F ⟫   = Prop f0 where
      GT : HOD
      GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = & L ; <odmax = um02 } where
          um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L
@@ -309,6 +324,14 @@
        filter2 : { p q : Ordinal } → odef (* filter)  p →  odef (* filter) q  → odef L (& ((* p) ∩ (* q))) → odef (* filter) (& ((* p) ∩ (* q)))
        proper : ¬ (odef (* filter ) o∅)
 
+Filter-is-Filter : { L P : HOD  } (LP : L ⊆ Power P) → (F : Filter {L} {P} LP) → (proper : ¬ (filter F) ∋ od∅ ) → IsFilter {L} {P} LP (& (filter F))
+Filter-is-Filter {L} {P} LP F proper = record { 
+       f⊆L     = subst (λ k → k ⊆ L ) (sym *iso) (f⊆L F)
+     ; filter1 = ? 
+     ; filter2 = ? 
+     ; proper  = subst₂ (λ j k → ¬ odef j k ) (sym *iso) ord-od∅ proper 
+   }
+
 -- all filter contains F
 F⊆X : { L P : HOD  } (LP : L ⊆ Power P) → Filter {L} {P} LP  → HOD
 F⊆X {L} {P} LP F = record { od = record { def = λ x → IsFilter {L} {P} LP x ∧ ( filter F ⊆ * x)  } ; odmax = osuc (& L)
@@ -319,7 +342,7 @@
 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (F : Filter {L} {P} LP) → o∅ o< & L →  {y : Ordinal } → odef (filter F) y →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F
 F→Maximum {L} {P} LP NEG CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = ? 
-         ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( IsFilter.proper imf)  ; is-maximum = {!!} }  where
+         ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( IsFilter.proper imf)  ; is-maximum = mf50 }  where
       FX : HOD
       FX = F⊆X {L} {P} LP F
       oF = & (filter F)
@@ -341,7 +364,7 @@
       SUP⊆ B B⊆FX OB with trio< (& B) o∅ 
       ... | tri< a ¬b ¬c = ⊥-elim (¬x<0 a )
       ... | tri≈ ¬a b ¬c = record { sup = filter F ; isSUP = record { ax = FX∋F ; x≤sup = λ {y} zy → ⊥-elim (o<¬≡ (sym b) (∈∅< zy))  } } 
-      ... | tri> ¬a ¬b 0<B = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = ? } } where
+      ... | tri> ¬a ¬b 0<B = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = mf40 } } where
           mf20 : HOD
           mf20 = ODC.minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B )))
           mf18 : odef B (& mf20 )
@@ -358,9 +381,21 @@
           mf31 {p} {q} bp bq Lpq with subst (λ k → odef k p ) *iso bp | subst (λ k → odef k q ) *iso bq
           ... | record { owner = bp ; ao = Bbp ; ox = bbp } | record { owner = bq ; ao = Bbq ; ox = bbq } 
              with OB (subst (λ k → odef B k) (sym &iso) Bbp) (subst (λ k → odef B k) (sym &iso) Bbq)
-          ... | tri< bp⊂bq ¬b ¬c = ?
-          ... | tri≈ ¬a bq=bp ¬c = ?
-          ... | tri> ¬a ¬b bq⊂bp = ?
+          ... | tri< bp⊂bq ¬b ¬c = subst₂ (λ j k → odef j k ) (sym  *iso) refl record { owner = bq ; ao = Bbq ; ox = mf36 } where
+              mf36 : odef (* bq) (& ((* p) ∩ (* q)))
+              mf36 = IsFilter.filter2 mf30 (proj2 bp⊂bq bbp) bbq Lpq where
+                  mf30 : IsFilter {L} {P} LP bq
+                  mf30 = proj1 ( B⊆FX Bbq ) 
+          ... | tri≈ ¬a bq=bp ¬c = subst₂ (λ j k → odef j k ) (sym  *iso) refl record { owner = bp ; ao = Bbp ; ox = mf36 } where
+              mf36 : odef (* bp) (& ((* p) ∩ (* q)))
+              mf36 = IsFilter.filter2 mf30 bbp (subst (λ k → odef k q) (sym bq=bp) bbq) Lpq where
+                  mf30 : IsFilter {L} {P} LP bp
+                  mf30 = proj1 ( B⊆FX Bbp ) 
+          ... | tri> ¬a ¬b bq⊂bp = subst₂ (λ j k → odef j k ) (sym  *iso) refl record { owner = bp ; ao = Bbp ; ox = mf36 } where
+              mf36 : odef (* bp) (& ((* p) ∩ (* q)))
+              mf36 = IsFilter.filter2 mf30 bbp (proj2 bq⊂bp bbq) Lpq where
+                  mf30 : IsFilter {L} {P} LP bp
+                  mf30 = proj1 ( B⊆FX Bbp ) 
           mf32 : ¬ odef (Union B) o∅
           mf32 record { owner = owner ; ao = bo ; ox = o0 } with proj1 ( B⊆FX bo ) 
           ... | record { f⊆L = f⊆L ; filter1 = filter1 ; filter2 = filter2 ; proper = proper } = ⊥-elim ( proper o0 )
@@ -372,6 +407,13 @@
                mf22 Fx = subst (λ k → odef k x) *iso ( proj2 (B⊆FX mf18) Fx )
           mf13 : odef FX (& (Union B))
           mf13 = ⟪ mf14  , subst (λ k → filter F ⊆ k ) (sym *iso) mf15  ⟫
+          mf42 : {z : Ordinal} → odef B z → * z ⊆  Union B
+          mf42 {z} Bz {x} zx = record { owner  = _ ; ao = Bz ; ox = zx }
+          mf40 : {z : Ordinal} → odef B z → (z ≡ & (Union B)) ∨ ( * z ⊂ * (& (Union B)) )
+          mf40 {z} Bz with B⊆FX Bz
+          ... | ⟪ filterz , F⊆z ⟫ with osuc-≡< ( ⊆→o≤ {* z} {Union B} (mf42 Bz) )
+          ... | case1 eq = case1 (trans (sym &iso) eq )
+          ... | case2 lt = case2 ⟪ subst₂ (λ j k → j o< & k ) refl (sym *iso) lt  , subst (λ  k → * z ⊆ k) (sym *iso)  (mf42 Bz)  ⟫
       mx : Maximal  FX
       mx = Zorn-lemma (∈∅< FX∋F) SUP⊆  
       imf : IsFilter {L} {P} LP (& (Maximal.maximal mx))
@@ -389,7 +431,10 @@
       mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00  
          ; filter1 = mf01  
          ; filter2 = mf02 }
-          
+      mf50 : (f : Filter LP) → ¬ (filter f ∋ od∅) → filter F ⊆ filter f → ¬ (* (& (zorn.Maximal.maximal mx)) ⊂ filter f)
+      mf50 f proper F⊆f = subst (λ k → ¬ ( k ⊂ filter f )) (sym *iso) (Maximal.¬maximal<x mx ⟪ Filter-is-Filter {L} {P} LP f proper  , mf51 ⟫ ) where
+         mf51 : filter F ⊆ * (& (filter f))
+         mf51 = ? 
 
 F→ultra : {L P : HOD} (LP : L ⊆ Power P) → (NEG : {p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (F : Filter {L} {P} LP) → (0<L : o∅ o< & L) →  {y : Ordinal} →  (0<F : odef (filter F) y) →  (proper : ¬ (filter F ∋ od∅))