# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655198657 -32400
# Node ID 9bdb671cbffd6c2d368c2518801d48e15f3a5d4f
# Parent  b42f0e50a8311b2a3ac6dd0aebda65116c9eea53
...

diff -r b42f0e50a831 -r 9bdb671cbffd src/zorn.agda
--- a/src/zorn.agda	Tue Jun 14 16:05:25 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 18:24:17 2022 +0900
@@ -286,10 +286,6 @@
 Zorn-lemma {A}  0<A supP = zorn00 where
      supO : (C : HOD ) → C ⊆' A → IsTotalOrderSet C → Ordinal
      supO C C⊆A TC = & ( SUP.sup ( supP  C  C⊆A TC ))
-     postulate
-        --- irrelevance of ⊆' and compare
-        sup== : {C C1 : HOD } → C ≡ C1 → {c  : C ⊆' A } {c1 : C1 ⊆' A } → {t  : IsTotalOrderSet C } {t1 : IsTotalOrderSet C1 }
-         → SUP.sup ( supP  C c t )  ≡  SUP.sup ( supP  C1 c1 t1 )
      <-irr0 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      <-irr0 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -328,6 +324,10 @@
      ... | 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 )
@@ -407,9 +407,18 @@
      init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
      init-chain {y} {x} ay f mf x≤y = record { chain = ys ay f mf ; chain⊆A = λ fx →  A∋fc y f mf fx
                      ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx ; chain∋sup = {!!}
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = {!!} ; fc∨sup = {!!} } where
+                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = is-max ; fc∨sup = it01 } where
                i-total : IsTotalOrderSet (ys ay f mf )
                i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
+               is-max : {a b : Ordinal} → odef (ys ay f mf) a →
+                    b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
+                    * a < * b → odef (ys ay f mf) b
+               is-max {a} {b} yca b≤x ab P a<b = {!!}
+               it01 : {c : Ordinal} → odef (ys ay f mf) c → Fc∨sup A (A∋fc y f mf (init ay)) f (& (ys ay f mf)) x c
+               it01 {c} cc = Fsup {!!} (Finit refl) record { fc∨sup = {!!} ; chain∋p = {!!} } {!!}
+               initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
+               initial {i} (init ai) = case1 refl
+               initial .{f x} (fsuc x lt) = {!!}
 
      --
      -- create all ZChains under o< x
@@ -445,7 +454,7 @@
           ... | no noax =  -- ¬ A ∋ p, just skip
                  record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
                      ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 ; chain∋sup = {!!}
-                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} }  where -- no extention
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = zc12 }  where -- no extention
                 zc12 : {c : Ordinal} → odef (ZChain.chain zc0) c → Fc∨sup A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) f (& (ZChain.chain zc0)) x c
                 zc12 {c} cc = fcs< A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) (& (ZChain.chain zc0)) px c px<x (ZChain.fc∨sup zc0 cc)
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -660,7 +669,7 @@
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
          -- yes we have the maximal
          zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
-         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
+         zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))   -- Axiom of choice
          zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
          zorn01  = proj1  zorn03  
          zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)