# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655700426 -32400
# Node ID 35d8aca1a2b788473e5c7d324e74142eec05fbe3
# Parent  886e1f82cca0e4f21949c2a0100a58f84cf7250e
failed again
monotonicity only happens on Minimum ZChain

diff -r 886e1f82cca0 -r 35d8aca1a2b7 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 20 08:43:23 2022 +0900
+++ b/src/zorn.agda	Mon Jun 20 13:47:06 2022 +0900
@@ -233,7 +233,11 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (supf : Ordinal → HOD) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
+   field
+      supf : Ordinal → HOD
+      chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
+      f-total : {x y : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
    chain : HOD
    chain = supf z 
    field
@@ -246,12 +250,9 @@
           → 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 → HOD
-      zc : ZChain A x f supf z
-      chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
-      f-total : {x y : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
+ZChainSupUnique : ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) ( a b : Ordinal )
+   → ( za : ZChain A x f a ) → (zb : ZChain A x f b ) → a o< b → i o≤ a → ZChain.supf za i ≡ ZChain.supf zb i
+ZChainSupUnique = ?
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -324,27 +325,24 @@
      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  ) ⟫
 
-     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc1 : ZChain1 A (& s) f (& A) ) → SUP A  (ZChain.chain (ZChain1.zc zc1)) 
-     zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain1.f-total zc1 {& A} {& A} o≤-refl )   where
-           zc = ZChain1.zc zc1
-     A∋zsup : (nmx : ¬ Maximal A ) (zc1 : ZChain1 A (& s) (cf nmx)  (& A) ) 
-        →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 )))
-     A∋zsup nmx zc1 = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 ) )
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc1 : ZChain1 A (& s) f  (& A) ) → SUP A (ZChain.chain (ZChain1.zc zc1))
-     sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain1.f-total zc1 {& A} {& A} o≤-refl )   where
-           zc = ZChain1.zc zc1
+     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A (& s) f (& A) ) → SUP A  (ZChain.chain zc) 
+     zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc {& A} {& A} o≤-refl )   
+     A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx)  (& A) ) 
+        →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc )))
+     A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) ) → SUP A (ZChain.chain zc)
+     sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc {& A} {& A} o≤-refl )   
      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 ) (zc1 : ZChain1 A (& s) f  (& A) )
-            → f (& (SUP.sup (sp0 f mf zc1 ))) ≡ & (SUP.sup (sp0 f mf zc1 ))
-     fixpoint f mf zc1 = z14 where
-           zc = ZChain1.zc zc1
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) )
+            → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
+     fixpoint f mf zc = z14 where
            chain = ZChain.chain zc
-           sp1 = sp0 f mf zc1
+           sp1 = sp0 f mf zc
            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
@@ -367,8 +365,8 @@
                    ... | 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 zc1))) ≡ & (SUP.sup (sp0 f mf zc1))
-           z14 with ZChain1.f-total zc1 {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
+           z14 with ZChain.f-total zc {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
                z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
@@ -388,13 +386,12 @@
      -- 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 : ZChain1 A (& s) (cf nmx) (& A)) → ⊥
-     z04 nmx zc1 = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1))))
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → ⊥
+     z04 nmx zc = <-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 ) zc1 ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where          -- x < f x
-          zc = ZChain1.zc zc1
-          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc1
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
 
      --
@@ -402,45 +399,41 @@
      --
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → { y₁ : Ordinal} (ay : odef A y₁)
-         → ZChain1 A y₁ f y) → {y : Ordinal} (ay : odef A y) → ZChain1 A y f x
+         → ZChain A y₁ f y) → {y : Ordinal} (ay : odef A y) → ZChain A y f x
      ind f mf x prev {y} ay with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
-          open ZChain
-          
           px = Oprev.oprev op
           supf : Ordinal → HOD
-          supf = ZChain1.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)
-          zc1 : ZChain1 A y f (Oprev.oprev op)
-          zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay 
-          zc0 : ZChain A y f (ZChain1.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)) (Oprev.oprev op)
-          zc0 = ZChain1.zc (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)
-          zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
-          zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+          supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay)
+          zc : ZChain A y f (Oprev.oprev op)
+          zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay 
+          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 
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
-                            * a < * b → odef (ZChain.chain zc0) b ) → ZChain1 A y f x
-          no-extenion is-max = record { supf = supf0 ; zc = record { chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc0)
-                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc0)
-                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc0) 
+          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) 
                      ; f-immediate =  subst (λ k →  {x₁ : Ordinal} {y₁ : Ordinal} → odef k x₁ → odef k y₁ →
-                            ¬ (* x₁ < * y₁) ∧ (* y₁ < * (f x₁)) ) seq (ZChain.f-immediate zc0) ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc0)
+                            ¬ (* x₁ < * y₁) ∧ (* y₁ < * (f x₁)) ) seq (ZChain.f-immediate zc) ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc)
                              ; 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 } 
