# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656726708 -32400
# Node ID 5e056537807d6dba0d23a4e734197b857a3c8269
# Parent  db9477c80dce10a82d639fe96f2a51fb058716ba
...

diff -r db9477c80dce -r 5e056537807d src/OrdUtil.agda
--- a/src/OrdUtil.agda	Sat Jul 02 07:52:05 2022 +0900
+++ b/src/OrdUtil.agda	Sat Jul 02 10:51:48 2022 +0900
@@ -82,6 +82,11 @@
 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a (ordtrans lt <-osuc ) )
 ... | tri> ¬a ¬b c  = ⊥-elim (¬a (ordtrans lt <-osuc ) )
 
+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
+
 -- 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 db9477c80dce -r 5e056537807d src/zorn.agda
--- a/src/zorn.agda	Sat Jul 02 07:52:05 2022 +0900
+++ b/src/zorn.agda	Sat Jul 02 10:51:48 2022 +0900
@@ -262,34 +262,13 @@
          → ( chainf : Ordinal → HOD ) → ( lt : ( z : Ordinal ) → z o< x → Chain A f ay z ( chainf z ))
          → Chain A f ay x 
              record { od = record { def = λ z → odef A z ∧ (UChain chainf x z ∨ FClosure A f y z ) } 
-                ; odmax = & A ; <odmax = λ {y} sy → {!!}   }
+                ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
-Chain-uniq : (A : HOD ) ( f : Ordinal → Ordinal ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-     → ( Ordinal → HOD ) → Set (Level.suc n)
-Chain-uniq A f {y} ay x chain  with Oprev-p x
-... | yes op = st1 where
-      px = Oprev.oprev op
-      st1 : Set (Level.suc n)
-      st1 with ODC.∋-p O A (* x)
-      ... | no noax = chain x ≡ chain px
-      ... | yes ax with ODC.p∨¬p O ( HasPrev A (chain px) ax f )   
-      ... | case1 pr = chain x ≡ chain px
-      ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (chain px) ax )
-      ... | case1 is-sup = chain x ≡ schain where
-            schain : HOD
-            schain = record { od = record { def = λ x → odef (chain px) x ∨ (FClosure A f y x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-      ... | case2 ¬x=sup = chain x ≡ chain px
-... | no ¬ox = chain x ≡ record { od = record { def = λ z → odef A z ∧ ( UChain chain x z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = λ {y} sy → {!!}   }
-
-record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init) ( z : Ordinal ) : Set (Level.suc n) where
    field
-      chain : Ordinal → HOD
-      chain-mono : {x : Ordinal} → x o≤ z → chain x ⊆' chain z 
-      chain-uniq : Chain-uniq A f ay z chain
-
-record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init)  (zc0 : ZChain1 A f ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
-   chain : HOD
-   chain = ZChain1.chain zc0 z 
+      chainf : Ordinal → HOD
+      chain-uniq : {x : Ordinal} → x o≤ z → Chain A f ay x (chainf x) 
+   chain = chainf z
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -363,21 +342,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 : ZChain1 A f as0 (& A) ) (zc : ZChain A f as0 zc0 (& A) ) 
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f 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 : ZChain1 A f as0 (& A)) (zc : ZChain A f as0 zc0 (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f 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
@@ -400,7 +379,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 : ⊥
@@ -421,76 +400,31 @@
      -- 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 ) → (zc0 : ZChain1 A (cf nmx) as0 (& A)) (zc : ZChain A (cf nmx) as0 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 ))))
+     z04 :  (nmx : ¬ Maximal A ) →  (zc : ZChain A (cf nmx) as0 (& 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 ))))
                                                (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 ay z ) → ZChain1 A f ay x
