# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657633840 -32400
# Node ID 0278f0d151f28798a6692ce368803c687e1edbb3
# Parent  3837fa940cd9d138599af66a15f5292f6b3e1133
one pass

diff -r 3837fa940cd9 -r 0278f0d151f2 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 12 15:29:41 2022 +0900
+++ b/src/zorn.agda	Tue Jul 12 22:50:40 2022 +0900
@@ -278,16 +278,12 @@
 UnionCF A f mf ay supf x
    = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
-record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+        {init : Ordinal} (ay : odef A init)  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal 
-      -- is-chain : {w : Ordinal } → Chain A f mf ay supf z w 
-      -- supf-mono : (x y : Ordinal ) → x o≤ y  → supf x o≤ supf y
-
-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 = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)
+   chain = UnionCF A f mf ay supf z
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -403,21 +399,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 ) (zc0 : (x : Ordinal) → ZChain1 A f mf as0 x ) (zc : ZChain A f mf as0 zc0 (& A) ) 
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& 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 
+     sp0 f mf 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 ) (zc0 : (x : Ordinal) → ZChain1 A f mf as0 x) (zc : ZChain A f mf as0 zc0 (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
             → (total : IsTotalOrderSet (ZChain.chain zc) )
-            → 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
+            → f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc  total))
+     fixpoint f mf zc total = z14 where
            chain = ZChain.chain zc
-           sp1 = sp0 f mf zc0 zc total
+           sp1 = sp0 f mf 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
@@ -440,7 +436,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 zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total ))
+           z14 :  f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf 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 : ⊥
@@ -462,108 +458,53 @@
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
      z04 :  (nmx : ¬ Maximal A ) 
-           → (zc0 : (x : Ordinal) → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 x) 
-           → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 zc0 (& A)) 
+           → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& 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 ))))
+     z04 nmx 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 ) zc0 zc total ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) 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) zc0 zc total
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
           c = & (SUP.sup sp1)
 
      --
      -- create all ZChains under o< x
      --
 
-     sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → ZChain1 A f mf ay z ) → ZChain1 A f mf ay x
-     sind f mf {y} ay x prev  with trio< o∅ x
-     ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c )
-     ... | tri≈ ¬a b ¬c = record { supf = λ _ → y }
-     ... | tri< 0<x ¬b ¬c with Oprev-p x
-     ... | yes op = sc4 where
-          open ZChain1
-          px = Oprev.oprev op
-          px<x : px o< x
-          px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
-          sc : ZChain1 A f mf ay px
-          sc = prev px px<x
-          pchain : HOD
-          pchain  = UnionCF A f mf ay (ZChain1.supf sc) x
-
-          no-ext :  ZChain1 A f mf ay x
-          no-ext = record { supf = ZChain1.supf sc }  
-          sc4 : ZChain1 A f mf ay x
-          sc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-ext
-          ... | 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 { supf = psup1 } where
-            psup1 : Ordinal → Ordinal
-            psup1 z with trio< z x 
-            ... | tri< a ¬b ¬c = ZChain1.supf sc z
-            ... | tri≈ ¬a b ¬c = x
-            ... | tri> ¬a ¬b c = x
-          ... | case2 ¬x=sup = no-ext
-     ... | no ¬ox = sc4 where
-          pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
-          pzc z z<x = prev z z<x
-          psupf : (z : Ordinal) → Ordinal
-          psupf z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain1.supf (pzc z a) z
-          ... | tri≈ ¬a b ¬c = o∅
-          ... | tri> ¬a ¬b c = o∅
-          UZ : HOD
-          UZ = UnionCF A f mf ay psupf x
-          total-UZ : IsTotalOrderSet UZ
-          total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay psupf (UChain.chain∋z (proj2 ca)) (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 { supf = psup1 }  where
-            psup1 : Ordinal → Ordinal
-            psup1 z with trio< z x 
-            ... | tri< a ¬b ¬c = ZChain1.supf (pzc z a) z
-            ... | tri≈ ¬a b ¬c = spu
-            ... | tri> ¬a ¬b c = spu
-
      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) 
-         → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x
-     ind f mf {y} ay x zc0 prev with trio< o∅ x
-     ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c )
-     ... | tri≈ ¬a refl ¬c = record { initial = initial1 } where
-          initial1 :  {z : Ordinal} → odef (UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)) z → * y ≤ * z 
-          initial1 {z} uz = ? where
-             zc01 : odef A z ∧ UChain A f mf ay (ZChain1.supf (zc0 (& A))) (& A) z
-             zc01 = uz
+         → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
+     ind f mf {y} ay x prev with trio< y x
+     ... | tri> ¬a ¬b c = ?
+     ... | tri≈ ¬a refl ¬c = ?
      ... | tri< 0<x ¬b ¬c with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
-          zc : ZChain A f mf ay zc0 (Oprev.oprev op)
+          zc : ZChain A f mf ay (Oprev.oprev op)
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
           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 
 
