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

diff -r 4a4ac5141b95 -r d3dbc18d2437 src/filter.agda
--- a/src/filter.agda	Wed Jan 11 08:38:05 2023 +0900
+++ b/src/filter.agda	Wed Jan 11 13:52:04 2023 +0900
@@ -165,6 +165,7 @@
 prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal {L} {P} LP → ∀ {p q : HOD } → Set n
 prime-ideal {L} {P} LP I {p} {q} =  ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q )
 
+open import Relation.Binary.Definitions
 
 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where
     field
@@ -177,12 +178,6 @@
        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
-    field 
-       y : Ordinal 
-       mfy : odef (filter (MaximumFilter.mf mx)) y
-       y-p⊂x : ( * y ＼ * p ) ⊂ * x
-
 mu10 : {a b : HOD} →  (a ＼ b) ⊆ a
 mu10 {a} {b} {x} ⟪ ax , ¬bx ⟫ = ax
 
@@ -194,6 +189,17 @@
 mu13 : {a b c : HOD} → o∅ o< & b →  a  ⊆ c →  (a ＼ b) ⊂ c
 mu13 = ?
 
+mu14 : {a b : HOD} → & ( a ∩ b ) o≤ & a
+mu14 {a} {b} = ⊆→o≤ ( λ ab → proj1 ab )
+
+-- mu15 : {a b : HOD} → & a o< & b → & ( a ∩ b ) ≡  & a  is not always valid
+
+record Fp {L P : HOD} (LP : L ⊆ Power P)  (mx : MaximumFilter {L} {P} LP ) (p x : Ordinal ) : Set n where
+    field 
+       y : Ordinal 
+       mfy : odef (filter (MaximumFilter.mf mx)) y
+       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))
@@ -202,7 +208,7 @@
 max→ultra {L} {P} LP NEG CAP CUP 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 
+    ultra {p} Lp Lnp with ODC.∋-p O (filter mf) p 
     ... | yes y = case1 y
     ... | no np = ? where
          F : HOD  
@@ -211,11 +217,11 @@
          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
             mu05 : (* y ＼ p) ⊆ r
-            mu05 = subst₂ (λ j k → (* y ＼ j ) ⊆ k ) *iso *iso (proj2 y-p⊂x)
+            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 = ⟪ ordtrans<-≤ (proj1 y-p⊂x) (subst₂ (λ j k → j o≤ k) (sym &iso) (sym &iso) (⊆→o≤ r⊆q)) , mu04 ⟫ 
+            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
@@ -223,36 +229,28 @@
             mu21 = CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfqy)) (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) 
             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
-            mu05 : & (* qy ＼ p) o< & q
-            mu05 = subst₂ (λ j k → & (* qy ＼ j ) o< k ) *iso &iso (proj1 qy-p⊂x)
-            mu06 : (* ry ＼ p) ⊆ r
-            mu06 = subst₂ (λ j k → (* ry ＼ j ) ⊆ k ) *iso *iso (proj2 ry-p⊂x)
             mu24 : ((* qy ∩ * ry) ＼ * (& p)) ⊆ (r ∩ q)
-            mu24 {x} ⟪ qry , npx ⟫ = ⟪ subst (λ k → odef k x) *iso ( proj2 ry-p⊂x ⟪ proj2 qry , npx ⟫ )  
-               , subst (λ k → odef k x) *iso ( proj2 qy-p⊂x ⟪ proj1 qry , npx ⟫ )   ⟫
-            mu25 : & ((* qy ∩ * ry) ＼ * (& p)) o≤ & (r ∩ q)
-            mu25 = ⊆→o≤ mu24
-            mu23 : ((* qy ∩ * ry) ＼ * (& p) ) ⊂ (r ∩ q)
-            mu23 with osuc-≡< mu25
-            ... | case1 eq = ?
-            ... | case2 lt = ⟪ lt  , mu24 ⟫
-            mu22 : (* (& (* qy ∩ * ry)) ＼ * (& p)) ⊂ * (& (r ∩ q))
-            mu22 = subst₂ (λ j k → (j ＼ * (& p)) ⊂ k ) (sym *iso) (sym *iso) mu23
+            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 ⟫ )   ⟫
+            mu23 : ((* qy ∩ * ry) ＼ * (& p) ) ⊆ (r ∩ q)
+            mu23 = mu24 
+            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 = ? ; filter1 = mu01 ; filter2 = mu02 }
+         FisFilter = record { filter = F ; f⊆L = λ {x} lt → proj1 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
-             mu03 : (* x ＼ * (& p)) ⊂ * x
-             mu03 =  ⟪ ? , ?  ⟫
-         F< : & (filter (MaximumFilter.mf mx)) o< & F
-         F< = ?
+             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≤ ?
          FisProper : ¬ (filter FisFilter ∋ od∅)
          FisProper = {!!}
 
 open _==_
 
--- open import Relation.Binary.Definitions
-
 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))