# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650213187 -32400
# Node ID c02c82656063732669e663b918467dad14cc8b83
# Parent  f351c183e7124860e54fd8112480423985302ebb
...

diff -r f351c183e712 -r c02c82656063 src/zorn.agda
--- a/src/zorn.agda	Mon Apr 18 00:11:24 2022 +0900
+++ b/src/zorn.agda	Mon Apr 18 01:33:07 2022 +0900
@@ -368,12 +368,11 @@
 
 all-climb-case : { A : HOD } → (0<A : o∅ o< & A) → IsPartialOrderSet A
      → (( x : Ordinal ) → (ax : odef A (& (* x))) → OSup> A ax )
-     → InFiniteIChain A (& A) (d→∋ A (ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ))
-all-climb-case {A} 0<A PO climb = record {    c-infinite = ac00 ; chain<x = ac01 }  where
-        x = ODC.minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
-        ax = ODC.x∋minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
+     → (x : HOD) ( ax : A ∋ x )
+     → InFiniteIChain A (& A) (d→∋ A ax)
+all-climb-case {A} 0<A PO climb x ax = record {    c-infinite = ac00 ; chain<x = ac01 }  where
         B = IChainSet A ax
-        ac01 : (y : Ordinal) → odef (IChainSet A (d→∋ A (ODC.x∋minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))))) y → y o< & A 
+        ac01 : (y : Ordinal) → odef (IChainSet A (d→∋ A ax)) y → y o< & A 
         ac01 y ⟪ ay , _ ⟫ = subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) ay) )
         ac00 : (y : Ordinal) (cy : odef (IChainSet A (d→∋ A ax)) y) → IChainSup> A (ic→A∋y A (d→∋ A ax) cy)
         ac00 y cy = record { y = z ; A∋y = az ; y>x = y<z} where
@@ -389,8 +388,6 @@
              y<z  = ic→< {A} PO y (subst (λ k → odef A k) &iso ay) (IChained.iy (proj2 icy))
                (subst (λ k → ic-connect k (IChained.iy (proj2 icy))) &iso (IChained.ic (proj2 icy)))
 
-
-
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
@@ -405,19 +402,26 @@
 Zorn-lemma {A}  0<A PO supP = zorn04 where
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a
-     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
-     z02 : {x : Ordinal } → (ax : A ∋ * x ) → InFiniteIChain A x ax  → ⊥
-     z02 {x} ax ic = zc5 ic where
-              FC : HOD
-              FC = IChainSet A ax
-              zc6 :  InFiniteIChain A x ax  → ¬ SUP A FC 
-              zc6 inf = {!!}
-              FC-is-total : IsTotalOrderSet FC
-              FC-is-total = {!!}
-              FC⊆A :  FC ⊆ A
-              FC⊆A = record { incl = λ {x} lt → proj1 lt }
-              zc5 : InFiniteIChain A x ax → ⊥
-              zc5 x = zc6 x ( supP FC FC⊆A FC-is-total )
+     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl
+          (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
+     s = ODC.minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
+     sa = ODC.x∋minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A))
+     z02 : {x max : Ordinal } → (ax : A ∋ * x ) → InFiniteIChain A max ax  → ⊥
+     z02 {x} {max} ax ifc = zc5 ifc where
+          FC : HOD
+          FC = IChainSet A ax
+          zc6 :  InFiniteIChain A max ax  → ¬ SUP A (InFCSet A ax ifc) 
+          zc6 inf sup = z01 nxa (SUP.A∋maximal sup) (SUP.x<sup sup {!!} ) {!!} where
+              nx : Ordinal
+              nx = cinext A ax ifc (& (SUP.sup sup))
+              nxa : A ∋ * nx
+              nxa = {!!}
+          fct : IsTotalOrderSet (InFCSet A ax ifc)
+          fct = ChainClosure-is-total  A {x} ax PO ifc
+          FC⊆A :  InFCSet A ax ifc ⊆ A
+          FC⊆A = InFCSet⊆A A {x} ax ifc
+          zc5 : InFiniteIChain A max ax → ⊥
+          zc5 ic = zc6 ic ( supP (InFCSet A ax ifc) FC⊆A fct )
      -- ZChain is not compatible with the SUP condition
      ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
          →  ZChain A x ∨ Maximal A