--- a/src/zorn.agda	Mon Jul 11 05:50:49 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 11:49:11 2022 +0900
@@ -278,7 +278,7 @@
       psup :  Ordinal → Ordinal 
       p≤z : (x : Ordinal ) →   odef A (psup x)
       chainf : (x : Ordinal) → HOD
-      is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x) w → Chain A f mf ay chainf (psup x) w 
+      is-chain : {x w : Ordinal} → odef (chainf x) w → Chain A f mf ay chainf (psup x) w 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
@@ -307,9 +307,9 @@
 --
 -- data Chain is total
 
-chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD)
+chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD)
    {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {x} {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
+chain-total A f mf {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
@@ -483,7 +483,7 @@
           pchain  = chainf sc px 
 
           no-ext :  ZChain1 A f mf ay x
-          no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 }  where
+          no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = ? }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? z x
             ... | yes _ = ZChain1.psup sc z
@@ -517,15 +517,40 @@
           UZ : HOD
           UZ = UnionCF A x pchainf
           chainf0 : (z : Ordinal ) → HOD
-          chainf0 z with o≤? x z
-          ... | yes _  = UZ
-          ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
+          chainf0 z with trio< z x
+          ... | tri< a ¬b ¬c = ZChain1.chainf (pzc z a) z
+          ... | tri≈ ¬a b ¬c = UZ
+          ... | tri> ¬a ¬b c = UZ
+          Chain-ext : {s a : Ordinal}  → (ca : odef UZ a)
+             → Chain A f mf ay ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca)))) s a → Chain A f mf ay chainf0 s a 
+          Chain-ext {s} {a} ca (ch-init a x) = ch-init a x
+          Chain-ext {s} {a} ca (ch-is-sup is-sup fc) = ch-is-sup sc5 fc where
+              sc7 : odef ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca))) s ) a
+              sc7 = ChainP.csupz is-sup
+              sc8  : (z<x : s o< x ) → chainf0 s ≡ ( ZChain1.chainf (pzc _ z<x )) s
+              sc8  z<x with  trio< s x
+              ... | tri≈ ¬a b ¬c = ?
+              ... | tri> ¬a ¬b c = ?
+              ... | tri< a ¬b ¬c with o<-irr a z<x 
+              ... | refl = refl 
+              sc6 : odef (chainf0 s) a
+              sc6 with trio< s x 
+              ... | tri≈ ¬a b ¬c = ?
+              ... | tri> ¬a ¬b c = ?
+              ... | tri< a' ¬b ¬c with o<-irr a' ? -- (UChain.u<x (proj2 ca))
+              ... | eq = ? -- ChainP.csupz is-sup 
+              sc5 : ChainP A f mf ay chainf0 s a
+              sc5 = record {
+                  asup = ChainP.asup is-sup
+                ; fcy<sup = ChainP.fcy<sup is-sup
+                ; csupz = sc6
+                ; order = ? }
           total-UZ : IsTotalOrderSet UZ
           total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay chainf0 {!!} {!!}
-                   -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  (UChain.chain∋z (proj2 ca))) 
-                   -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  (UChain.chain∋z (proj2 cb)))
+               uz01 = chain-total A f mf ay chainf0  
+                   (Chain-ext ca (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) (UChain.chain∋z (proj2 ca)))) 
+                   (Chain-ext cb (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) (UChain.chain∋z (proj2 cb)))) 
           usup : SUP A UZ
           usup = supP UZ (λ lt → proj1 lt) total-UZ 
           spu = & (SUP.sup usup)