+                                 HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max 
                      ; chain-mono = mono ; f-total = {!!} } where
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
                 ... | tri< a ¬b ¬c = supf z
-                ... | tri≈ ¬a b ¬c = ZChain.chain zc0
-                ... | tri> ¬a ¬b c = ZChain.chain zc0 
-                seq : ZChain.chain zc0 ≡ supf0 x 
+                ... | tri≈ ¬a b ¬c = ZChain.chain zc
+                ... | tri> ¬a ¬b c = ZChain.chain zc 
+                seq : ZChain.chain zc ≡ supf0 x 
                 seq with trio< x x
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
                 ... | tri≈ ¬a b ¬c = refl 
@@ -455,7 +448,7 @@
                 mono {a} {b} a≤b b<ox with osuc-≡< a≤b
                 ... | case1 refl = λ x → x
                 ... | case2 a<b with osuc-≡< b<ox 
-                ... | case1 b=x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x) nc00 ( ZChain1.chain-mono zc1 a≤px <-osuc  ) where
+                ... | case1 b=x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x) nc00 ( ZChain.chain-mono zc a≤px <-osuc  ) where
                      a<x : a o< x
                      a<x with  osuc-≡< b<ox
                      ... | case1 b=x = subst (λ k → a o< k ) b=x a<b
@@ -468,38 +461,38 @@
                      ... | tri≈ ¬a b ¬c = refl
                      ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b=x )
                 ... | case2 b<x = subst₂ (λ j k → j ⊆' k ) (seq<x a<x ) (seq<x b<x )
-                            ( ZChain1.chain-mono zc1 a≤b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x ) )
+                            ( ZChain.chain-mono zc a≤b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) b<x ) )
                    where
                      a<x : a o< x
                      a<x with  osuc-≡< b<ox
                      ... | case1 b=x = subst (λ k → a o< k ) b=x a<b
                      ... | case2 b<x = ordtrans a<b b<x
 
-          zc4 : ZChain1 A y f x 
+          zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extenion zc11  where -- ¬ A ∋ p, just skip
-                zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
-                            * a < * b → odef (ZChain.chain zc0) b
-                zc11 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
+          ... | 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) →
+                    HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
+                            * a < * b → odef (ZChain.chain zc) b
+                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 zc0 za (zc0-b<x b lt)  ab P a<b
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf supO x
-          ... | case1 pr = no-extenion zc17  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-                chain0 = ZChain.chain zc0
-                zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
-                            HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab →
-                            * a < * b → odef (ZChain.chain zc0) b
-                zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
-                ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
-          ... | case1 is-sup = -- x is a sup of zc0 
-                record { zc = record { chain⊆A = {!!} ; f-next = {!!} 
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} }  ; supf = supf0 ; chain-mono = mono ; f-total = {!!} } where 
-                sup0 : SUP A (ZChain.chain zc0) 
+                ... | 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
+          ... | 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) →
+                            HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab →
+                            * a < * b → odef (ZChain.chain zc) b
+                zc7 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
+                ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab P a<b
+                ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
+          ... | 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 = {!!} 
+                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 ; chain-mono = mono ; f-total = {!!} } where 
+                sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
+                        x21 :  {y : HOD} → ZChain.chain zc ∋ 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  )
@@ -507,17 +500,17 @@
                 sp = SUP.sup sup0 
                 x=sup : x ≡ & sp 
                 x=sup = sym &iso 
-                chain0 = ZChain.chain zc0
+                chain0 = ZChain.chain zc
                 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
-                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc0 (subst (λ k → odef chain0 k) (sym &iso) zx )))
+                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc (subst (λ k → odef chain0 k) (sym &iso) zx )))
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
-                A∋schain (case1 zx ) = ZChain.chain⊆A zc0 zx 
+                A∋schain (case1 zx ) = ZChain.chain⊆A zc zx 
                 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
                 s⊆A : schain ⊆' A
-                s⊆A {x} (case1 zx) = ZChain.chain⊆A zc0 zx
+                s⊆A {x} (case1 zx) = ZChain.chain⊆A zc zx
                 s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx 
                 cmp  : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
                 cmp {a} {b} za fb  with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb  
