# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673425567 -32400
# Node ID 9904b262c08f85994feffa805b3be9e40f1ea88f
# Parent  d3dbc18d24378850ed261f8e1fbff4a883fdd1cf
...

diff -r d3dbc18d2437 -r 9904b262c08f src/filter.agda
--- a/src/filter.agda	Wed Jan 11 13:52:04 2023 +0900
+++ b/src/filter.agda	Wed Jan 11 17:26:07 2023 +0900
@@ -201,16 +201,14 @@
        y-p⊂x : ( * y ＼ * p ) ⊆ * x
 
 max→ultra : {L P : HOD} (LP : L ⊆ Power P) 
-       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ＼ q)) 
        → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
-       → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q))
-       → (mx : MaximumFilter {L} {P} LP ) → ultra-filter ( MaximumFilter.mf mx )
-max→ultra {L} {P} LP NEG CAP CUP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
+       → (mx : MaximumFilter {L} {P} LP ) → {y : Ordinal } → odef (filter (MaximumFilter.mf mx)) y → ultra-filter ( MaximumFilter.mf mx )
+max→ultra {L} {P} LP CAP mx {y} mxy = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
     mf = MaximumFilter.mf mx
     ultra : {p : HOD} → L ∋ p → L ∋ (P ＼ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P ＼ p))
     ultra {p} Lp Lnp with ODC.∋-p O (filter mf) p 
     ... | yes y = case1 y
-    ... | no np = ? where
+    ... | no np = case2 (subst (λ k → k ∋ (P ＼ p)) F=mf F∋P-p) where
          F : HOD  
          F = record { od = record { def = λ x →  odef L x ∧ Fp {L} {P} LP mx (& p) x } 
             ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } 
@@ -243,11 +241,18 @@
              mu03 : (* x ＼ * (& p)) ⊆ * x
              mu03 {z} ⟪ xz , _ ⟫ = xz
          F∋P-p : F ∋ (P ＼ p )
-         F∋P-p = ⟪ Lnp , record { y = ? ; mfy = ? ; y-p⊂x = ? }  ⟫ 
-         F≤ : & (filter (MaximumFilter.mf mx)) o≤ & F
-         F≤ = ⊆→o≤ ?
+         F∋P-p = ⟪ Lnp , record { y = y ; mfy = mxy ; y-p⊂x = mu30 }  ⟫  where
+             mu30 : (* y ＼ * (& p)) ⊆ * (& (P ＼ p))
+             mu30 {z} ⟪ yz , ¬pz ⟫ = subst (λ k → odef k z) (sym *iso) ( ⟪ Pz , (λ pz → ¬pz (subst (λ k → odef k z) (sym *iso) pz ))  ⟫  ) where
+                 Pz : odef P z
+                 Pz = LP (f⊆L mf mxy) _ yz
          FisProper : ¬ (filter FisFilter ∋ od∅)
-         FisProper = {!!}
+         FisProper ⟪ L0 , record { y = z ; mfy = mfz ; y-p⊂x = z-p⊂x } ⟫ = ?
+         mu40 = (MaximumFilter.is-maximum mx)
+         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 ⟫ )
 
 open _==_