# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673667367 -32400
# Node ID e9a05e7c4e358eb8cd8170f08c2391cd2368ff40
# Parent  7515d1b0570b1ab82660aaa9ad4d74a33fa9a443
Maximal Filter and Ultra Filter generation done

diff -r 7515d1b0570b -r e9a05e7c4e35 src/filter.agda
--- a/src/filter.agda	Sat Jan 14 07:47:44 2023 +0900
+++ b/src/filter.agda	Sat Jan 14 12:36:07 2023 +0900
@@ -252,12 +252,14 @@
              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) ) ⟫ ) ) )
-         mu41 : filter F0 ⊆ F
-         mu41 {x} fx = ⟪ f⊆L F0 fx , record { y = ? ; mfy = ? ; y-p⊂x = ? } ⟫
+         F0⊆F : filter F0 ⊆ F
+         F0⊆F {x} fx = ⟪ f⊆L F0 fx , record { y = _ ; mfy = MaximumFilter.F⊆mf mx fx ; y-p⊂x = mu42 } ⟫ where
+             mu42 : (* x ＼ * (& p)) ⊆ * x
+             mu42 {z} ⟪ xz , ¬p ⟫ = xz
          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 F0⊆F ⟪ lt , FisGreater ⟫ )
 
 open _==_
 
@@ -327,8 +329,10 @@
 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 = ? 
+     ; filter1 = λ {p} {q} Lq Fp p⊆q → subst₂ (λ j k → odef j k ) (sym *iso) &iso 
+        ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q  )
+     ; filter2 = λ {p} {q} Fp Fq Lpq → subst₂ (λ j k → odef j k ) (sym *iso) refl ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp)
+         (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq )
      ; proper  = subst₂ (λ j k → ¬ odef j k ) (sym *iso) ord-od∅ proper 
    }
 
@@ -341,7 +345,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 = ? 
+F→Maximum {L} {P} LP NEG CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = subst (λ k → filter F ⊆ k ) (sym *iso) mf52  
          ; 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
@@ -431,10 +435,14 @@
       mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00  
          ; filter1 = mf01  
          ; filter2 = mf02 }
+      mf52 : filter F ⊆ Maximal.maximal mx
+      mf52 = subst (λ k → filter F ⊆ k ) *iso (proj2 mf53) where
+         mf53 : FX ∋ Maximal.maximal mx 
+         mf53 = Maximal.as mx 
       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 = ? 
+         mf51 = subst (λ k → filter F ⊆ k ) (sym *iso) F⊆f 
 
 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∅))