# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671619106 -32400
# Node ID b19716b2dbaede95a58ab91f1048b914187483ed
# Parent  6caa088346f02cdcf89d669f1ecaf0a64288bd7e
this is no good

diff -r 6caa088346f0 -r b19716b2dbae src/zorn.agda
--- a/src/zorn.agda	Wed Dec 21 08:39:39 2022 +0900
+++ b/src/zorn.agda	Wed Dec 21 19:38:26 2022 +0900
@@ -151,14 +151,17 @@
    x≤sup = IsMinSUP.x≤sup isMinSUP
    minsup = IsMinSUP.minsup isMinSUP
 
+minsup-unique : {A B : HOD} → {x y : MinSUP A B} → MinSUP.sup x ≡ MinSUP.sup y
+minsup-unique {A} {B} {x} {y} with trio< (MinSUP.sup x) (MinSUP.sup y)
+... | tri< a ¬b ¬c = ⊥-elim ( o≤> ( MinSUP.minsup y (MinSUP.as x) (MinSUP.x≤sup x) ) a )
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( MinSUP.minsup x (MinSUP.as y) (MinSUP.x≤sup y) ) c )
+
 record IChain (A : HOD) ( f : Ordinal → Ordinal ) (x : Ordinal ) : Set n where
    field
       y : Ordinal
       x=fy   : x ≡ f y
 
-z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
-z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-
 --
 --   Our Proof strategy of the Zorn Lemma  
 --
@@ -173,9 +176,6 @@
 --
 
 
-∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
-∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
-
 -- Union of supf z and FClosure A f y
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
@@ -251,7 +251,7 @@
                   ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫  )
                 ... | case2 notz = case1 (λ _ → notz )
          m03 : ¬ ((z : Ordinal) → z o< & A → ¬ odef A z ∧ xsup z)
-         m03 not = ⊥-elim ( not s1 (z09 (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where
+         m03 not = ⊥-elim ( not s1 (odef< (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where
              S : SUP A B
              S = supP B  B⊆A total
              s1 = & (SUP.sup S)
@@ -262,28 +262,31 @@
          m02 : MinSUP A B
          m02 = dont-or (m00 (& A)) m03
 
---   -- Uncountable ascending chain by axiom of choice
---   cf : ¬ Maximal A → Ordinal → Ordinal
---   cf  nmx x with ODC.∋-p O A (* x)
---   ... | no _ = o∅
---   ... | yes ax with is-o∅ (& ( Gtx ax ))
---   ... | yes nogt = -- no larger element, so it is maximal
---       ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ )
---   ... | no not =  & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
---   is-cf : (nmx : ¬ Maximal A ) → {x : Ordinal} → odef A x → odef A (cf nmx x) ∧ ( * x < * (cf nmx x) )
---   is-cf nmx {x} ax with ODC.∋-p O A (* x)
---   ... | no not = ⊥-elim ( not (subst (λ k → odef A k ) (sym &iso) ax ))
---   ... | yes ax with is-o∅ (& ( Gtx ax ))
---   ... | yes nogt = ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ )
---   ... | no not = ODC.x∋minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
---
---   ---
---   --- infintie ascention sequence of f
---   ---
---   cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) →  odef A x → ( * x < * (cf nmx x) ) ∧  odef A (cf nmx x )
---   cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫
---   cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
---   cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
+     -- Uncountable ascending chain by axiom of choice
+     cf : ¬ Maximal A → Ordinal → Ordinal
+     cf  nmx x with ODC.∋-p O A (* x)
+     ... | no _ = o∅
+     ... | yes ax with is-o∅ (& ( Gtx ax ))
+     ... | yes nogt = -- no larger element, so it is maximal
+         ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ )
+     ... | no not =  & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
+     is-cf : (nmx : ¬ Maximal A ) → {x : Ordinal} → odef A x → odef A (cf nmx x) ∧ ( * x < * (cf nmx x) )
+     is-cf nmx {x} ax with ODC.∋-p O A (* x)
+     ... | no not = ⊥-elim ( not (subst (λ k → odef A k ) (sym &iso) ax ))
+     ... | yes ax with is-o∅ (& ( Gtx ax ))
+     ... | yes nogt = ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ )
+     ... | no not = ODC.x∋minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
+  
+     ---
+     --- infintie ascention sequence of f
+     ---
+     cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) →  odef A x → ( * x < * (cf nmx x) ) ∧  odef A (cf nmx x )
+     cf-is-<-monotonic nmx x ax = ⟪ proj2 (is-cf nmx ax ) , proj1 (is-cf nmx ax ) ⟫
+     cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
+     cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
+
+     CF :  ¬ Maximal A → HOD
+     CF nmx = record { od = record { def = λ x → odef A x ∧ IChain A (cf nmx) x } ; odmax = & A ; <odmax = λ lt → odef< (proj1 lt) } 
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -298,23 +301,65 @@
           asupf : {z : Ordinal} → odef A (supf z) 
           supf-< : {z : Ordinal} → odef A z →  * z < * (supf z) 
           f-next  : {z : Ordinal } → odef chain z → odef chain (supf z)
