# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656539825 -32400
# Node ID 4186c0331abb3b8108092ca666c313bdf439e9c6
# Parent  cf5af048db99fa0d4959350751b0b2977491c090
sind again

diff -r cf5af048db99 -r 4186c0331abb src/OrdUtil.agda
--- a/src/OrdUtil.agda	Sat Jun 25 17:36:18 2022 +0900
+++ b/src/OrdUtil.agda	Thu Jun 30 06:57:05 2022 +0900
@@ -41,9 +41,6 @@
 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
 
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
-----   y < osuc y < x < osuc x
-----   y < osuc y = x < osuc x
-----   y < osuc y > x < osuc x   -> y = x ∨ x < y → ⊥
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
@@ -57,6 +54,11 @@
 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
 
+ordtrans≤-< :  {ox oy oz : Ordinal } → ox o< osuc oy  → oy o< oz  → ox o< oz
+ordtrans≤-< {ox} {oy} {oz} x≤y y<z with  osuc-≡< x≤y
+... | case1 x=y = subst ( λ k → k o< oz ) (sym x=y) y<z
+... | case2 x<y = ordtrans x<y y<z
+
 open _∧_
 
 osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
@@ -74,6 +76,12 @@
 _o≤_ :  Ordinal → Ordinal → Set  n
 a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
 
+o<→≤ : {a b : Ordinal} → a o< b → a o≤ b
+o<→≤ {a} {b} lt with trio< a (osuc b)
+... | tri< a₁ ¬b ¬c = a₁
+... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a (ordtrans lt <-osuc ) )
+... | tri> ¬a ¬b c  = ⊥-elim (¬a (ordtrans lt <-osuc ) )
+
 -- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1
 
 xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
diff -r cf5af048db99 -r 4186c0331abb src/ordinal.agda
--- a/src/ordinal.agda	Sat Jun 25 17:36:18 2022 +0900
+++ b/src/ordinal.agda	Thu Jun 30 06:57:05 2022 +0900
@@ -1,13 +1,13 @@
-open import Level
+open import Level 
 module ordinal where
 
 open import logic
 open import nat
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Definitions
-open import Data.Nat.Properties 
+open import Data.Nat.Properties as NP
 open import Relation.Nullary
 open import Relation.Binary.Core
 
@@ -16,30 +16,30 @@
 -- Countable Ordinals
 --
 
-data OrdinalD {n : Level} :  (lv : Nat) → Set n where
-   Φ : (lv : Nat) → OrdinalD  lv
-   OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
+data OrdinalD {n : Level} :  (lv : ℕ) → Set n where
+   Φ : (lv : ℕ) → OrdinalD  lv
+   OSuc : (lv : ℕ) → OrdinalD {n} lv → OrdinalD lv
 
 record Ordinal {n : Level} : Set n where
    constructor ordinal  
    field
-     lv : Nat
+     lv : ℕ
      ord : OrdinalD {n} lv
 
-data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
-   Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
-   s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
+data _d<_ {n : Level} :   {lx ly : ℕ} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
+   Φ<  : {lx : ℕ} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
+   s<  : {lx : ℕ} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
 
 open Ordinal
 
 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
 _o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
 
-s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
+s<refl : {n : Level } {lx : ℕ } { x : OrdinalD {n} lx } → x d< OSuc lx x
 s<refl {n} {lv} {Φ lv}  = Φ<
 s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
 
-trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
+trio<> : {n : Level} →  {lx : ℕ} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
 trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
 
@@ -56,16 +56,16 @@
       lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
 ordinal-cong refl refl = refl
 
-≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
+≡→¬d< : {n : Level} →  {lv : ℕ} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
 ≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
 
-trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
+trio<≡ : {n : Level} →  {lx : ℕ} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
 trio<≡ refl = ≡→¬d<
 
-trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
+trio>≡ : {n : Level} →  {lx : ℕ} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
 trio>≡ refl = ≡→¬d<
 
-triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
+triOrdd : {n : Level} →  {lx : ℕ}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
 triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
 triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
@@ -97,7 +97,7 @@
 o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = 
    o<> (case2 y<x) (case2 x<y)
 
-orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
+orddtrans : {n : Level} {lx : ℕ} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
 
@@ -163,11 +163,11 @@
 open _∧_
 
 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