@@ -534,7 +527,7 @@
                         a<b : a < b
                         a<b = ptrans  (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
                 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
-                scmp {a} {b} (case1 za) (case1 zb) = ZChain1.f-total zc1 {px} {px} o≤-refl za zb
+                scmp {a} {b} (case1 za) (case1 zb) = ZChain.f-total zc {px} {px} o≤-refl za zb
                 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb 
                 scmp  (case2 fa) (case1 zb) with  cmp zb fa
                 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq))  a
@@ -542,24 +535,24 @@
                 ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq))  ¬a
                 scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb)
                 scnext : {a : Ordinal} → odef schain a → odef schain (f a)
-                scnext {x} (case1 zx) = case1 (ZChain.f-next zc0 zx)
+                scnext {x} (case1 zx) = case1 (ZChain.f-next zc zx)
                 scnext {x} (case2 sx) = case2 ( fsuc x sx )
                 scinit :  {x : Ordinal} → odef schain x → * y ≤ * x
-                scinit {x} (case1 zx) = ZChain.initial zc0 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 zc0 ) )
+                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 ) )
                 ... | 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 )
                 ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) )
                 A∋za : {a : Ordinal } → odef chain0 a → odef A a
-                A∋za za = ZChain.chain⊆A zc0 za 
+                A∋za za = ZChain.chain⊆A zc za 
                 za<sup :  {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨  ( * a < sp )
                 za<sup za =  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za )
                 simm : {a b : Ordinal}  → odef schain a → odef schain b → ¬ (* a < * b) ∧ (* b < * (f a))
-                simm {a} {b} (case1 za) (case1 zb) = ZChain.f-immediate zc0 za zb
+                simm {a} {b} (case1 za) (case1 zb) = ZChain.f-immediate zc za zb
                 simm {a} {b} (case1 za) (case2 sb) p with  proj1 (mf a (A∋za za) )
                 ... | case1 eq = <-irr (case2  (subst (λ k → * b < k ) (sym eq) (proj2 p))) (proj1 p) 
-                ... | case2 a<fa with za<sup  ( ZChain.f-next zc0 za ) | s≤fc (& sp) f mf sb
+                ... | case2 a<fa with za<sup  ( ZChain.f-next zc za ) | s≤fc (& sp) f mf sb
                 ... | case1 fa=sp | case1 sp=b = <-irr (case1 (trans fa=sp (trans (sym *iso) sp=b )) ) ( proj2 p )
                 ... | case2 fa<sp | case1 sp=b = <-irr (case2 fa<sp) (subst (λ k → k < * (f a) ) (trans (sym sp=b) *iso) (proj2 p ) )
                 ... | case1 fa=sp | case2 sp<b = <-irr (case2 (proj2 p )) (subst  (λ k → k < * b) (sym fa=sp) (subst (λ k → k < * b ) *iso sp<b ) )
@@ -580,21 +573,21 @@
                 s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where   -- has previous
                      z21 : HasPrev A schain ab f → odef schain b
                      z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 
-                           case1 (ZChain.is-max zc0 za (zc0-b<x b b<x) ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
+                           case1 (ZChain.is-max zc za (zc-b<x b b<x) ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
                      z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
-                s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc0 za (zc0-b<x b b<x) ab (case2 z22) a<b ) where -- previous sup
-                     z22 : IsSup A (ZChain.chain zc0)   ab 
+                s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc za (zc-b<x b b<x) ab (case2 z22) a<b ) where -- previous sup
+                     z22 : IsSup A (ZChain.chain zc)   ab 
                      z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
                 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p)  a<b | case2 b<x with HasPrev.ay p
-                ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy ))               -- in previous closure of f
+                ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc zy ))               -- in previous closure of f
                 ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy ))  -- in current  closure of f
-                s-ismax {a} {b} (case2 sa) b<ox ab (case2 p)  a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc0
-                     z24 : IsSup A schain ab → IsSup A (ZChain.chain zc0) ab 
+                s-ismax {a} {b} (case2 sa) b<ox ab (case2 p)  a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc
+                     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 zc0 )
-                     ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
-                     ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<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
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
                 ... | tri< a ¬b ¬c = supf z
@@ -614,29 +607,27 @@
                 mono {a} {b} a≤b b<ox = {!!}
 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
-                            HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0)   ab →
-                            * a < * b → odef (ZChain.chain zc0) b
+                z18 :  {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
                 z18 {a} {b} za b<x ab p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab p a<b 
+                ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab p a<b 
                 ... | case1 b=x with p
                 ... | 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 = record { supf = supf0 ; chain-mono = {!!} ; f-total = u-total
-              ; zc  = record { chain⊆A = {!!} ; f-next = {!!} 
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} } }  where --- limit ordinal case
+     ... | no ¬ox = record { supf = supf0 ; chain-mono = u-mono ; f-total = u-total
+              ; chain⊆A = {!!} ; f-next = {!!} 
+                     ; initial = {!!} ; f-immediate = {!!} ; 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 (ZChain1.zc (prev u u<x {y} ay ))) z
+               chain∋z : odef (ZChain.chain (prev u u<x {y} ay )) z
          Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
