--- a/src/zorn.agda	Sun Jul 10 10:08:59 2022 +0900
+++ b/src/zorn.agda	Sun Jul 10 10:51:30 2022 +0900
@@ -264,15 +264,12 @@
       p≤z : (x : Ordinal ) →   odef A (psup x)
       chainf : (x : Ordinal) → HOD
       is-chain : (x w : Ordinal) → odef (chainf x) w → Chain A f mf ay (psup x ) w 
-      psup-mono : (x : Ordinal) → (x≤z : x o≤ z ) → chainf x ⊆' chainf z 
 
 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
    chain : HOD
    chain = ZChain1.chainf (zc0 (& A)) z 
    field
-      chain-mono : (px py : Ordinal) → (x≤y : px o≤ py ) (y≤z : py o≤ z ) → (w : Ordinal ) 
-          → ZChain1.chainf (zc0 (& A)) px   ⊆' ZChain1.chainf (zc0 (& A)) py 
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
@@ -465,7 +462,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 ; psup-mono = sc0 }  where
+          no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? z x
             ... | yes _ = ZChain1.psup sc z
@@ -478,8 +475,6 @@
             chainf1 z with o≤? z x
             ... | yes _  = ZChain1.chainf sc z
             ... | no _ = ZChain1.chainf sc x
-            sc0 : (z : Ordinal) → z o≤ x → chainf1 z ⊆' chainf1 x
-            sc0 z = ?
             is-chain1 : ?
             is-chain1 = ?
           sc4 : ZChain1 A f mf ay x
@@ -488,7 +483,7 @@
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
           ... | case1 pr = no-ext
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? ; psup-mono = ? } where
+          ... | case1 is-sup = record { psup = ? ; p≤z = ? ; chainf = ? ; is-chain = ? } where
                 schain : HOD
                 schain = ? -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
                     -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
@@ -507,11 +502,12 @@
                                             (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)
           sc4 :  ZChain1 A f mf ay x
-          sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 ; psup-mono = sc0 }  where
+          sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? x z
-            ... | yes _ = & (SUP.sup usup)
+            ... | yes _ = spu
             ... | no z<x = ZChain1.psup (pzc z (o¬≤→< z<x)) z
             p≤z1 : (z : Ordinal ) → odef A (psup1 z)
             p≤z1 z with o≤? x z
@@ -519,16 +515,19 @@
             ... | no z<x  = ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
             chainf1 : (z : Ordinal ) → HOD
             chainf1 z with o≤? x z
-            ... | yes _  = UZ
+            ... | yes _  = record { od = record { def = λ w → odef A w ∧ (odef UZ w ∨ FClosure A f spu w ) } ; odmax = & A ; <odmax = ? }
             ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
-            sc0 : (z : Ordinal) → z o≤ x → chainf1 z ⊆' chainf1 x
-            sc0 z z≤x {i} lt with o≤? x z
-            ... | yes _ = ?
-            ... | no z<x = ? where -- subst (λ k → odef k i) refl sc1 where
-                sc1 : odef (ZChain1.chainf (pzc z (o¬≤→< z<x)) z) i
-                sc1 = ZChain1.psup-mono (pzc z (o¬≤→< z<x)) _ o≤-refl lt
-            is-chain1 : ?
-            is-chain1 = ?
+            is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay (psup1 z ) w
+            is-chain1 z w lt with o≤? x z
+            ... | no z<x = ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w lt
+            is-chain1 z w ⟪ aw , case1 uz ⟫   | yes _ = subst (λ k → Chain A f mf ay k w) ? uz02  where
+                uz02 : Chain A f mf ay (ZChain1.psup (pzc (UChain.u (proj2 uz)) (UChain.u<x (proj2 uz))) (UChain.u (proj2 uz))) w
+                uz02 = (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 uz))) _ _  (UChain.chain∋z (proj2 uz) ))
+            is-chain1 z w ⟪ aw , case2 uzfc ⟫ | yes _ = ch-is-sup ? ? is-sup uzfc where
+                0<s : ?
+                0<s = ?
+                is-sup : (x1 w₁ : Ordinal) → x1 o< & (SUP.sup usup) → Chain A f mf ay x1 w₁ → w₁ << & (SUP.sup usup)
+                is-sup = ?
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x)