# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650079208 -32400
# Node ID 2860168484036f4da4db626b25b87acd3d0222ee
# Parent  5faeae7cfe22eca6c6bf063d9a47aa125fa641ce
...

diff -r 5faeae7cfe22 -r 286016848403 src/filter.agda
--- a/src/filter.agda	Sat Apr 16 12:10:09 2022 +0900
+++ b/src/filter.agda	Sat Apr 16 12:20:08 2022 +0900
@@ -228,20 +228,24 @@
      F∋-p = incl 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 {!!} {!!}) )
- 
--- open import zorn 
+
+_⊆'_ : ( A B : HOD ) → Set n
+_⊆'_ A B = (x : Ordinal ) → odef A x → odef B x
+
+import zorn 
+open zorn O _⊆'_
 
--- MaximumSubset : {L P : HOD} 
---        → o∅ o< & L →  o∅ o< & P → P ⊆ L
---        → IsPartialOrderSet P _⊆'_
---        → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B _⊆'_ → SUP P B _⊆'_ )
---        → Maximal P (_⊆'_)
--- MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma {P} {_⊆'_} 0<P PO SP
+MaximumSubset : {L P : HOD} 
+      → o∅ o< & L →  o∅ o< & P → P ⊆ L
+      → IsPartialOrderSet P 
+      → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B  → SUP P B  )
+      → Maximal P 
+MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma 0<P PO SP
 
--- 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 = {!!} where
---       mf01 : Maximal O P (_⊆'_ O)
---       mf01 = MaximumSubset O 0<L {!!}  {!!} {!!} {!!} 
+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
+     mf01 : Maximal  P 
+     mf01 = MaximumSubset  0<L {!!}  {!!} {!!} {!!} 
 
 
diff -r 5faeae7cfe22 -r 286016848403 src/zorn.agda
--- a/src/zorn.agda	Sat Apr 16 12:10:09 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 12:20:08 2022 +0900
@@ -394,18 +394,13 @@
      ... | yes ax = {!!}
      zorn03 : (x : Ordinal) → ZChain A x  ∨ Maximal A 
      zorn03 x = TransFinite ind  x
-     zorn07 : (x : HOD) → (ax : A ∋ x ) → OSup> A (d→∋ A ax) ∨ Maximal A ∨ InFiniteIChain A (d→∋ A ax)
-     zorn07 x = ε-induction (λ {x} prev ax →  Zorn-lemma-3case 0<A PO (me {A} {x}  ax ) ) x
-     zorn05 : Maximal A 
-     zorn05 with zorn07 A {!!}
-     ... | case1 chain = {!!}
-     ... | case2 (case1 m) = m
-     ... | case2 (case2 chain) = {!!}
      zorn04 : Maximal A 
      zorn04 with zorn03 (& A)
      ... | case1 chain = ⊥-elim ( o<> (c<→o< {ZChain.max chain} {A} (ZChain.A∋max chain))  (ZChain.y<max chain) )
      ... | case2 m = m
 
+-- usage (see filter.agda )
+--
 -- _⊆'_ : ( A B : HOD ) → Set n
 -- _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x