# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1718932426 -32400
# Node ID 51b6bc16593c44108821f77c723aa3822441c92b
# Parent  ca5bfb401ada68ce82564033abea8ff041395663
filter fix done

diff -r ca5bfb401ada -r 51b6bc16593c src/filter.agda
--- a/src/filter.agda	Thu Jun 20 18:15:17 2024 +0900
+++ b/src/filter.agda	Fri Jun 21 10:13:46 2024 +0900
@@ -254,7 +254,7 @@
              mu42 {z} ⟪ xz , ¬p ⟫ = xz
          F=mf : F =h= filter mf
          F=mf with osuc-≡< ( ⊆→o≤ FisGreater )
-         ... | case1 eq = ord→== (sym eq) -- &≡&→≡ (sym eq)
+         ... | case1 eq = ord→== (sym eq) 
          ... | case2 lt = ⊥-elim ( MaximumFilter.is-maximum mx FisFilter FisProper F0⊆F ⟪ lt , FisGreater ⟫ )
 
 
@@ -270,19 +270,21 @@
          um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L
          um02 {y} Fy = odef< ( f⊆L F (proj1 Fy ) )
      GT≠∅ :  ¬ (GT =h= od∅)
-     GT≠∅ eq = ? where -- ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where
-        U≠F : ¬ ( filter U ≡ filter F )
-        U≠F eq = o<¬≡ (cong (&) eq) U<F
+     GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F  gt02 )   ) ) where
+        U≠F : ¬ ( & (filter U) ≡ & (filter F ))
+        U≠F eq  = o<¬≡ eq U<F
         gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x))
         gt01 x not = ¬x<0 ( eq→ eq not )
+        gt02 : filter F ⊆ filter U
+        gt02 {x} fx = U-F=∅→F⊆U {filter U} {filter F} {filter U} (λ x → x) gt01 fx
      p : HOD
      p = minimal GT GT≠∅
      ¬U∋p : ¬ ( filter U ∋ p )
-     ¬U∋p = ? -- proj2 (ODC.x∋minimal O GT GT≠∅)
+     ¬U∋p = proj2 (x∋minimal GT GT≠∅)
      L∋p : L ∋  p
-     L∋p = ? -- f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅))
+     L∋p = f⊆L F ( proj1 (x∋minimal GT GT≠∅))
      um00 : ¬ odef (filter U) (& p)
-     um00 = ? -- proj2 (ODC.x∋minimal O GT GT≠∅)
+     um00 = proj2 (x∋minimal GT GT≠∅)
      L∋-p : L ∋  ( P ＼ p )
      L∋-p = NEG L∋p
      U∋-p : filter U ∋  ( P ＼ p )
@@ -290,11 +292,14 @@
      ... | 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 = proj1 (x∋minimal GT GT≠∅)
      F∋-p : filter F ∋ ( P ＼ p )
      F∋-p = 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 L∋p L∋-p) )
+     f0 = subst (λ k → odef (filter F) k ) (==→o≡ ff0 ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) ) where
+         ff0 : (p ∩ (P ＼ p)) =h= od∅
+         ff0 = record { eq→ = λ {x} lt → ⊥-elim (proj2 (proj2 lt ) (proj1 lt)) 
+                     ;  eq← = λ {x} lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) }
 
 --  if there is a filter , there is a ultra filter under the axiom of choise
 --        Zorn Lemma
@@ -308,10 +313,12 @@
 
 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 = ? -- λ {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 
-   }
+       f⊆L     = λ {x} lt →  f⊆L F (eq→  *iso  lt ) 
+     ; filter1 = λ {p} {q} Lq Fp p⊆q → eq←  *iso (subst (λ k → odef (filter F) k )  &iso 
+         (filter1 F (subst (λ k → odef L k) (sym &iso) Lq) (subst (λ k → odef (filter F) k) (sym &iso) (eq→ *iso Fp ) ) p⊆q ))
+     ; filter2 = λ {p} {q} Fp Fq Lpq → eq← *iso (filter2 F 
+         (subst (λ k → odef (filter F) k) (sym &iso) (eq→ *iso Fp )) 
+         (subst (λ k → odef (filter F) k) (sym &iso) (eq→ *iso Fq )) 
+         Lpq )
+     ; proper  = λ lt → proper (eq→ *iso (subst (λ k → odef (* (& (filter F))) k) (sym ord-od∅) lt )) 
+   }