--- a/src/zorn.agda	Sun Jul 10 06:34:54 2022 +0900
+++ b/src/zorn.agda	Sun Jul 10 08:10:34 2022 +0900
@@ -255,7 +255,7 @@
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
     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 ) 
+    ch-is-sup : {x z : Ordinal } (0<x : o∅ o< x) ( 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
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
@@ -291,6 +291,25 @@
 SupCond : ( A B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → Set (Level.suc n)
 SupCond A B _ _ = SUP A B  
 
+-- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
+--
+-- data Chain is total
+
+chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) 
+   {s s1 a b : Ordinal } ( ca : Chain A f mf ay s a ) ( cb : Chain A f mf ay s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
+chain-total A f mf {y} ay {s} {s1} {a} {b} ca cb = TransFinite 
+   {λ x → {s1 a b : Ordinal } ( ca : Chain A f mf ay x a ) ( cb : Chain A f mf ay s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )} ct-ind s ca cb where
+     ct-ind : (x : Ordinal) →
+       ((y₁ : Ordinal) → y₁ o< x → {s1 a b : Ordinal} → Chain A f mf ay y₁ a → Chain A f mf ay s1 b → Tri (* a < * b) (* a ≡ * b) (* b < * a)) 
+       → {s1 a b : Ordinal} → Chain A f mf ay x a → Chain A f mf ay s1 b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
+     ct-ind x prev {s1} {a} {b} (ch-init s a x=0 fca) (ch-init s1 b x=0' fcb) = fcn-cmp y f mf fca fcb
+     ct-ind x prev {s1} {a} {b} (ch-init s a x=0 fca) (ch-is-sup 0<x as supb fcb) = ?
+     ct-ind x prev {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-init s1 b x=0' fcb) = ?
+     ct-ind x prev {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-is-sup 0<x' as' supb fcb) with trio< x s1
+     ... | tri< a₁ ¬b ¬c = ?
+     ... | tri≈ ¬a  refl ¬c = fcn-cmp s1 f mf fca fcb
+     ... | tri> ¬a ¬b c = ?
+
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
     → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition