--- a/src/zorn.agda	Tue Jun 14 11:08:15 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 14:36:45 2022 +0900
@@ -241,7 +241,6 @@
 record FSup ( A : HOD ) ( f : Ordinal → Ordinal ) (p c : Ordinal)   ( x : Ordinal ) : Set n where
    field
       sup :  (z : Ordinal) → FClosure A f p z → * z < * x 
-      chain∋x : odef (* c) x 
       chain∋p : odef (* c) p 
 
 data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (c : Ordinal) : (x : Ordinal) → Set n where
@@ -261,7 +260,7 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
-      chain∋sup : (s : HOD) → s ⊆' chain → {b : Ordinal} (ab : odef A b)  → IsSup A s ab → odef chain b
+      chain∋sup : (s : HOD) → s ⊆' chain → {b : Ordinal} (ab : odef A b) → b o< z  → IsSup A s ab → odef chain b
       fc∨sup :  {c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A chain∋x) f (& chain) c 
 
 
@@ -419,6 +418,14 @@
           zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
+          ys : HOD
+          ys = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
+          init-chain : ZChain A y f y
+          init-chain = record { chain = ys ; 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
+               i-total : IsTotalOrderSet ys
+               i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
           zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
@@ -601,8 +608,6 @@
                 um01 with FC
                 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
                 ... | Fsup {p} {i} p<i pFC sup = cb∋i where
-                     ca∋i  : odef (chain za) i
-                     ca∋i  = subst (λ k → odef k i) *iso (FSup.chain∋x sup)
                      i-asup : (z : Ordinal) → FClosure A f p z → * z < * i
                      i-asup = FSup.sup sup
                      um06 : odef (chain za) p
@@ -614,11 +619,11 @@
                      um08 : odef (chain zb) p
                      um08 = previ p p<i um06
                      cl : HOD
-                     cl = record { od = record { def = λ x → FClosure A f p x } ; odmax = & A ; <odmax = λ lt → cla lt } where
-                         cla : {i2 : Ordinal} → FClosure A f p i2 → i2 o< & A
-                         cla {i2} cl = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (A∋fc p f mf cl) ) )
+                     cl = record { od = record { def = λ x → FClosure A f p x } ; odmax = & A ; <odmax = cl<A } where
+                         cl<A : {i2 : Ordinal} → FClosure A f p i2 → i2 o< & A
+                         cl<A {i2} cl = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (A∋fc p f mf cl) ) )
                      cb∋i : odef (chain zb) i
-                     cb∋i = ZChain.chain∋sup zb cl (λ {i2} lt → um07 i2 lt) (chain⊆A za zai) record { x<sup = λ {i2} cl → case2 (i-asup i2 cl) } 
+                     cb∋i = ZChain.chain∋sup zb cl (λ {i2} lt → um07 i2 lt) (chain⊆A za zai) {!!} record { x<sup = λ {i2} cl → case2 (i-asup i2 cl) } 
                 ... | Fc {p} {i} p<i pFC FC with (FChain.fc∨sup FC) 
                 ... | fc = um02 i fc where
                      um02 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2