# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673524367 -32400
# Node ID c2c0cf7f2d7e59d7154204de0eb5e9eb992950fe
# Parent  9904b262c08f85994feffa805b3be9e40f1ea88f
...

diff -r 9904b262c08f -r c2c0cf7f2d7e src/filter.agda
--- a/src/filter.agda	Wed Jan 11 17:26:07 2023 +0900
+++ b/src/filter.agda	Thu Jan 12 20:52:47 2023 +0900
@@ -37,6 +37,11 @@
 open _∨_
 open Bool
 
+-- L is a boolean algebra, but we don't assume this explicitly
+--
+--     NEG : {p : HOD} → L ∋ p → L ∋ (P ＼ p)
+--     CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )
+--
 -- Kunen p.76 and p.53, we use ⊆
 record Filter { L P : HOD  } (LP : L ⊆ Power P) : Set (suc n) where
    field
@@ -134,14 +139,6 @@
         lemma10 : {p : HOD} → L ∋ p → L ∋ P → L ∋ (p ∪ (P ＼ p))
         lemma10 {p} L∋p lt = subst (λ k → L ∋ k ) (==→o≡ (p+1-p=1 {p} (p⊆L L∋p))) lt
 
------
---
---  if there is a filter , there is a ultra filter under the axiom of choise
---        Zorn Lemma
-
--- filter→ultra :  {P L : HOD} → (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (F : Filter {L} {P} LP)  → ultra-filter F
--- filter→ultra {P} {L} LP Lm F = {!!}
-
 record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
    field
        dense : HOD
@@ -178,22 +175,6 @@
        proper  : ¬ (filter mf ∋ od∅)
        is-maximum : ( f : Filter {L} {P} LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( filter mf  ⊂ filter f  )
 
-mu10 : {a b : HOD} →  (a ＼ b) ⊆ a
-mu10 {a} {b} {x} ⟪ ax , ¬bx ⟫ = ax
-
-mu11 : {a b : HOD} → o∅ o< & b →  (a ＼ b) ⊂ a
-mu11 {a} {b} 0<b = ⟪ mu12 , mu10 {a} {b} ⟫ where
-    mu12 : & (a ＼ b) o< & a
-    mu12 = ?
-
-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 
@@ -246,8 +227,13 @@
              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
-         FisProper : ¬ (filter FisFilter ∋ od∅)
-         FisProper ⟪ L0 , record { y = z ; mfy = mfz ; y-p⊂x = z-p⊂x } ⟫ = ?
+         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
+             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) ) ⟫ ) ) )
          mu40 = (MaximumFilter.is-maximum mx)
          F=mf : F ≡ filter mf
          F=mf with osuc-≡< ( ⊆→o≤ FisGreater )
@@ -294,6 +280,9 @@
      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) )
 
+--  if there is a filter , there is a ultra filter under the axiom of choise
+--        Zorn Lemma
+
 import zorn 
 
 open import Relation.Binary
@@ -301,25 +290,38 @@
 PO : IsStrictPartialOrder _≡_ _⊂_ 
 PO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
    ; trans = λ {a} {b} {c} → trans-⊂ {a} {b} {c}
-   ; irrefl = λ x=y x<y → ?
-   ; <-resp-≈ =  record { fst = λ {x} {y} {y1} y=y1 xy1 → ? ; snd = λ {x} {x1} {y} x=x1 x1y → ? } }
+   ; irrefl = λ x=y x<y → o<¬≡ (cong (&) x=y) (proj1 x<y)
+   ; <-resp-≈ =  record { fst = ( λ {x} {y} {y1} y=y1 xy1 → subst (λ k → x ⊂ k) y=y1 xy1  )
+                        ; snd = (λ {x} {x1} {y} x=x1 x1y → subst (λ k → k ⊂ x) x=x1 x1y ) } }
 
 open zorn O _⊂_ PO
 
 open import  Relation.Binary.Structures
 
-SUP⊆ : (P B : HOD) → B ⊆ P → IsTotalOrderSet B → SUP P B
-SUP⊆ P B B⊆P OB = record { sup = Union B ; isSUP = record { ax = ? ; x≤sup = ? } }
+record is-filter { L P : HOD  } (LP : L ⊆ Power P) (filter : Ordinal ) : Set n where
+   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)))
+       proper : ¬ (odef (* filter ) o∅)
 
-MaximumSubset : {L P : HOD} 
-      → o∅ o< & L →  o∅ o< & P → P ⊆ L
-      → Maximal  P
-MaximumSubset {L} {P} 0<L 0<P P⊆L = Zorn-lemma 0<P (SUP⊆ P)
+-- all filter contains F
+F⊆X : { L P : HOD  } (LP : L ⊆ Power P) → Filter {L} {P} LP  → HOD
+F⊆X {L} {P} LP F = record { od = record { def = λ x → is-filter {L} {P} LP x ∧ ( filter F ⊆ * x)  } ; odmax = osuc (& L)
+      ; <odmax = λ {x} lt → fx00 lt } where
+      fx00 : {x : Ordinal } → is-filter LP x ∧ filter F ⊆ * x → x o< osuc (& L)
+      fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (is-filter.f⊆L (proj1 lt ))  )
 
 MaximumFilterExist : {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 
 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} }  where
-     mf01 : Maximal  {!!}  
-     mf01 = MaximumSubset  0<L {!!} {!!}  
+      FX : HOD
+      FX = F⊆X {L} {P} LP F
+      FX∋F : odef FX (& (filter F))
+      FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = ? ; filter2 = ? ; proper = ? }  , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ 
+      SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B
+      SUP⊆ B B⊆FX OB = record { sup = Union B ; isSUP = record { ax = ? ; x≤sup = ?  } }
+      mf01 : Maximal  FX
+      mf01 = Zorn-lemma (∈∅< FX∋F) SUP⊆