-  → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
-  → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
+  → ( ∀ (lx : ℕ ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
+  → ( ∀ (lx : ℕ ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
-  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
+  TransFinite1 : (lx : ℕ) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
   TransFinite1 Zero (Φ 0) = ⟪  caseΦ Zero lemma , lemma1 ⟫ where
       lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
       lemma x (case1 ())
@@ -176,9 +176,9 @@
       lemma1 x (case1 ())
       lemma1 x (case2 ())
   TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where
-      lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
+      lemma0 : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
       lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
-      lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
+      lemma : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
       lemma lx1 ox1            (case1 lt) with <-∨ lt
       lemma lx (Φ lx)          (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
       lemma lx (Φ lx)          (case1 lt) | case2 lt1 = lemma0  lx (Φ lx) (case1 lt1)
@@ -200,17 +200,34 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
-open import Data.Nat.Properties as DP
 OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (DP.<-irrelevant _ _ )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ )
 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
 OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl
 OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
-      lemma1 : {lx : Nat} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
+      lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
       lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl
       lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y )
+
+TransFinite3 : {n m : Level} { ψ : Ordinal {suc n} → Set m }
+          → ( (x : Ordinal {suc n})  → ( (y : Ordinal {suc n}  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : Ordinal {suc n} )  → ψ x
+TransFinite3 {n} {m} {ψ} ind x = TransFinite {n} {m} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : ℕ) → ((x₁ : Ordinal {suc n}) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev 
+
+-- TP : {n m l : Level} → {Q : Ordinal {suc n} → Set m} {P : { x y : Ordinal {suc n} } → Q x → Q y → Set l}  
+--     → ( ind : (x : Ordinal {suc n})  → ( (y : Ordinal  {suc n} ) → y o< x → Q y ) → Q x )                                                                 
+--     → ( (x : Ordinal {suc n} )  → ( prev : (y : Ordinal {suc n} ) → y o< x → Q y ) → {y : Ordinal {suc n}} → (y<x : y o< x)  → P (prev y y<x) (ind x prev)  )  
+--     →  {x z : Ordinal {suc n} } → (z≤x : z o< osuc x ) → P (TransFinite3 {n} {m} { λ x → Q x } {!!} x  )  {!!} -- P (TransFinite {?} ind z) (TransFinite {?} ind x )
+-- TP = ?
  
+
 open import Ordinals 
 
 C-Ordinal : {n : Level} →  Ordinals {suc n} 
@@ -250,7 +267,7 @@
          lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl
          lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl
          lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
-             lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
+             lemma3 : {n l : ℕ} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
              lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
      open Oprev
      Oprev-p  : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n})  osuc x )
@@ -263,13 +280,13 @@
      TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x
-     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
-        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+     TransFinite2 {ψ} ind x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : ℕ) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
             ψ (record { lv = lx ; ord = Φ lx })
-        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
-        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+        caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
-        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
+        caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev 
 
 
 -- H-Ordinal : {n : Level} → Ordinals {suc n} →  Ordinals {suc n}  →  Ordinals {suc n} 
diff -r cf5af048db99 -r 4186c0331abb src/zorn.agda
--- a/src/zorn.agda	Sat Jun 25 17:36:18 2022 +0900
+++ b/src/zorn.agda	Thu Jun 30 06:57:05 2022 +0900
@@ -230,23 +230,37 @@
       x=fy :  x ≡ f y 
 
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
-   field
+   ield
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain1 ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf : Ordinal → HOD
+      chain-mono : {x : Ordinal} → x o≤ z → supf x ⊆' supf z 
+
+ZChain0 : (A : HOD ) → Set (Level.suc n)
+ZChain0 A = ZChain1 ( & A )
+
+record ZChain ( A : HOD )  (init : Ordinal)  ( f : Ordinal → Ordinal ) (zc0 : ZChain0 A ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = supf z 
+   chain = ZChain1.supf zc0 z 
    field
       chain⊆A : chain ⊆' A
-      chain∋x : odef chain x
-      initial : {y : Ordinal } → odef chain y → * x ≤ * y
+      chain∋init : odef chain init
+      initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
+      f-total : {x : Ordinal} → IsTotalOrderSet chain
       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
-      pmono : (x : Ordinal ) → x o≤ z → supf x ⊆' supf z
+
+record UZFChain ( A : HOD )  ( f : Ordinal → Ordinal ) (zc0 : ZChain0 A ) (x y  : Ordinal) 
+         (prev : (z : Ordinal) → z o< x → ZChain A y f zc0 z) (z : Ordinal) : Set n where 
+   -- Union of ZFChain from y which has maximality o< x
+   field
+      u : Ordinal
+      u<x : u o< x
+      chain∋z : odef (ZChain.chain (prev u u<x  )) z
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -319,20 +333,21 @@
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) ) (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
-     sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total 
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain0 A) (zc : ZChain A (& s) f zc0 (& A) ) 
+        (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
+     sp0 f mf zc0 zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain0 A ) (zc : ZChain A (& s) f zc0 (& A) )
             → (total : IsTotalOrderSet (ZChain.chain zc) )
