# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674098270 -32400
# Node ID b77391353c40fd371075d6d70d4d31bad6718200
# Parent  c4fd0bfdfbae5c2f348f7c622093cb9291c298b2
filter definition?

diff -r c4fd0bfdfbae -r b77391353c40 src/filter.agda
--- a/src/filter.agda	Thu Jan 19 11:13:40 2023 +0900
+++ b/src/filter.agda	Thu Jan 19 12:17:50 2023 +0900
@@ -48,7 +48,7 @@
        filter  : HOD   
        f⊆L     : filter ⊆ L
        filter1 : { p q : HOD } →  L ∋ q → filter ∋ p →  p ⊆ q  → filter ∋ q
-       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → L ∋ (p ∩ q) → filter ∋ (p ∩ q)
+       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
 
 open Filter
 
@@ -121,7 +121,7 @@
     lemma9 : L ∋ ((p ∪ q ) ∩ (P ＼ p))
     lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (IN Lq (NG Lp))
     lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
-    lemma6 = filter2 F lt ¬p∈P  lemma9
+    lemma6 = filter2 F lt ¬p∈P  
     lemma7 : filter F ∋ (q ∩ (P ＼ p))
     lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6
     lemma8 : (q ∩ (P ＼ p)) ⊆ q
@@ -197,33 +197,30 @@
        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))
        → (F0 : Filter {L} {P} LP) → {y : Ordinal } → odef (filter F0) y 
        → (mx : MaximumFilter {L} {P} LP F0 ) → ultra-filter ( MaximumFilter.mf mx )
-max→ultra {L} {P} LP CAP F0 {y} mfy mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
+max→ultra {L} {P} LP F0 {y} mfy 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 F0 mx (& p) x } 
-            ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } 
+         F = record { od = record { def = λ x →  Fp {L} {P} LP F0 mx (& p) x } 
+            ; odmax = & L ; <odmax = ? }
          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
+         mu01 {r} {q} Lq record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x }  r⊆q = record { y = y ; mfy = mfy ; y-p⊂x = mu03 }  where
             mu05 : (* y ＼ p) ⊆ r
             mu05 = subst₂ (λ j k → (* y ＼ j ) ⊆ k ) *iso *iso y-p⊂x
             mu04 :  (* y ＼ * (& p)) ⊆ * (& q)
             mu04 {x} ⟪ yx , npx ⟫ = subst (λ k → odef k x ) (sym *iso) (r⊆q (mu05 ⟪ yx , (λ px1 → npx (subst (λ k → odef k x) (sym *iso) px1 )) ⟫ )  )
             mu03 :  (* y ＼ * (& p)) ⊆ * (& q)
             mu03 = mu04 
-         mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q)
-         mu02 {r} {q} ⟪ Lr , record { y = ry ; mfy = mfry ; y-p⊂x = ry-p⊂x } ⟫ 
-          ⟪ Lq , record { y = qy ; mfy = mfqy ; y-p⊂x = qy-p⊂x } ⟫  Lrq = ⟪ Lrq , record { y = & (* qy  ∩ * ry) ; mfy = mu20 ; y-p⊂x = mu22 } ⟫ where
-            mu21 : L ∋ (* qy ∩ * ry)
-            mu21 = CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfqy)) (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) 
+         mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → F ∋ (r ∩ q)
+         mu02 {r} {q}  record { y = ry ; mfy = mfry ; y-p⊂x = ry-p⊂x } 
+           record { y = qy ; mfy = mfqy ; y-p⊂x = qy-p⊂x }   = record { y = & (* qy  ∩ * ry) ; mfy = mu20 ; y-p⊂x = mu22 }  where
             mu20 : odef (filter mf) (& (* qy ∩ * ry))
-            mu20 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfqy) (subst (λ k → odef (filter mf) k) (sym &iso) mfry)  mu21
+            mu20 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfqy) (subst (λ k → odef (filter mf) k) (sym &iso) mfry)  
             mu24 : ((* qy ∩ * ry) ＼ * (& p)) ⊆ (r ∩ q)
             mu24 {x} ⟪ qry , npx ⟫ = ⟪ subst (λ k → odef k x) *iso ( ry-p⊂x ⟪ proj2 qry , npx ⟫ )  
                , subst (λ k → odef k x) *iso ( qy-p⊂x ⟪ proj1 qry , npx ⟫ )   ⟫
@@ -232,13 +229,13 @@
             mu22 : (* (& (* qy ∩ * ry)) ＼ * (& p)) ⊆ * (& (r ∩ q))
             mu22 = subst₂ (λ j k → (j ＼ * (& p)) ⊆ k ) (sym *iso) (sym *iso) mu23
          FisFilter : Filter {L} {P} LP
-         FisFilter = record { filter = F ; f⊆L = λ {x} lt → proj1 lt  ; filter1 = mu01 ; filter2 = mu02 }
+         FisFilter = record { filter = F ; f⊆L = λ {x} lt → ? ; filter1 = mu01 ; filter2 = mu02 }
          FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx))  x → odef (filter FisFilter ) x
-         FisGreater {x} mfx = ⟪ f⊆L mf mfx , record { y = x ; mfy = mfx ; y-p⊂x = mu03 }  ⟫ where
+         FisGreater {x} mfx = record { y = x ; mfy = mfx ; y-p⊂x = mu03 }   where
              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
+         F∋P-p = record { y = y ; mfy = mxy ; y-p⊂x = mu30 }    where
              mxy : odef (filter (MaximumFilter.mf mx)) y
              mxy = MaximumFilter.F⊆mf mx mfy
              mu30 : (* y ＼ * (& p)) ⊆ * (& (P ＼ p))
@@ -246,14 +243,14 @@
                  Pz : odef P z
                  Pz = LP (f⊆L mf mxy ) _ 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 } ⟫ = 
+         FisProper  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
              mu31 : * z ⊆ p
              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) ) ⟫ ) ) )
          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
+         F0⊆F {x} 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
@@ -263,8 +260,8 @@
 
 open _==_
 
-ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} 
-       → L ∋ p → L ∋ ( P ＼ p)) 
+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 U
 ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; F⊆mf = λ x → x ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where 
@@ -299,7 +296,7 @@
      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 ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p  )
 
 --  if there is a filter , there is a ultra filter under the axiom of choise
 --        Zorn Lemma
@@ -308,7 +305,7 @@
    field
        f⊆L     : (* filter) ⊆ L
        filter1 : { p q : Ordinal } → odef L q → odef (* filter) p →  (* p) ⊆ (* q)  → odef (* filter) q
-       filter2 : { p q : Ordinal } → odef (* filter)  p →  odef (* filter) q  → odef L (& ((* p) ∩ (* q))) → odef (* filter) (& ((* p) ∩ (* q)))
+       filter2 : { p q : Ordinal } → odef (* filter)  p →  odef (* filter) q  → odef (* filter) (& ((* p) ∩ (* q)))
        proper : ¬ (odef (* filter ) o∅)
 
 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))
@@ -316,8 +313,8 @@
        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 )
+     ; filter2 = λ {p} {q} Fp Fq → 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) )
      ; proper  = subst₂ (λ j k → ¬ odef j k ) (sym *iso) ord-od∅ proper 
    }