--- a/src/zorn.agda	Fri Apr 15 18:27:04 2022 +0900
+++ b/src/zorn.agda	Fri Apr 15 20:02:12 2022 +0900
@@ -161,11 +161,14 @@
 
 -- finite IChain
 
+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
    field
       chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< x
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
-          → IChainSup> A ax
+          → IChainSup> A (ic→A∋y A ax cy)
 
 open import Data.Nat hiding (_<_) 
 import Data.Nat.Properties as NP
@@ -183,6 +186,8 @@
 cton0 A next (csuc x ax z) = suc (cton0 A next z)
 cton : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → Element (ChainClosure A next) → ℕ
 cton A next y = cton0 A next (is-elm y)
+ct∈A : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → {x : Ordinal} → Chain A next x → odef A x
+ct∈A = {!!}
 
 InFCSet : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → (ifc : InFiniteIChain A ax ) → HOD
@@ -196,10 +201,19 @@
    ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
     IPO : IsPartialOrderSet (InFCSet A ax ifc )
     IPO = ⊆-IsPartialOrderSet record { incl = λ {x} lt → {!!} } PO
-    cnext :  (y : Ordinal ) → odef (IChainSet {A} (me ax)) y → Ordinal
+    B = IChainSet {A} (me ax)
+    cnext :  (y : Ordinal ) → odef B y → Ordinal
     cnext y ay = IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay  )
+    ct-monotonic : {ox oy : Ordinal} → (x : Chain B cnext ox ) → (y : Chain B cnext oy )
+       → (cton0 B cnext x) Data.Nat.< (cton0 B cnext y) → * ox < * oy
+    ct-monotonic x (csuc oy ax y) (s≤s lt) with NP.<-cmp ( cton0 B cnext x ) ( cton0 B cnext y )
+    ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO {me {!!}} {me {!!}} (ct-monotonic x y a ) ct01  where
+        ct01 : * oy < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy ax) )
+        ct01 = (IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy ax))
+    ... | tri≈ ¬a b ¬c = {!!}
+    ... | tri> ¬a ¬b c = {!!}
     cmp : Trichotomous _ _ 
-    cmp x y with NP.<-cmp (cton (IChainSet {A} (me ax)) cnext x) (cton (IChainSet {A} (me ax)) cnext y)
+    cmp x y with NP.<-cmp (cton B cnext x) (cton B cnext y)
     ... | tri< a ¬b ¬c = {!!}
     ... | tri≈ ¬a b ¬c = {!!}
     ... | tri> ¬a ¬b c = {!!}
@@ -336,14 +350,18 @@
           ... | 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 
+              B : InFiniteIChain A ax  → HOD
+              B ifc =  InFCSet A ax ifc
+              zc6 :  (ifc : InFiniteIChain A ax ) → ¬ SUP A (B ifc)
               zc6 = {!!}
-              FC-is-total : IsTotalOrderSet FC
-              FC-is-total = {!!}
-              FC⊆A :  FC ⊆ A
-              FC⊆A = {!!}
+              FC-is-total : (ifc : InFiniteIChain A 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 (subst (OD.def (od A)) (sym &iso) ax) → InFiniteIChain A ax
+              ifc record { chain<x = chain<x ; c-infinite = c-infinite } = record { chain<x = ? ; c-infinite = ? } 
               zc5 : InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax) → ⊥
-              zc5 x = zc6 x ( supP FC FC⊆A FC-is-total )
+              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
           zc1 : ZChain A (& A)