-            → f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc  total))
-     fixpoint f mf zc total = z14 where
+            → f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc  total))
+     fixpoint f mf zc0 zc total = z14 where
            chain = ZChain.chain zc
-           sp1 = sp0 f mf zc total
+           sp1 = sp0 f mf zc0 zc total
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
               →  HasPrev A chain ab f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
@@ -341,11 +356,11 @@
            z11 = c<→o< ( SUP.A∋maximal sp1)
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
-           ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)
+           ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
-               z13 with SUP.x<sup sp1 ( ZChain.chain∋x zc )
+               z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
                z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.A∋maximal sp1)
@@ -355,7 +370,7 @@
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
                    -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
-           z14 :  f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total ))
+           z14 :  f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total ))
            z14 with total (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
@@ -376,92 +391,59 @@
      -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
-     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
-     z04 nmx zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
+     z04 :  (nmx : ¬ Maximal A ) → (zc0 : ZChain0 A) (zc : ZChain A (& s) (cf nmx) zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
+     z04 nmx zc0 zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc0 zc total ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where          -- x < f x
           sp1 : SUP A (ZChain.chain zc)
-          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc0 zc total
           c = & (SUP.sup sp1)
 
      --
      -- create all ZChains under o< x
      --
 
-     ys : {y : Ordinal} → (ay : odef A y)  (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD
-     ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
-     init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
-     init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx →  A∋fc y f mf fx
-                     ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf 
-                     ; initial = {!!} ; chain∋x  = init ay ; is-max = is-max ; pmono = {!!} } where
-               i-total : IsTotalOrderSet (ys ay f mf )
-               i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
-               is-max : {a b : Ordinal} → odef (ys ay f mf) a →
-                    b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
-                    * a < * b → odef (ys ay f mf) b
-               is-max {a} {b} yca b≤x ab P a<b = {!!}
-               initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
-               initial {i} (init ai) = case1 refl
-               initial .{f x} (fsuc x lt) = {!!}
-
-     record ZChain0 ( A : HOD ) : Set (Level.suc n) where
-        field
-           chain : HOD
-           chain⊆A : chain ⊆' A
-
      sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → ZChain0 A ) → ZChain0 A
+         → ((z : Ordinal) → z o< x → ZChain1 z ) → ZChain1 x
      sind f mf {y} ay x prev  with Oprev-p x
      ... | yes op = sc4 where
           px = Oprev.oprev op
-          sc : ZChain0 A
+          sc : ZChain1 px
           sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
 
-          sc4 : ZChain0 A
+          sc4 : ZChain1 x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = sc
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain0.chain sc) ax f )   
-          ... | case1 pr = sc
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain0.chain sc) ax )
-          ... | case1 is-sup = record { chain =  schain ; chain⊆A = {!!} } where
+          ... | no noax = ?
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.supf sc x) ax f )   
+          ... | case1 pr = ?
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.supf sc x) ax )
+          ... | case1 is-sup = ? where
                 -- A∋sc -- x is a sup of zc 
-                sup0 : SUP A (ZChain0.chain sc )
+                sup0 : SUP A (ZChain1.supf sc x )
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → (ZChain0.chain sc) ∋ y → (y ≡ * x) ∨ (y < * x)
+                        x21 :  {y : HOD} → (ZChain1.supf sc x) ∋ y → (y ≡ * x) ∨ (y < * x)
                         x21 {y} zy with IsSup.x<sup is-sup zy 
                         ... | case1 y=x = case1 (subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x)  )
                         ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x  )
                 sp : HOD
                 sp = SUP.sup sup0 
                 schain : HOD
-                schain = record { od = record { def = λ x → odef (ZChain0.chain sc) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-          ... | case2 ¬x=sup = sc
-     ... | no ¬ox with trio< x y
-     ... | tri< a ¬b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}}  ; chain⊆A = {!!}  }
-     ... | tri≈ ¬a b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}}  ; chain⊆A = {!!}  }
-     ... | tri> ¬a ¬b y<x = record { chain = Uz ; chain⊆A = {!!} } where
-         record Usup (z : Ordinal) : Set n where -- Union of supf from y which has maximality o< x
-            field
-               u : Ordinal
-               u<x : u o< x
-               chain∋z : odef (ZChain0.chain (prev u u<x )) z
-         Uz : HOD
-         Uz = record { od = record { def = λ y → Usup y } ; odmax = & A
-             ; <odmax = {!!} } -- λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
+                schain = record { od = record { def = λ x → odef (ZChain1.supf sc x) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
+          ... | case2 ¬x=sup = ?
+     ... | no ¬ox = ? 
 
-
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → ZChain A y f z) → ZChain A y f x
-     ind f mf {y} ay x prev with Oprev-p x
+     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (zc0 : ZChain0 A) → (x : Ordinal)
+         → ((z : Ordinal) → z o< x → ZChain A y f zc0 z) → ZChain A y f zc0 x
+     ind f mf {y} ay zc0 x prev with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
           supf : Ordinal → HOD
-          supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) )
-          zc : ZChain A y f (Oprev.oprev op)
+          supf = ZChain1.supf zc0
+          zc : ZChain A y f zc0 (Oprev.oprev op)
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
@@ -472,13 +454,13 @@
           --
           no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
-                            * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f x
-          no-extenion is-max = record { supf = supf0 ;  chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc)
-                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc)
-                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc) 
-                     ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc) ; pmono = {!!} 
+                            * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f zc0 x
+          no-extenion is-max = record { supf = supf0 ;  chain⊆A = subst (λ k → k ⊆' A ) ? (ZChain.chain⊆A zc)
+                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) ? (ZChain.initial zc)
+                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) ? (ZChain.f-next zc) 
+                     ; chain∋init  = subst (λ k → odef k y ) ? (ZChain.chain∋init  zc) ; pmono = {!!} 
                              ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
-                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max } where
+                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) ? is-max } where
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
                 ... | tri< a ¬b ¬c = supf z
@@ -495,7 +477,7 @@
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
-          zc4 : ZChain A y f x 
+          zc4 : ZChain A y f zc0 x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
                 zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
@@ -504,7 +486,7 @@
                 zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
                 ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt)  ab P a<b
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf supO x
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
           ... | case1 pr = no-extenion zc7  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 chain0 = ZChain.chain zc
                 zc7 :  {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
@@ -516,7 +498,7 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = {!!} ; f-next = {!!}  ; pmono = {!!}
-                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 } where
+                     ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!}   ; supf = supf0 } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -571,7 +553,7 @@
                 scnext {x} (case2 sx) = case2 ( fsuc x sx )
                 scinit :  {x : Ordinal} → odef schain x → * y ≤ * x
                 scinit {x} (case1 zx) = ZChain.initial zc zx
-                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋x zc ) )
+                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init zc ) )
                 ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) )
                 ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp )
                 ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x )
@@ -600,9 +582,9 @@
                      z24 : IsSup A schain ab → IsSup A (ZChain.chain zc) ab 
                      z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
                      z23 : odef chain0 b
-                     z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc )
-                     ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc )
-                     ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋x zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b
+                     z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc )
+                     ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋init zc )
+                     ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋init zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b
                 seq : schain ≡ supf0 x 
                 seq with trio< x x
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
@@ -624,32 +606,30 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox with trio< x y
-     ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
-     ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
-     ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} ; pmono = {!!}
-                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!} }   where --- limit ordinal case
-         record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
-            field
-               u : Ordinal
-               u<x : u o< x
-               chain∋z : odef (ZChain.chain (prev u u<x  )) z
-         Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
-         Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
-         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u)
+     ... | no ¬ox = record { chain⊆A = ? ; f-next = ? ; chain = ?
+                     ; initial = ? ; chain∋init  = ? ; is-max = {!!} }   where --- limit ordinal case
+         supf : Ordinal → HOD
+         supf = ZChain1.supf zc0
+         Uz⊆A : {z : Ordinal} → UZFChain A f zc0 x y prev z ∨ FClosure A f y z → odef A z
+         Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u)
+         Uz⊆A (case2 lt) = A∋fc _ f mf lt 
+         uzc : {z : Ordinal} → (u : UZFChain A f zc0 x y prev z) → ZChain A y f zc0 (UZFChain.u u)
          uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) 
          Uz : HOD
