--- a/src/zorn.agda	Fri Jun 17 21:45:33 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 21:50:50 2022 +0900
@@ -233,32 +233,23 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record SupF (A : HOD) : Set n where
+record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (supf : Ordinal → SupF A) ( z : Ordinal ) : Set (Level.suc n) where
    field
-      chain : Ordinal
-      -- sup : Ordinal 
-      -- asup : odef A sup
-      -- is-sup :  IsSup A (* chain) asup
-
-record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (supf : Ordinal → SupF A) ( z : Ordinal ) : Set (Level.suc n) where
-   chain : HOD
-   chain = * (SupF.chain (supf z ))
-   field
+      chain : HOD
       chain⊆A : chain ⊆' A
       chain∋x : odef chain x
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
-      f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
       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
 
-record ZChain1 ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal )  ( z : Ordinal ) : Set (Level.suc n) where
-   field
-      supf : Ordinal → SupF A
-      zc : ZChain A x f supf z
-      chain-mono : {x y : Ordinal} → x o≤ y → y o< osuc z →  * (SupF.chain (supf x )) ⊆' * (SupF.chain (supf y ))
+chain-mono ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal )  ( z : Ordinal )
+   → {x y : Ordinal} (zx : ZChain A x f z ) → (zy : ZChain A y f z)  → x o≤ y → y o< osuc z →  * (ZChain.chain zx) ⊆' * (ZChain.chain zy )
+
+f-total  ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal )  ( z : Ordinal )
+   → {x y : Ordinal} (zx : ZChain A x f z ) → IsTotalOrderSet (ZChain.chain zx )
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field