# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1648979518 -32400
# Node ID 263d2d1a000ebb4121aba7b445ba8cdbe029b450
# Parent  6c22ee73ff06cf6af02bfb93ec0674a76e1bb55c
...

diff -r 6c22ee73ff06 -r 263d2d1a000e src/filter.agda
--- a/src/filter.agda	Sun Apr 03 17:53:13 2022 +0900
+++ b/src/filter.agda	Sun Apr 03 18:51:58 2022 +0900
@@ -173,13 +173,11 @@
        genf : Filter LP
        generic : (D : Dense LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
 
-open import zorn
-
 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
     field
        mf : Filter LP
        proper  : ¬ (filter mf ∋ od∅)
-       is-maximum : ( f : Filter LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( (¬ filter  mf ≡ filter f ) ∧ (filter mf  ⊆ filter f ))
+       is-maximum : ( f : Filter LP ) →  ¬ (filter f ∋ od∅)  →  ¬ filter  mf ≡ filter f → ¬ ( filter mf  ⊆ filter f  )
 
 max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter LP ) → ultra-filter ( MaximumFilter.mf mx )
 max→ultra {L} {P} LP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
@@ -189,7 +187,7 @@
     ... | yes y = case1 y
     ... | no np with ∋-p (filter mf) (P ＼ p) 
     ... | yes y = case2 y
-    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper ⟪ {!!} , record { incl = FisGreater } ⟫ ) where
+    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter FisProper  {!!}  record { incl = FisGreater } ) where
          Y : (y : Ordinal) → (my : odef (filter mf) y ) → HOD
          Y y my = record { od = record { def = λ x → (x ≡ y) ∨ (x ≡ & p) } ; odmax = & L ; <odmax = {!!} }
          F : HOD
@@ -206,8 +204,10 @@
 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))
-       → (F U : Filter LP) →  ¬ (filter F ∋ od∅) → ultra-filter U → ¬ filter U ≡ filter F → ¬ (filter U ⊆ filter F )
-ultra→max {L} {P} LP NG CAP F U Prop u U≠F U⊆F = ⊥-elim ( Prop f0 ) where
+       → (U : Filter LP) → ultra-filter U → MaximumFilter LP 
+ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where
+  is-maximum : (F : Filter LP) → (¬ (filter F ∋ od∅)) → ( U≠F :  ¬ filter  U ≡ filter F ) →  (U⊆F : filter U  ⊆ filter F ) → ⊥
+  is-maximum F Prop U≠F U⊆F  = Prop f0 where
      GT : HOD
      GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = {!!} ; <odmax = {!!} }
      GT≠∅ :  ¬ (GT =h= od∅)
@@ -229,3 +229,28 @@
      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 {!!} {!!}) )
  
+open import zorn
+
+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 LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter LP 
+MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} } where
+     _⊆'_ : ( A B : HOD ) → Set n
+     _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x
+     FL : HOD
+     FL = {!!}
+     0<FL :  o∅ o< & FL
+     0<FL = {!!}
+     PO : PartialOrderSet O FL _⊆'_
+     PO = {!!}
+     supP : (B : HOD) → B ⊆ FL → TotalOrderSet O B _⊆'_ → SUP O FL B _⊆'_
+     supP B B⊆FL cmp = record { sup = sup ; A∋maximal = A∋maximal ; x≤sup = x≤sup } where
+        sup : HOD
+        sup = {!!}
+        A∋maximal : B ∋ sup
+        A∋maximal = {!!}
+        x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x ⊆' sup )   
+        x≤sup = {!!}
+     maximum : Maximal O FL _⊆'_
+     maximum = Zorn-lemma O {FL} {_⊆'_} 0<FL {!!} {!!}
+
+
diff -r 6c22ee73ff06 -r 263d2d1a000e src/zorn.agda
--- a/src/zorn.agda	Sun Apr 03 17:53:13 2022 +0900
+++ b/src/zorn.agda	Sun Apr 03 18:51:58 2022 +0900
@@ -158,7 +158,7 @@
                  total : TotalOrderSet Bx _<_
                  total ex ey with is-elm ex | is-elm ey
                  ... | case1 eq | case1 eq1 = tri≈ {!!} {!!} {!!} 
-                 ... | case1 x | case2 x₁ = tri< {!!} {!!} {!!} 
+                 ... | case1 x | case2 x₁ = tri< {!!} {!!} {!!}  
                  ... | case2 x | case1 x₁ = {!!}
                  ... | case2 x | case2 x₁ = ZChain.total zc1 (me x) (me x₁)
      ind nomx x prev | no ¬ox with trio< (& A) x   --- limit ordinal case