-         Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
+         Uz = record { od = record { def = λ z → UZFChain A f zc0 x y prev z ∨ FClosure A f y z } ; odmax = & A
              ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
          u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
-         u-next {z} u = record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u)  }
+         u-next {z} (case1 u) = case1 record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u)  }
+         u-next {z} (case2 u) = case2 ( fsuc _ u )
          u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
-         u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
-         u-chain∋x :  odef Uz y
-         u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ) }
+         u-initial {z} (case1 u) = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
+         u-initial {z} (case2 u) = s≤fc _ f mf u
+         u-chain∋init :  odef Uz y
+         u-chain∋init = case2 ( init ay )
+
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain.supf (prev z a ) z
+         ... | tri< a ¬b ¬c = ZChain1.supf zc0 z
          ... | tri≈ ¬a b ¬c = Uz 
          ... | tri> ¬a ¬b c = Uz
          seq : Uz ≡ supf0 x
@@ -657,52 +637,21 @@
          ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
          ... | tri≈ ¬a b ¬c = refl
          ... | tri> ¬a ¬b c = refl
-         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain.supf (prev b b<x ) b  ≡ supf0 b
+         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain1.supf zc0 b  ≡ supf0 b
          seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (prev b k ) b) o<-irr --  b<x ≡ a
+         ... | tri< a ¬b ¬c = cong (λ k → ZChain1.supf zc0 b) o<-irr --  b<x ≡ a
          ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
          ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
          ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y
          ord≤< {x} {y} {z} x<z z≤y  with  osuc-≡< z≤y
          ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z
          ... | case2 z<y  = ordtrans x<z z<y
-         u-mono : {z : Ordinal} → z o≤ x → supf0 z ⊆' supf0 x
-         u-mono {z} z≤x {i} with trio< z x | trio< x x
-         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = λ lt → {!!}
-         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = {!!} ; u<x = {!!} ;  chain∋z = lt }
-         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = λ lt → {!!}
-         ... | tri≈ ¬a b ¬c | s = {!!} -- λ lt → lt 
-         ... | tri> ¬a ¬b c | s = {!!} -- λ lt → lt 
          
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A)
-     SZ f mf {y} ay = TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) (& A)
-
-     postulate
-       TFcomm :  { ψ : Ordinal  → Set (Level.suc n) }
-          → (ind :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
-          →  ∀ (x : Ordinal)  →   ind  x (λ y _ → TransFinite ind  y )  ≡ TransFinite ind  x
+     SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain0 A 
+     SZ0 f mf ay = TransFinite {λ z → ZChain1 z} (sind f mf ay ) (& A)
 
-     record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) : Set (Level.suc n) where
-      field
-         zc : ZChain A y f (& A)
-      supf = ZChain.supf zc 
-      field
-         chain-mono : {x y : Ordinal} → x o≤ y → supf x ⊆' supf y 
-         f-total : {x : Ordinal} → IsTotalOrderSet (supf x) 
-
-     SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
-         → ZChain1 f mf ay 
-     SZ1 f mf {y} ay = record { zc = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) (& A)
-             ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where
-         sf : Ordinal → HOD
-         sf x = ZChain.supf (TransFinite (ind f mf ay) (& A)) x
-         sf' : Ordinal → HOD
-         sf' x = ZChain.supf (ind f mf ay (& A) {!!} )  x
-         mono :  {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → sf x ⊆' sf w 
-         mono {a} {b} sf a≤b = TransFinite0 {λ b → a o≤ b → sf a ⊆' sf b } mind b a≤b where
-            mind :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o≤ y₁ → sf a ⊆' sf y₁) → a o≤ x → sf a ⊆' sf x
-            mind x prev a≤x sai = {!!}
-
+     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (SZ0 f mf ya)  (& A)
+     SZ f mf {y} ay = TransFinite {λ z → ZChain A y f (SZ0 f mf ay)  z  } (ind f mf ay (SZ0 f mf ay)  ) (& A)
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -714,16 +663,18 @@
          zorn01  = proj1  zorn03  
          zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
          zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
-     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 total ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zc0 zorn04 total ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
-         zorn04 : ZChain A (& s) (cf nmx) (& A)
-         zorn04 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) )
+         zc0 : ZChain0 A 
+         zc0 = TransFinite {λ z → ZChain1 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  (subst (λ k → odef A k ) &iso as )) (& A)
+         zorn04 : ZChain A (& s) (cf nmx) zc0 (& A)
+         zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
          total : IsTotalOrderSet (ZChain.chain zorn04)
-         total =  ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) 
+         total =  ZChain.f-total (SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) 
 
 -- usage (see filter.agda )
 --