# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649757134 -32400
# Node ID 1546541ed4618b752fed750e363c6746186c0b59
# Parent  3c03f5bf9e16d8e7f89abd46c07d1cac783f74e2
...

diff -r 3c03f5bf9e16 -r 1546541ed461 src/filter.agda
--- a/src/filter.agda	Tue Apr 12 15:58:53 2022 +0900
+++ b/src/filter.agda	Tue Apr 12 18:52:14 2022 +0900
@@ -229,12 +229,19 @@
      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
+-- 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 = {!!} where
-      mf01 : Maximal O P (_⊆'_ O)
-      mf01 = MaximumSubset O 0<L {!!}  {!!} {!!} {!!} 
+-- 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
+
+-- 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 {!!}  {!!} {!!} {!!} 
 
 
diff -r 3c03f5bf9e16 -r 1546541ed461 src/zorn.agda
--- a/src/zorn.agda	Tue Apr 12 15:58:53 2022 +0900
+++ b/src/zorn.agda	Tue Apr 12 18:52:14 2022 +0900
@@ -88,18 +88,6 @@
 me : { A a : HOD } → A ∋ a → Element A
 me {A} {a} lt = record { elm = a ; is-elm = lt }
 
-record SUP ( A B : HOD )  : Set (suc n) where
-   field
-      sup : HOD
-      A∋maximal : A ∋ sup
-      x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
-
-record Maximal ( A : HOD )  : Set (suc n) where
-   field
-      maximal : HOD
-      A∋maximal : A ∋ maximal
-      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
-
 record ZChain ( A : HOD ) (y : Ordinal)   : Set (suc n) where
    field
       max : HOD
@@ -143,11 +131,24 @@
       icy : odef (IChainSet {A} (me ax)) y  
       c-finite : ¬ OSup> (IChainSet {A} (me ax)) (d→∋ (IChainSet {A} (me ax)) icy)
       
-Zorn-lemma-case : { A : HOD } 
+record Maximal ( A : HOD )  : Set (suc n) where
+   field
+      maximal : HOD
+      A∋maximal : A ∋ maximal
+      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
+
+--
+-- possible three cases in a limit ordinal step
+-- 
+-- case 1) < goes > x
+-- case 2) no > x in some chain ( maximal )
+-- case 3) countably infinite chain below x
+--
+Zorn-lemma-3case : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
     → (x : Element A) → OSup> A (d→∋ A (is-elm x)) ∨ Maximal A ∨ InFiniteIChain A (d→∋ A (is-elm x))
-Zorn-lemma-case {A}  0<A PO x = zc2 where
+Zorn-lemma-3case {A}  0<A PO x = zc2 where
     Gtx : HOD
     Gtx = record { od = record { def = λ y → odef ( IChainSet x ) y ∧  ( & (elm x) o< y ) } ; odmax = & A
         ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A (proj1 (proj1 lt))))  }
@@ -162,6 +163,12 @@
     ... | yes  nohg = case2 (case2 {!!} )
 
 
+record SUP ( A B : HOD )  : Set (suc n) where
+   field
+      sup : HOD
+      A∋maximal : A ∋ sup
+      x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
+
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
@@ -261,14 +268,29 @@
           ... | tri< a ¬b ¬c = case1 record { max = ZChain.max z ; y<max = a }
           ... | tri≈ ¬a b ¬c = {!!} -- x = max so ¬ A ∋ max 
           ... | tri> ¬a ¬b c = {!!} -- can't happen
-     ... | yes ax = zc1 where -- we have previous ordinal and A ∋ x
+     ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
-          zc1 : ZChain A x ∨ Maximal A
-          zc1 with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
+          zc1 : OSup> A (subst (OD.def (od A)) (sym &iso) ax) → ZChain A x ∨ Maximal A
+          zc1 os with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
           ... | case2 x = case2 x
           ... | case1 x with is-o∅ ( & (Gtx ax ))
           ... | yes no-sup = case2 {!!}
           ... | no sup = case1 {!!}
+          zc4 : ZChain A x ∨ Maximal A
+          zc4 with Zorn-lemma-3case 0<A PO (me ax)
+          ... | case1 y>x = zc1 y>x
+          ... | case2 (case1 x) = case2 x
+          ... | case2 (case2 x) = ⊥-elim (zc5 x) where
+              FC : HOD
+              FC = IChainSet {A} (me ax)
+              zc6 :  InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax)  → ¬ SUP A FC 
+              zc6 = {!!}
+              FC-is-total : IsTotalOrderSet FC
+              FC-is-total = {!!}
+              FC⊆A :  FC ⊆ A
+              FC⊆A = {!!}
+              zc5 : InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax) → ⊥
+              zc5 x = zc6 x ( supP FC FC⊆A FC-is-total )
      ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = {!!} where
           zc1 : ZChain A (& A)