--- a/src/zorn.agda	Tue Jul 05 08:22:32 2022 +0900
+++ b/src/zorn.agda	Fri Jul 08 13:31:19 2022 +0900
@@ -246,9 +246,6 @@
     ch-init    : (x z : Ordinal) → x ≡ o∅ → FClosure A f y z  → Chain A f mf  ay x z 
     ch-is-sup : {x z : Ordinal }  ( ax : odef A x ) 
          → ( is-sup : (x1 w : Ordinal) → x1 o< x → Chain A f mf ay x1 w → w << x )  → ( fc : FClosure A f x z ) → Chain A f mf ay x z
-    ch-noax : {x z p : Ordinal }  ( ax : ¬ odef A x ) → p o< x → ( prev : Chain A f mf ay p z ) →  Chain A f mf ay x z
-    ch-nosup : {x z p : Ordinal }  ( ax : odef A x ) 
-         → ( nosup : ¬ ( (x1 w : Ordinal) → x1 o< x → Chain A f mf ay x1 w → w << x ) ) → ( prev : Chain A f mf ay p z ) → Chain A f mf ay x z
 
 -- Union of supf z which o< x
 --
@@ -256,14 +253,17 @@
    field
       u : Ordinal
       u<x : u o< x
-      chain∋z : Chain A f mf ay u z
+      chain∋z : Chain A f mf ay u z  -- it inclues initial case ch-init
 
 UnionCF : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (x : Ordinal)  → HOD
 UnionCF A f mf ay x = record { od = record { def = λ z → odef A z ∧  UChain A f mf ay x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) ( z : Ordinal )  : Set (Level.suc n) where
+   field
+      sup : Ordinal
+      sup<x : sup o≤ z
    chain : HOD
-   chain = record { od = record { def = λ x →  Chain A f mf ay z x } ; odmax = (& A) ; <odmax = ? }
+   chain = record { od = record { def = λ x →  odef A x ∧ Chain A f mf ay sup x } ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy }
    field
       chainf : (w : Ordinal) → Chain A f mf ay z w 
       chain⊆A : chain ⊆' A
@@ -556,6 +556,10 @@
           uzc = UnionCF A f mf ay x 
           -- c-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → (w<x : w o< x ) → chainf z ? ⊆' chainf w w<x
           -- c-mono {z} {w} z≤w w≤x {i} = ?
+          uz-total : IsTotalOrderSet uzc
+          uz-total {a} {b} x y = uz01 ? ? where
+               uz01 : (Chain A f mf ay ? (& a)) → ? → Tri (a < b) (a ≡ b) (b < a)
+               uz01 = ?
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = ? where -- ¬ A ∋ p, just skip
@@ -586,7 +590,6 @@
               u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
               ... | s | t = {!!}
 
-         
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) 
      SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) (& A)