-     sind f mf {y} ay x prev  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 ay px
-          sc = prev px px<x
-          no-ext : ZChain1 A f ay x
-          no-ext = record { chain = s01 ; chain-mono = ? ; chain-uniq = s02 } where
-                s01 : Ordinal → HOD
-                s01 z with trio< z x
-                ... | tri< a ¬b ¬c = chain (prev z a ) z
-                ... | tri≈ ¬a b ¬c = chain (prev px px<x ) px
-                ... | tri> ¬a ¬b c = chain (prev px px<x ) px
-                s02 : Chain-uniq A f ay x s01
-                s02 with trio< x x
-                ... | tri< a ¬b ¬c = ?
-                ... | tri≈ ¬a refl ¬c = ?
-                ... | tri> ¬a ¬b c = ?
-          sc4 : ZChain1 A f ay x
-          sc4 with ODC.∋-p O A (* x)
-          ... | no noax = {!!}
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc x) ax f )   
-          ... | case1 pr = {!!}
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc x) ax )
-          ... | case1 is-sup = {!!} where
-                -- A∋sc -- x is a sup of zc 
-                sup0 : SUP A (ZChain1.chain sc x )
-                sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → (ZChain1.chain 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 (ZChain1.chain sc x) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-          ... | case2 ¬x=sup = {!!}
-     ... | no ¬ox = ? where
-          sc5 : HOD
-          sc5 = record { od = record { def = λ z → odef A z ∧ (UChain ? x z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : ZChain1 A f ay (& A)) 
-         → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x
-     ind f mf {y} ay x zc0 prev with Oprev-p x
+     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
+         → ((z : Ordinal) → z o< x → ZChain A f ay z) → ZChain A f ay x
+     ind f mf {y} ay x prev with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
+          zc : ZChain A f ay (Oprev.oprev op)
+          zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           supf : Ordinal → HOD
-          supf = ZChain1.chain zc0
-          zc : ZChain A f ay zc0 (Oprev.oprev op)
-          zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
+          supf = ZChain.chainf zc
           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
@@ -500,12 +434,15 @@
           --
           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 f ay ?  x
-          no-extenion is-max = record { chain⊆A = ? -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
+                            * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay  x
+          no-extenion is-max = record { 
+                       chainf = {!!}
+                     ; chain-uniq = {!!}
+                     ; chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
+                     ; chain∋init  = subst (λ k → odef k y ) {!!} (ZChain.chain∋init  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) 
-                     ; f-total = ? 
-                     ; chain∋init  = subst (λ k → odef k y ) {!!} (ZChain.chain∋init  zc) 
+                     ; f-total = {!!} 
                      ; 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  ) {!!} is-max } where
                 supf0 : Ordinal → HOD
@@ -524,7 +461,7 @@
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
-          zc4 : ZChain A f ay zc0 x 
+          zc4 : ZChain A f ay 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) →
@@ -533,7 +470,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 zc0 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 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) →
@@ -653,53 +590,35 @@
                 ... | 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 { chain⊆A = {!!} ; f-next = {!!} ; f-total = ?
+     ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!}
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          supf : Ordinal → HOD
-         supf = ZChain1.chain zc0
-         uzc : {z : Ordinal} → (u : UChain supf x z) → ZChain A f ay zc0 (UChain.u u)
+         supf = {!!}
+         uzc : {z : Ordinal} → (u : UChain supf x z) → ZChain A f ay (UChain.u u)
          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
          Uz : HOD
-         Uz = record { od = record { def = λ z → odef A z ∧ ( UChain supf z x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = ?  }
+         Uz = record { od = record { def = λ z → odef A z ∧ ( UChain supf z x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
          u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
-         u-next {z} = ?
+         u-next {z} = {!!}
          -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u)  }
          -- u-next {z} (case2 u) = case2 ( fsuc _ u )
          u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
-         u-initial {z} = ?
+         u-initial {z} = {!!}
          -- (case1 u) = ZChain.initial ( uzc u )  (UChain.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 )
+         u-chain∋init = {!!} -- case2 ( init ay )
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain1.chain zc0 z
+         ... | tri< a ¬b ¬c = {!!}
          ... | tri≈ ¬a b ¬c = Uz 
          ... | tri> ¬a ¬b c = Uz
          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
-         ... | s | t = ?
-
-         seq : Uz ≡ supf0 x
-         seq with trio< x x
-         ... | 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.chain zc0 b  ≡ supf0 b
-         seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = cong (λ k → ZChain1.chain 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
+         ... | s | t = {!!}
          
-     SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain1 A f ay (& A)
-     SZ0 f mf ay = TransFinite {λ z → ZChain1 A f ay z} (sind f mf ay ) (& A)
-
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f ay (SZ0 f mf ay)  (& A)
-     SZ f mf {y} ay = TransFinite {λ z → ZChain A f 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 ay (& A)
+     SZ f mf {y} ay = TransFinite {λ z → ZChain A f ay   z  } (λ x → ind f mf ay x ) (& A)
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -711,15 +630,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 : ZChain1 A  (cf nmx) as0 (& A)
-         zc0 = TransFinite {λ z → ZChain1 A (cf nmx) as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  as0) (& A)
-         zorn04 : ZChain A (cf nmx) as0 zc0 (& A)
+         zorn04 : ZChain A (cf 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