-          supf→chain : Ordinal → Ordinal 
-          sc-iso : {z : Ordinal} → supf (supf→chain z) ≡ z
-          sc=chain : supf→chain x ≡ & chain
-          sc-mono : {a b : Ordinal} → a o< b → supf→chain a o< supf→chain b
+          supr : Ordinal → Ordinal 
+          sc-iso : {z : Ordinal} → z o≤ supr x → supr (supf z) ≡ z -- supr is count of the elemnt of the chain o< A, dense
+          sc=chain : supr x ≡ & chain
+          sc-mono : {a b : Ordinal} → a o< b → supr a o< supr b
+          is-minsup : {z : Ordinal } → (z≤x : z o≤ x) → IsMinSUP A (* (supr z)) (supf z)
 
-       cf-is-<-monotonic : <-monotonic-f A supf
-       cf-is-<-monotonic x ax = ⟪ supf-< ax , asupf ⟫
-       cf-is-≤-monotonic : ≤-monotonic-f A supf 
-       cf-is-≤-monotonic x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic x ax  ))  , proj2 ( cf-is-<-monotonic x ax  ) ⟫
+       <-monotonic : <-monotonic-f A supf
+       <-monotonic x ax = ⟪ supf-< ax , asupf ⟫
+       ≤-monotonic : ≤-monotonic-f A supf 
+       ≤-monotonic x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic x ax  ))  , proj2 ( cf-is-<-monotonic x ax  ) ⟫
+
+     -- starting from chain = ( y , y )
+     -- if x is in CF, but on in the chain add to the chain, and increment supfr
+     --      the chain means previous chain or Union of previous chain
 
      SZ : ¬ Maximal A → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A ay x
      SZ nmx  {y} ay x =  TransFinite {λ z → ZChain A ay z  } (λ x → ind x ) x where
-          ind : (x : Ordinal) → ((z : Ordinal) → z o< x → ZChain A ay z) → ZChain A ay x
-          ind x prev = ?  -- with Oprev-p x
+        ind : (x : Ordinal) → ((z : Ordinal) → z o< x → ZChain A ay z) → ZChain A ay x
+        ind x prev = record {
+                  chain = record { od = record { def = λ x → odef A x ∧ IChain A supf x } ; odmax = & A ; <odmax = λ lt → odef< (proj1 lt) } 
+                ; chain⊆A = λ cx → proj1 cx 
+                ; f-total = λ ia ib → subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (f-total (proj2 ia) (proj2 ib))  
+                ; supf = ?
+                ; asupf = ?
+                ; supf-< = ?
+                ; f-next =  ?
+                ; supr = ?
+                ; sc-iso = ?
+                ; sc=chain = ?
+                ; sc-mono = ?
+                ; is-minsup = ?
+             } where
+          chain : HOD
+          chain = ?
+          chain⊆A : chain ⊆ A
+          chain⊆A = ?
+          f-total  : ?
+          f-total  = ?
+          supf : Ordinal → Ordinal 
+          supf = ?
+          asupf : {z : Ordinal} → odef A (supf z) 
+          asupf = ?
+          supf-< : {z : Ordinal} → odef A z →  * z < * (supf z) 
+          supf-< = ?
+          f-next  : {z : Ordinal } → odef chain z → odef chain (supf z)
+          f-next  = ?
+          supr : Ordinal → Ordinal 
+          supr = ?
+          sc-iso : {z : Ordinal} → supf (supr z) ≡ z
+          sc-iso = ?
+          sc=chain : supr x ≡ & chain
+          sc=chain = ?
+          sc-mono : {a b : Ordinal} → a o< b → supr a o< supr b
+          sc-mono = ?
+          is-minsup : {z : Ordinal } → (z≤x : z o≤ x) → IsMinSUP A (* (supr z)) (supf z)
+          is-minsup = ?
 
 --  record {
---       chain = record { od = record { def = λ x → odef A x ∧ IChain A f x } ; odmax = & A ; <odmax = λ lt → z09 (proj1 lt) } ;
+--       chain = record { od = record { def = λ x → odef A x ∧ IChain A f x } ; odmax = & A ; <odmax = λ lt → odef< (proj1 lt) } ;
 --       chain⊆A = λ cx → proj1 cx ;
 --       f-total = λ ia ib → subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (f-total (proj2 ia) (proj2 ib))  ; 
 --       f-next = λ ix → ⟪ ? , f-next (proj2 ix) ⟫ ;
@@ -344,7 +389,7 @@
            asp = MinSUP.as sp1
            f = ZChain.supf zc
            mf : ≤-monotonic-f A f
-           mf = ZChain.cf-is-≤-monotonic zc
+           mf = ZChain.≤-monotonic zc
            z12 : odef chain sp
            z12 = ? -- ZChain.fixpoint zc sp1
            z14 :  f sp ≡ sp
@@ -374,10 +419,10 @@
            (subst (λ k → odef A k ) (sym &iso) (ZChain.asupf zc ))
            (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
            (case1 ( cong (*)( fixpoint zc msp1  ))) -- x ≡ f x ̄
-                (proj1 (ZChain.cf-is-<-monotonic zc c (MinSUP.as msp1 ))) where          -- x < f x
+                (proj1 (ZChain.<-monotonic zc c (MinSUP.as msp1 ))) where          -- x < f x
 
           msp1 : MinSUP A (ZChain.chain zc)
-          msp1 = msp0 (ZChain.supf zc) (ZChain.cf-is-<-monotonic zc) as0 zc
+          msp1 = msp0 (ZChain.supf zc) (ZChain.<-monotonic zc) as0 zc
           c : Ordinal
           c = MinSUP.sup msp1