-         Uz⊆A {z} u = ZChain.chain⊆A (ZChain1.zc ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay )) (UZFChain.chain∋z u)
-         uzc1 : {z : Ordinal} → (u : UZFChain z) → ZChain1 A y f (UZFChain.u u)
-         uzc1 {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) {y} ay
-         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (ZChain1.supf (uzc1 u)) (UZFChain.u u)
-         uzc {z} u =  ZChain1.zc (prev (UZFChain.u u) (UZFChain.u<x u) {y} ay)
+         Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay ) (UZFChain.chain∋z u)
+         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u)
+         uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) {y} ay
          Uz : HOD
          Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
              ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
@@ -645,10 +636,10 @@
          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 = {!!} ; chain∋z = ZChain.chain∋x (ZChain1.zc (prev y {!!} ay )) }
+         u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (prev y {!!} ay ) }
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain1.supf (prev z a {y} ay) z
+         ... | tri< a ¬b ¬c = ZChain.supf (prev z a {y} ay) z
          ... | tri≈ ¬a b ¬c = Uz 
          ... | tri> ¬a ¬b c = Uz
          seq : Uz ≡ supf0 x
@@ -656,29 +647,41 @@
          ... | 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 ) →  ZChain1.supf (prev b b<x {y} ay) b  ≡ supf0 b
+         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain.supf (prev b b<x {y} ay) b  ≡ supf0 b
          seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = cong (λ k → ZChain1.supf (prev b k {y} ay) b) o<-irr --  b<x ≡ a
+         ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (prev b k {y} ay) b) o<-irr --  b<x ≡ a
          ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
          ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
-         u-mono :  {z : Ordinal} {y : Ordinal} → z o≤ y → y o≤ x → supf0 z ⊆' supf0 y
-         u-mono {z} {y} z≤y y≤x with trio< z x | trio< y x
-         ... | tri< a ¬b ¬c | t = {!!}
-         ... | tri≈ ¬a b ¬c | t = {!!}
-         ... | tri> ¬a ¬b c | t = ⊥-elim ( osuc-< y≤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} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
+         u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
+         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = um00 where -- ZChain.chain-mono (prev w ? ay) ? ? lt
+             um00 : odef  (ZChain.supf (prev z a ay) z) i → odef  (ZChain.supf (prev w a₁ ay) w) i 
+             um00 = {!!}
+             um01 : odef  (ZChain.supf (prev z a ay) z) i → odef  (ZChain.supf (prev z {!!} ay) w) i 
+             um01 = ZChain.chain-mono (prev z a ay) {!!} {!!}
+         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = z ; u<x = a ; chain∋z = lt }
+         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim ( osuc-< w≤x c )
+         ... | tri≈ ¬a z=x ¬c | tri< w<x ¬b ¬c₁ = ⊥-elim ( osuc-< z≤w (subst (λ k → w o< k ) (sym z=x) w<x ) )
+         ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = λ lt → lt 
+         ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( osuc-< w≤x c ) -- o<> c ( ord≤< w≤x )) -- z≡w x o< w
+         ... | tri> ¬a ¬b c | t = ⊥-elim ( osuc-< w≤x (ord≤< c  z≤w ) ) -- x o< z → x o< w 
          u-total : {z : Ordinal}  → z o≤ x → IsTotalOrderSet (supf0 z)
          u-total {z}  z<x ux uy  with trio< z x
          ... | t = {!!}
          -- with trio< (UZFChain.u ux) (UZFChain.u uy)
-         -- ... | tri< a ¬b ¬c = ZChain1.f-total (uzc1 uy) {!!} (u-mono (UZFChain.u ux) (UZFChain.u uy)
-         --    (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc1 ux) (uzc1 uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
-         -- ... | tri≈ ¬a b ¬c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-         --    (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy))
-         -- ... | tri> ¬a ¬b c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-         --    (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy)) 
+         -- ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) {!!} (u-mono (UZFChain.u ux) (UZFChain.u uy)
+         --    (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+         -- ... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+         --    (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy))
+         -- ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+         --    (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
          
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain1 A y f (& A)
-     SZ f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain1 A y f z  } (ind f mf) (& A)
+     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A)
+     SZ f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain A y f z  } (ind f mf) (& A)
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -696,7 +699,7 @@
          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 : ZChain1 A (& s) (cf nmx) (& A)
+         zorn04 : ZChain A (& s) (cf nmx) (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 
 -- usage (see filter.agda )