+          pchain : HOD
+          pchain  = UnionCF A f mf ay (ZChain.supf zc) x
+          ptotal : IsTotalOrderSet pchain
+          ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+               uz01 = chain-total A f mf ay (ZChain.supf zc) (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → 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 f mf ay zc0 x
-          no-extenion is-max  = record { initial = ZChain.initial zc ; chain∋init = ZChain.chain∋init zc }
+                            * a < * b → odef (ZChain.chain zc ) b ) → ZChain A f mf ay x
+          no-extenion is-max  = record { initial = ? ; chain∋init = ? }
 
-          zc4 : ZChain A f mf ay zc0 x 
+          zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
                 zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
@@ -573,7 +514,7 @@
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
                 ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) 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 zc0 x
+               -- we have to check adding x preserve is-max ZChain A y f mf 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 z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
@@ -586,32 +527,29 @@
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
                      ; initial = pinit ; chain∋init  = pcy ; is-max = p-ismax } where
-                pchain : HOD
-                pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)
-                psupf = ZChain1.supf (zc0 (& A))
+                psupf : Ordinal → Ordinal
+                psupf z with trio< z x 
+                ... | tri< a ¬b ¬c = ZChain.supf zc z
+                ... | tri≈ ¬a b ¬c = x
+                ... | tri> ¬a ¬b c = x
                 pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
                 pchain⊆A {y} ny = proj1 ny
                 pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
-                pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = fua } ⟫ where
+                pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
                     afa : odef A ( f a )
                     afa = proj2 ( mf a aa )
                     fua : Chain A f mf ay psupf (UChain.u ua) (f a)
                     fua with UChain.chain∋z ua
                     ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-                    ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc)
-                ptotal : {a b : HOD } → odef pchain (& a) → odef pchain (& b)
-                   →   Tri ( a <  b) ( a ≡  b) ( b <  a )
-                ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-                    uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-                    uz01 = chain-total A f mf ay _ (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+                    ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
                 pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
                 pinit {a} ⟪ aa , ua ⟫  with UChain.chain∋z ua
                 ... | ch-init a fc = s≤fc y f mf fc
-                ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
+                ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc)  where
                      zc7 : y << psupf (UChain.u ua)
-                     zc7 = ChainP.fcy<sup is-sup (init ay)
+                     zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
                 pcy : odef pchain y
-                pcy = ⟪ ay , record { u =  y ; u<x = ∈∧P→o< ⟪  ay , lift true  ⟫ ; chain∋z = ch-init _ (init ay)  }  ⟫
+                pcy = ? -- ⟪ ay , record { u =  y ; u<x = ∈∧P→o< ⟪  ay , lift true  ⟫ ; chain∋z = ch-init _ (init ay)  }  ⟫
                 p-ismax :  {a b : Ordinal} → odef pchain  a →
                     b o< osuc x → (ab : odef A b) →
                     ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
@@ -630,26 +568,40 @@
                 ... | 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 op = zc5 where
-          uzc : {z : Ordinal} → (u : UChain A f mf ay (ZChain1.supf (zc0 (& A))) x z ) → ZChain A f mf ay zc0 (UChain.u u)
-          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
+          pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
+          pzc z z<x = prev z z<x
+          psupf0 : (z : Ordinal) → Ordinal
+          psupf0 z with trio< z x
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
+          ... | tri≈ ¬a b ¬c = o∅
+          ... | tri> ¬a ¬b c = o∅
           UZ : HOD
-          UZ = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) x
-          zc5 : ZChain A f mf ay zc0 x 
+          UZ = UnionCF A f mf ay psupf0 x
+          total-UZ : IsTotalOrderSet UZ
+          total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+               uz01 = chain-total A f mf ay psupf0 (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+          usup : SUP A UZ
+          usup = supP UZ (λ lt → proj1 lt) total-UZ 
+          spu = & (SUP.sup usup)
+          psupf : Ordinal → Ordinal
+          psupf z with trio< z x 
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
+          ... | tri≈ ¬a b ¬c = spu
+          ... | tri> ¬a ¬b c = spu
+          zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = {!!} where -- ¬ A ∋ p, just skip
           ... | yes ax with ODC.p∨¬p O ( HasPrev A UZ ax f )   
-               -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
+               -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A UZ ax )
           ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
 
          
-     SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x
-     SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x
-
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (SZ0 f mf ay )  (& A)
-     SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay (SZ0 f mf ay )  z  } (λ x → ind f mf ay x (SZ0 f mf ay )  ) (& A)
+     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)
+     SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay   z  } (λ x → ind f mf ay x   ) (& A)
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -661,15 +613,13 @@
          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 zc0  zorn04 total ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx 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) ) ⟫
-         zc0 : (x : Ordinal) → ZChain1 A  (cf nmx) (cf-is-≤-monotonic nmx) as0 x
-         zc0 x = TransFinite {λ z → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  as0) x
-         zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 zc0 (& A)
+         zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
          total : IsTotalOrderSet (ZChain.chain zorn04)
          total {a} {b} = zorn06  where