# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1648975993 -32400
# Node ID 6c22ee73ff06cf6af02bfb93ec0674a76e1bb55c
# Parent  fea0c2454b85982d2908786b0dd7ec8462de0449
...

diff -r fea0c2454b85 -r 6c22ee73ff06 src/BAlgbra.agda
--- a/src/BAlgbra.agda	Sun Apr 03 11:34:01 2022 +0900
+++ b/src/BAlgbra.agda	Sun Apr 03 17:53:13 2022 +0900
@@ -57,6 +57,13 @@
 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
      ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
 
+U-F=∅→F⊆U : {F U : HOD} →  ((x : Ordinal) →  ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U
+U-F=∅→F⊆U {F} {U} not = record { incl = gt02 } where
+    gt02 : { x : Ordinal } → odef F x → odef U x
+    gt02 {x} fx with ODC.∋-p O U (* x)
+    ... | yes y = subst (λ k → odef U k ) &iso y
+    ... | no  n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ )
+
 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
 ∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
     lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
diff -r fea0c2454b85 -r 6c22ee73ff06 src/ODUtil.agda
--- a/src/ODUtil.agda	Sun Apr 03 11:34:01 2022 +0900
+++ b/src/ODUtil.agda	Sun Apr 03 17:53:13 2022 +0900
@@ -66,6 +66,10 @@
 od⊆→o≤  : {x y : HOD } → x ⊆ y → & x o< osuc (& y)
 od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z)))
 
+⊆→= : {F U : HOD} → F ⊆ U  → U ⊆ F → F =h= U
+⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (incl FU (subst (λ k → odef F k) (sym &iso) lt) )
+                                     ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (incl UF (subst (λ k → odef U k) (sym &iso) lt) ) }
+
 subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
 subset-lemma  {A} {x} = record {
       proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
diff -r fea0c2454b85 -r 6c22ee73ff06 src/filter.agda
--- a/src/filter.agda	Sun Apr 03 11:34:01 2022 +0900
+++ b/src/filter.agda	Sun Apr 03 17:53:13 2022 +0900
@@ -179,7 +179,7 @@
     field
        mf : Filter LP
        proper  : ¬ (filter mf ∋ od∅)
-       is-maximum : ( f : Filter LP ) →  ¬ ( filter mf  ⊆ filter f )
+       is-maximum : ( f : Filter LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( (¬ filter  mf ≡ filter f ) ∧ (filter mf  ⊆ filter f ))
 
 max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter LP ) → ultra-filter ( MaximumFilter.mf mx )
 max→ultra {L} {P} LP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
@@ -189,18 +189,43 @@
     ... | yes y = case1 y
     ... | no np with ∋-p (filter mf) (P ＼ p) 
     ... | yes y = case2 y
-    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter {!!} ) where
+    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper ⟪ {!!} , record { incl = FisGreater } ⟫ ) where
          Y : (y : Ordinal) → (my : odef (filter mf) y ) → HOD
          Y y my = record { od = record { def = λ x → (x ≡ y) ∨ (x ≡ & p) } ; odmax = & L ; <odmax = {!!} }
          F : HOD
          F = record { od = record { def = λ x → (x ≡ & p) ∨ ((y : Ordinal) → (my : odef (filter mf) y ) → x ≡ & (Y y my) )  } ; odmax = & L ; <odmax = {!!} }
          FisFilter : Filter LP
          FisFilter = record { filter = F ; f⊆L = {!!} ; filter1 = {!!} ; filter2 = {!!} }
+         FisGreater : {x : HOD} → filter (MaximumFilter.mf mx) ∋ x → filter FisFilter ∋ x
+         FisGreater = {!!}
+         FisProper : ¬ (filter FisFilter ∋ od∅)
+         FisProper = {!!}
 
-ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (F U : Filter LP)  → ultra-filter U → ¬ filter U ⊆ filter F 
-ultra→max {L} {P} LP NG F U u U⊆F = {!!} where
-     max : {x : HOD} → filter F ∋ x → filter U ∋ x
-     max {x} fx with ultra-filter.ultra u {x} (incl (f⊆L F) fx) (NG (incl (f⊆L F) fx))
-     ... | case1 ux = ux
-     ... | case2 u-x = {!!}
+open _==_
+
+open import Relation.Binary.Definitions
+
+ultra→max : {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 U : Filter LP) →  ¬ (filter F ∋ od∅) → ultra-filter U → ¬ filter U ≡ filter F → ¬ (filter U ⊆ filter F )
+ultra→max {L} {P} LP NG CAP F U Prop u U≠F U⊆F = ⊥-elim ( Prop f0 ) where
+     GT : HOD
+     GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = {!!} ; <odmax = {!!} }
+     GT≠∅ :  ¬ (GT =h= od∅)
+     GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ (⊆→=  U⊆F (U-F=∅→F⊆U gt01)))) where
+         gt01 : (x : Ordinal) → ¬ odef (filter F) x ∧ (¬ odef (filter U) x)
+         gt01 x not = ¬x<0 ( eq→ eq not )
+     p : HOD
+     p = ODC.minimal O GT GT≠∅
+     ¬U∋p : ¬ ( filter U ∋ p )
+     ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅)
+     U∋-p : filter U ∋  ( P ＼ p )
+     U∋-p with ultra-filter.ultra u {p} {!!} {!!}
+     ... | case1 ux = ⊥-elim ( ¬U∋p ux )
+     ... | case2 u-x = u-x
+     F∋p : filter F ∋ p
+     F∋p = proj1 (ODC.x∋minimal O GT GT≠∅)
+     F∋-p : filter F ∋ ( P ＼ p )
+     F∋-p = incl U⊆F U∋-p 
+     f0 : filter F ∋ od∅
+     f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP {!!} {!!}) )