--- a/src/zorn.agda	Sat Dec 10 17:41:17 2022 +0900
+++ b/src/zorn.agda	Sun Dec 11 08:48:42 2022 +0900
@@ -276,11 +276,22 @@
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z
     ch-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z
 
-UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
+UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
 UnionCF A f ay supf x
    = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ;
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
+-- Union of all UChain under limit ordinal x
+
+data IChain  { A : HOD } { f : Ordinal → Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal)  {y : Ordinal } (ay : odef A y )
+       (x : Ordinal) : (z : Ordinal) → Set n where
+    ic-init : {z : Ordinal } (fc : FClosure A f y z) → IChain supf ay x z
+    ic-is-sup  : (u : Ordinal) {z : Ordinal }  (u<x : u o< x) (supu=u : supf u<x u ≡ u) ( fc : FClosure A f (supf u<x u) z ) → IChain supf ay x z
+
+UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) (supfz : {z : Ordinal } → z o< x → Ordinal) ( x : Ordinal ) → HOD
+UnionIC A f ay supf x
+   = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} supf ay x z } ;
+       odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
    → supf x o< supf y → x o<  y
@@ -507,12 +518,6 @@
       as : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
-record IChain  (A : HOD)  ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
-  field
-     i : Ordinal
-     i<x : i o< x
-     fc : FClosure A f (supfz i<x) z
-
 --
 -- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup
 --
@@ -1240,8 +1245,8 @@
               mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
                  mf00 : * x < * (f x)
                  mf00 = proj1 ( mf< x ax )
-     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = ? ; supf-mono = supf-mono ; order = ?
-              ; zo≤sz = λ _ → ?   ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
+     ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ?
+              ; zo≤sz = ?   ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
           -- mf : ≤-monotonic-f A f
           -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫  will result memory exhaust