# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673564428 -32400
# Node ID 464efeeb988e1f2fe79347a6c3057277444c9e99
# Parent  4c85ce2794e980afd92fbb2c5d8f44dee4b65eab
..

diff -r 4c85ce2794e9 -r 464efeeb988e src/filter.agda
--- a/src/filter.agda	Fri Jan 13 07:37:27 2023 +0900
+++ b/src/filter.agda	Fri Jan 13 08:00:28 2023 +0900
@@ -169,13 +169,14 @@
        genf : Filter {L} {P} LP
        generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
 
-record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
+record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) (F : Filter {L} {P} LP) : Set (suc n) where
     field
        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  )
 
-record Fp {L P : HOD} (LP : L ⊆ Power P)  (mx : MaximumFilter {L} {P} LP ) (p x : Ordinal ) : Set n where
+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 
        y : Ordinal 
        mfy : odef (filter (MaximumFilter.mf mx)) y
@@ -183,15 +184,16 @@
 
 max→ultra : {L P : HOD} (LP : L ⊆ Power P) 
        → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
-       → (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
+       → (F0 : Filter {L} {P} LP) 
+       → (mx : MaximumFilter {L} {P} LP F0 ) → ultra-filter ( MaximumFilter.mf mx )
+max→ultra {L} {P} LP CAP F0 mx = 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 = 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 } 
+         F = record { od = record { def = λ x →  odef L x ∧ Fp {L} {P} LP F0 mx (& p) x } 
             ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } 
          mu01 :  {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q
          mu01 {r} {q} Lq ⟪ Lr , record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x } ⟫ r⊆q = ⟪ Lq , record { y = y ; mfy = mfy ; y-p⊂x = mu03 } ⟫ where
@@ -222,11 +224,11 @@
              mu03 : (* x ＼ * (& p)) ⊆ * x
              mu03 {z} ⟪ xz , _ ⟫ = xz
          F∋P-p : F ∋ (P ＼ p )
-         F∋P-p = ⟪ Lnp , record { y = y ; mfy = mxy ; y-p⊂x = mu30 }  ⟫  where
-             mu30 : (* y ＼ * (& p)) ⊆ * (& (P ＼ p))
+         F∋P-p = ⟪ Lnp , record { y = ? ; mfy = ? ; y-p⊂x = mu30 }  ⟫  where
+             mu30 : (* ? ＼ * (& 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
+                 Pz = LP (f⊆L mf ? ) _ yz
          FisProper : ¬ (filter FisFilter ∋ od∅)    -- if F contains p, p is in mf which contract np
          FisProper ⟪ L0 , record { y = z ; mfy = mfz ; y-p⊂x = z-p⊂x } ⟫ = 
            ⊥-elim ( np (filter1 mf Lp (subst (λ k → odef (filter mf) k) (sym &iso) mfz) mu31) ) where
@@ -245,8 +247,8 @@
 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))
-       → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP 
-ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where
+       → (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 = ? ; 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
      GT : HOD
@@ -313,8 +315,8 @@
       fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (is-filter.f⊆L (proj1 lt ))  )
 
 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 →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP 
-F→Maximum {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = mf
+      → (F : Filter {L} {P} LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F
+F→Maximum {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = mf ; F⊆mf = ? 
          ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( is-filter.proper imf)  ; is-maximum = {!!} }  where
       FX : HOD
       FX = F⊆X {L} {P} LP F
@@ -344,7 +346,6 @@
 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) →  (0<F : o∅ o< & (filter F))  →  (proper : ¬ (filter F ∋ od∅)) 
       → ultra-filter ( MaximumFilter.mf (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ))
-F→ultra {L} {P} LP NEG CAP F 0<L 0<F proper = max→ultra {L} {P} LP CAP (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ) 
-     {& (filter F)} ? -- (MaximumFilter.proper (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ))
+F→ultra {L} {P} LP NEG CAP F 0<L 0<F proper = max→ultra {L} {P} LP CAP F (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper )