# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650193138 -32400
# Node ID 8e36b5c35777fcd6b5a435d12b961fbb219c47e6
# Parent  5d3df69d3732b7edb736ca44da1577e6ee7de1ca
...

diff -r 5d3df69d3732 -r 8e36b5c35777 src/zorn.agda
--- a/src/zorn.agda	Sun Apr 17 17:16:23 2022 +0900
+++ b/src/zorn.agda	Sun Apr 17 19:58:58 2022 +0900
@@ -173,9 +173,9 @@
 ic→A∋y : (A : HOD) {x y : Ordinal}  (ax : A ∋ * x) → odef (IChainSet {A} (me ax)) y → A ∋ * y
 ic→A∋y A {x} {y} ax ⟪ ay , _ ⟫ = subst (λ k → odef A k) (sym &iso) ay
 
-record InFiniteIChain (A : HOD) {x : Ordinal}  (ax : A ∋ * x) : Set n where
+record InFiniteIChain (A : HOD) (max : Ordinal) {x : Ordinal}  (ax : A ∋ * x) : Set n where
    field
-      chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< x
+      chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< max
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
           → IChainSup> A (ic→A∋y A ax cy)
 
@@ -205,22 +205,22 @@
 cton : (A : HOD ) (s : Ordinal)   → (next : Ordinal → Ordinal ) → Element (ChainClosure A s next) → ℕ
 cton A s next y = cton0 A s next (is-elm y)
 
-cinext :  (A : HOD) {x : Ordinal } → (ax : A ∋ * x ) → (ifc : InFiniteIChain A ax ) → Ordinal  →  Ordinal
+cinext :  (A : HOD) {x max : Ordinal } → (ax : A ∋ * x ) → (ifc : InFiniteIChain A max ax ) → Ordinal  →  Ordinal
 cinext A ax ifc y with ODC.∋-p O (IChainSet (me ax)) (* y)
 ... | yes ics-y = IChainSup>.y ( InFiniteIChain.c-infinite ifc y (subst (λ k → odef (IChainSet (me ax)) k) &iso ics-y ))
 ... | no _ = o∅
 
-InFCSet : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
-     → (ifc : InFiniteIChain A ax ) → HOD
+InFCSet : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x)
+     → (ifc : InFiniteIChain A max ax ) → HOD
 InFCSet A {x} ax ifc =  ChainClosure (IChainSet {A} (me ax)) x (cinext A ax ifc ) 
 
-InFCSet⊆A : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x) →  (ifc : InFiniteIChain A ax ) → InFCSet A ax ifc ⊆ A
+InFCSet⊆A : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x) →  (ifc : InFiniteIChain A max ax ) → InFCSet A ax ifc ⊆ A
 InFCSet⊆A A {x} ax ifc = record { incl = λ {y} lt → incl (IChainSet⊆A (me ax)) (
      ct∈A (IChainSet {A} (me ax)) x (cinext A ax ifc) lt ) }
 
-ChainClosure-is-total : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
+ChainClosure-is-total : (A : HOD) → {x max : Ordinal}  (ax : A ∋ * x)
      → IsPartialOrderSet A 
-     → (ifc : InFiniteIChain A ax )
+     → (ifc : InFiniteIChain A max ax )
      → IsTotalOrderSet ( InFCSet A ax ifc )
 ChainClosure-is-total A {x} ax PO ifc = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO
    ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
@@ -307,7 +307,7 @@
 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))
+    → (x : Element A) → OSup> A (d→∋ A (is-elm x)) ∨ Maximal A ∨ InFiniteIChain A (& (elm x))  (d→∋ A (is-elm x))
 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
@@ -315,7 +315,7 @@
     HG : HOD
     HG = record { od = record { def = λ y → odef A y ∧ IsFC A (d→∋ A (is-elm x) ) y } ; odmax = & A
         ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A  (proj1 lt) ))  }
-    zc2 :  OSup> A (d→∋ A (is-elm x))  ∨ Maximal A ∨ InFiniteIChain A  (d→∋ A (is-elm x))
+    zc2 :  OSup> A (d→∋ A (is-elm x))  ∨ Maximal A ∨ InFiniteIChain A (& (elm x))  (d→∋ A (is-elm x))
     zc2 with  is-o∅ (& Gtx)
     ... | no not = case1 record { y = & y ; icy = zc4 ; y>x = proj2 zc3 } where
         y : HOD
@@ -379,8 +379,29 @@
 
 all-climb-case : { A : HOD } → (0<A : o∅ o< & A) → IsPartialOrderSet A
      → (( x : Element A) → OSup> A (d→∋ A (is-elm x) ))
-     → InFiniteIChain 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 = {!!}  ; chain<x = {!!} } 
+     → 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 = λ y cy → ac00 (& x) y (proj1 cy) (subst (λ k → IChained A k y  )
+         (cong (&) (me-elm-refl A (me ax))) (proj2 cy))
+    ; 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))
+        B = IChainSet {A} (me (d→∋ A ax))
+        ac01 : (y : Ordinal) → odef (IChainSet {A} (me (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 : (x y : Ordinal) (ay : odef A y) (cy :  IChained A x y) → IChainSup> A (subst (λ k → odef A k ) (sym &iso) ay )
+        ac00 x y ay cy = record { y = z ; A∋y = az ; y>x = {!!} } where
+             z : Ordinal
+             z = OSup>.y ( climb (me (subst (λ k → odef A k ) (sym &iso) ay) ) )
+             az : odef A z
+             icy :  odef (IChainSet {A} (me (subst (λ k → odef A k ) {!!} ay))) z
+             icy  = OSup>.icy ( climb (me (subst (λ k → odef A k ) (sym &iso) ay) ) )
+             az = {!!}
+             -- incl (IChainSet⊆A {A} ? ) (subst (λ k → odef (IChainSet {A} ? ) k ) ? (OSup>.icy ( climb (me (subst (λ k → odef A k ) (sym &iso) ay) ) )))
+             - = OSup>.y ( climb (me (subst (λ k → odef A k ) (sym &iso) ay) ) )
+             -- iy0 : IChained A (& (* (& (ODC.minimal O A (λ eq → ¬x<0 (subst (_o<_ o∅) (=od∅→≡o∅ eq) 0<A)))))) ?
+             -- iy0 = iy 
+
+
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
@@ -397,17 +418,17 @@
      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  ax  → ⊥
+     z02 : {x : Ordinal } → (ax : A ∋ * x ) → InFiniteIChain A x ax  → ⊥
      z02 {x} ax ic = zc5 ic where
               FC : HOD
               FC = IChainSet {A} (me ax)
-              zc6 :  InFiniteIChain A ax  → ¬ SUP A FC 
+              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 ax → ⊥
+              zc5 : InFiniteIChain A x ax → ⊥
               zc5 x = zc6 x ( supP FC FC⊆A FC-is-total )
      -- ZChain is not compatible with the SUP condition
      ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
@@ -434,24 +455,24 @@
           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
+          ... | case2 (case2 ex) = ⊥-elim (zc5 {!!} ) where
               FC : HOD
               FC = IChainSet {A} (me ax)
-              B : InFiniteIChain A ax  → HOD
+              B : InFiniteIChain A x ax  → HOD
               B ifc =  InFCSet A ax ifc
-              zc6 :  (ifc : InFiniteIChain A ax ) → ¬ SUP A (B ifc)
+              zc6 :  (ifc : InFiniteIChain A x ax ) → ¬ SUP A (B ifc)
               zc6 = {!!}
-              FC-is-total : (ifc : InFiniteIChain A ax)  → IsTotalOrderSet (B ifc)
+              FC-is-total : (ifc : InFiniteIChain A x ax)  → IsTotalOrderSet (B ifc)
               FC-is-total ifc = ChainClosure-is-total A ax PO ifc 
-              B⊆A : (ifc : InFiniteIChain A ax)  →   B ifc ⊆ A
+              B⊆A : (ifc : InFiniteIChain A x ax)  →   B ifc ⊆ A
               B⊆A = {!!}
-              ifc : InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax) → InFiniteIChain A ax
+              ifc : InFiniteIChain A x (subst (OD.def (od A)) (sym &iso) ax) → InFiniteIChain A x ax
               ifc record {  c-infinite = c-infinite } = record {  c-infinite = {!!} }  where
                   ifc01 : {!!} -- me (subst (OD.def (od A)) (sym &iso) ax)
                   ifc01 = {!!}
                -- (y : Ordinal) → odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) ax))) y → y o< & (* x₁)
                --  (y : Ordinal) → odef (IChainSet (me ax)) y → y o< x₁
-              zc5 : InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax) → ⊥
+              zc5 : InFiniteIChain A x (subst (OD.def (od A)) (sym &iso) ax) → ⊥
               zc5 x = zc6 (ifc x) ( supP (B (ifc x)) (B⊆A (ifc x)) (FC-is-total (ifc x) ))
      ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = {!!} where