# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670029033 -32400
# Node ID 4b22a2ece4e806f51d0a778aed41c2cb58401685
# Parent  dfbac4b59bae12631a5f490527d075380c513812
...

diff -r dfbac4b59bae -r 4b22a2ece4e8 src/zorn.agda
--- a/src/zorn.agda	Sat Dec 03 08:58:46 2022 +0900
+++ b/src/zorn.agda	Sat Dec 03 09:57:13 2022 +0900
@@ -247,7 +247,6 @@
    x≤sup = IsSUP.x≤sup isSUP
 
 --
-
 --
 --         f (f ( ... (supf y))) f (f ( ... (supf z1)))
 --        /          |         /             |
@@ -256,7 +255,8 @@
 --           o<                      o<
 --
 --    if sup z1 ≡ sup z2, the chain is stopped at sup z1, then f (sup z1) ≡ sup z1
-
+--    this means sup z1 is the Maximal, so f is <-monotonic if we have no Maximal.
+--
 
 fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal } 
     → (aa : odef A a ) →(  {y : Ordinal} → FClosure A f a y → (y ≡ b ) ∨ (y << b )) → a ≡ b → f a ≡ a
@@ -266,7 +266,6 @@
      fc00 :   b ≤  (f b)
      fc00 = proj1 (mf _ (subst (λ k → odef A k) a=b aa ))
 
-
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
@@ -354,7 +353,7 @@
    chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl)  ⟫
 
    mf : ≤-monotonic-f A f 
-   mf x ax = ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf x ax ) ⟫
+   mf x ax = ? 
 
    f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a)
    f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-init (fsuc _ fc) ⟫ 
@@ -677,7 +676,7 @@
                   m05 : ZChain.supf zc b ≡ b
                   m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }  , m04 ⟫
                   m10 : odef (UnionCF A f ay supf x) b
-                  m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
+                  m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
@@ -695,7 +694,7 @@
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
-                          m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
+                          m13 = ZChain.cfcs zc b<x x≤A m14 fc
 
         ... | no lim = record { is-max = is-max }  where
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a →
@@ -717,7 +716,7 @@
                   m05 : ZChain.supf zc b ≡ b
                   m05 = ZChain.sup=u zc ab (o<→≤  m09) ⟪ record { x≤sup = λ lt → IsSUP.x≤sup (proj2 is-sup) lt } , m04 ⟫    -- ZChain on x
                   m10 : odef (UnionCF A f ay supf x) b
-                  m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
+                  m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
                   m17 : MinSUP A (UnionCF A f ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
@@ -735,7 +734,7 @@
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
-                          m13 = ZChain.cfcs zc mf< b<x x≤A m14 fc
+                          m13 = ZChain.cfcs zc b<x x≤A m14 fc
 
      uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
      uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax =
@@ -799,7 +798,9 @@
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ )
 
           mf : ≤-monotonic-f A f 
-          mf x ax = ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf x ax ) ⟫
+          mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
+             mf00 : * x < * (f x)
+             mf00 = proj1 ( mf< x ax )
 
           --
           -- find the next value of supf
@@ -929,9 +930,9 @@
 
                  -- this is a kind of maximality, so we cannot prove this without <-monotonicity
                  --
-                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
+                 cfcs : {a b w : Ordinal } 
                      → a o< b → b o≤ x → supf1 a o< b  → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
-                 cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
+                 cfcs {a} {b} {w} a<b b≤x sa<b fc with zc43 (supf0 a) px
                  ... | case2 px≤sa = z50 where
                       a<x : a o< x
                       a<x = ordtrans<-≤ a<b b≤x
@@ -947,7 +948,7 @@
                           spx=sa : supf0 px ≡ supf0 a
                           spx=sa = begin
                                 supf0 px ≡⟨ cong supf0 px=sa  ⟩ 
-                                supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px  ⟩
+                                supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc a≤px sa≤px  ⟩
                                 supf0 a ∎  where open ≡-Reasoning
                           z51 : supf0 px o< b
                           z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩ 
@@ -955,7 +956,7 @@
                                 supf1 a ∎ )) sa<b where open ≡-Reasoning
                           z52 : supf1 a ≡ supf1 (supf0 px)
                           z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 
-                                supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 
+                                supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px sa≤px ) ⟩ 
                                 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
                                 supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ 
                                 supf1 (supf0 px) ∎ where open ≡-Reasoning
@@ -974,14 +975,14 @@
                  ... | tri< a<px ¬b ¬c = z50 where
                       z50 : odef (UnionCF A f ay supf1 b) w
                       z50 with osuc-≡< b≤x
-                      ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc  
+                      ... | case2 lt with ZChain.cfcs zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc  
                       ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                       ... | ⟪ az , ch-is-sup u u<b su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc u≤px )  ⟫ where
                            u≤px : u o≤ px
                            u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op))  (ordtrans<-≤ u<b b≤x )
                            u<x : u o< x
                            u<x = ordtrans<-≤ u<b b≤x 
-                      z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc  
+                      z50 | case1 eq with ZChain.cfcs zc a<px o≤-refl sa<px fc  
                       ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                       ... | ⟪ az , ch-is-sup u u<px su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc (o<→≤ u<px)) ⟫  where -- u o< px → u o< b ?
                            u<b : u o< b
@@ -1008,7 +1009,7 @@
                           spx≤px : supf0 px o≤ px
                           spx≤px = zc-b<x _ sfpx<x
                           z52 : supf1 (supf0 px) ≡ supf0 px
-                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl (zc-b<x _ sfpx<x ) )
+                          z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc o≤-refl (zc-b<x _ sfpx<x ) )
                           fc1 : FClosure A f (supf1 spx) w
                           fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc
                       ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where 
@@ -1114,11 +1115,10 @@
                  --  supf0 px not is included by the chain
                  --     supf1 x ≡ supf0 px because of supfmax
 
-                 cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                     → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f ay supf0 b) w
-                 cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with trio< b px 
-                 ... | tri< a ¬b ¬c = ZChain.cfcs zc mf< a<b (o<→≤ a) sa<b fc
-                 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc mf< a<b o≤-refl sa<b fc 
+                 cfcs : {a b w : Ordinal } → a o< b → b o≤ x →  supf0 a o< b → FClosure A f (supf0 a) w → odef (UnionCF A f ay supf0 b) w
+                 cfcs {a} {b} {w} a<b b≤x sa<b fc with trio< b px 
+                 ... | tri< a ¬b ¬c = ZChain.cfcs zc a<b (o<→≤ a) sa<b fc
+                 ... | tri≈ ¬a refl ¬c = ZChain.cfcs zc a<b o≤-refl sa<b fc 
                  ... | tri> ¬a ¬b px<b = cfcs1 where
                      x=b : x ≡ b
                      x=b with trio< x b
@@ -1136,7 +1136,7 @@
                          spx<b : supf0 px o< b
                          spx<b = subst (λ k → supf0 k o< b) a=px sa<b
                          cs01 : supf0 a ≡ supf0 (supf0 px)
-                         cs01 = trans (cong supf0 a=px) ( sym ( ZChain.supf-idem zc mf< o≤-refl 
+                         cs01 = trans (cong supf0 a=px) ( sym ( ZChain.supf-idem zc o≤-refl 
                               (subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ spx<b b≤x))))
                          fc1 : FClosure A f (supf0 (supf0 px)) w
                          fc1 = subst (λ k → FClosure A f k w) cs01 fc
@@ -1156,12 +1156,12 @@
                          cfcs2 : odef (UnionCF A f ay supf0 b) w
                          cfcs2 with trio< (supf0 a) px
                          ... | tri< sa<x ¬b ¬c = chain-mono f mf ay (ZChain.supf zc) (ZChain.supf-mono zc) (o<→≤ px<b) 
-                             ( ZChain.cfcs zc mf< a<px o≤-refl sa<x fc ) 
+                             ( ZChain.cfcs zc a<px o≤-refl sa<x fc ) 
                          ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , (zc-b<x _ sa<x)  ⟫ )
                          ... | tri≈ ¬a sa=px ¬c with trio< a px
                          ... | tri< a<px ¬b ¬c = ⟪  A∋fc {A} _ f mf fc , ? ⟫ where
                               cs01 : supf0 a ≡ supf0 (supf0 a)
-                              cs01 =  sym ( ZChain.supf-idem zc mf< (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
+                              cs01 =  sym ( ZChain.supf-idem zc (zc-b<x _ (ordtrans<-≤ a<b b≤x)) (zc-b<x _ (ordtrans<-≤ sa<b b≤x)))  
                               fc1 : FClosure A f (supf0 (supf0 a)) w
                               fc1 = subst (λ k → FClosure A f k w) cs01 fc
                               m : MinSUP A (UnionCF A f ay supf0 (supf0 a))
@@ -1240,10 +1240,15 @@
      ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
               ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
+          -- mf : ≤-monotonic-f A f 
+          -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫  will result memory exhaust
+
           mf : ≤-monotonic-f A f 
-          mf x ax = ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf x ax ) ⟫
+          mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
+             mf00 : * x < * (f x)
+             mf00 = proj1 ( mf< x ax )
 
-          pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
+          pzc : {z : Ordinal} → z o< x → ZChain A f mf< ay z
           pzc {z} z<x = prev z z<x
 
           ysp =  MinSUP.sup (ysup f mf ay)
@@ -1262,7 +1267,7 @@
           zeq : {xa xb z : Ordinal } 
              → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 
              → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z  
-          zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf ay xa≤xb  
+          zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  supf-unique A f mf< ay xa≤xb  
               (pzc xa<x)  (pzc xb<x)  z≤xa
 
           iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y 
@@ -1340,9 +1345,8 @@
           is-minsup :  {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)
           is-minsup = ?
 
-          cfcs : (mf< : <-monotonic-f A f) {a b w : Ordinal } 
-                 → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
-          cfcs mf< {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
+          cfcs :  {a b w : Ordinal } → a o< b → b o≤ x →  supf1 a o< b → FClosure A f (supf1 a) w → odef (UnionCF A f ay supf1 b) w
+          cfcs {a} {b} {w} a<b b≤x sa<b fc with osuc-≡< b≤x
           ... | case1 b=x with trio< a x 
           ... | tri< a<x ¬b ¬c = zc40 where
                sa = ZChain.supf (pzc  (ob<x lim a<x)) a
@@ -1362,17 +1366,17 @@
                zc42 : osuc a o≤ osuc m
                zc42 = osucc (o<→≤ ( omax-x _ _ ) )
                sam<m : sam o< m
-               sam<m = subst (λ k → k o< m ) (supf-unique A f mf ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
+               sam<m = subst (λ k → k o< m ) (supf-unique A f mf< ay zc42 (pzc (ob<x lim a<x)) (pzc (ob<x lim m<x)) (o<→≤ <-osuc)) ( omax-y _ _ )
                fcm : FClosure A f (ZChain.supf (pzc (ob<x lim m<x)) a) w
                fcm = subst (λ k → FClosure A f k w ) (zeq (ob<x lim a<x) (ob<x lim m<x) zc42 (o<→≤ <-osuc) ) fc
                zcm : odef (UnionCF A f ay (ZChain.supf (pzc  (ob<x lim m<x))) (osuc (omax a sa))) w
-               zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
+               zcm = ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                zc40 : odef (UnionCF A f ay supf1 b) w
-               zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) mf< (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
+               zc40 with ZChain.cfcs (pzc  (ob<x lim m<x)) (o<→≤ (omax-x _ _)) o≤-refl (o<→≤ sam<m) fcm
                ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫  
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬a (ordtrans<-≤ a<b b≤x))
-          cfcs mf< {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
+          cfcs {a} {b} {w} a<b b≤x sa<b fc | case2 b<x = zc40 where
                supfb =  ZChain.supf (pzc (ob<x lim b<x)) 
                sb=sa : {a : Ordinal } → a o< b → supf1 a ≡ ZChain.supf (pzc (ob<x lim b<x)) a 
                sb=sa {a} a<b = trans (sf1=sf (ordtrans<-≤ a<b b≤x)) (zeq _ _ (o<→≤ (osucc a<b)) (o<→≤ <-osuc) )
@@ -1380,7 +1384,7 @@
                fcb = subst (λ k → FClosure A f k w) (sb=sa a<b) fc 
                --  supfb a o< b assures it is in Union b
                zcb : odef (UnionCF A f ay supfb b) w
-               zcb = ZChain.cfcs (pzc (ob<x lim b<x)) mf< a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
+               zcb = ZChain.cfcs (pzc (ob<x lim b<x)) a<b (o<→≤ <-osuc) (subst (λ k → k o< b) (sb=sa a<b) sa<b) fcb
                zc40 : odef (UnionCF A f ay supf1 b) w
                zc40 with zcb
                ... | ⟪ az , cp  ⟫ = ⟪ az , ? ⟫ 
@@ -1398,15 +1402,15 @@
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
 
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x
-     SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z  } (λ x → ind f mf ay x   ) x
+     SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf< ay x
+     SZ f mf< {y} ay x = TransFinite {λ z → ZChain A f mf< ay z  } (λ x → ind f mf< ay x   ) x
 
-     msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
-         → (zc : ZChain A f mf ay x )
+     msp0 : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
+         → (zc : ZChain A f mf< ay x )
          → MinSUP A (UnionCF A f ay (ZChain.supf zc) x)
-     msp0 f mf {x} ay zc = minsupP (UnionCF A f ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
+     msp0 f mf< {x} ay zc = minsupP (UnionCF A f ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) (ZChain.f-total zc)
 
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (mf< : <-monotonic-f A f )  (zc : ZChain A f mf< as0 (& A) )
             → (sp1 : MinSUP A (ZChain.chain zc))
             → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
      fixpoint f mf mf< zc sp1 = z14 where
@@ -1454,24 +1458,13 @@
                ... | case1 eq = ¬b (cong (*) eq)
                ... | case2 lt = ¬a lt
 
-     tri : {n : Level} (u w : Ordinal ) { R : Set n }  → ( u o< w → R ) → ( u ≡  w → R ) → ( w o< u → R ) → R
-     tri {_} u w p q r with trio< u w
-     ... | tri< a ¬b ¬c = p a
-     ... | tri≈ ¬a b ¬c = q b
-     ... | tri> ¬a ¬b c = r c
-
-     or : {n m r : Level } {P : Set n } {Q : Set m} {R : Set r}  → P ∨ Q → ( P → R ) → (Q → R ) → R
-     or (case1 p) p→r q→r = p→r p
-     or (case2 q) p→r q→r = q→r q
-
-
      -- ZChain contradicts ¬ Maximal
      --
      -- 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 (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-<-monotonic nmx) as0 (& A)) → ⊥
      z04 nmx zc = <-irr0  {* (cf nmx c)} {* c}
            (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.as  msp1 ))))
            (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
@@ -1480,7 +1473,7 @@
 
           supf = ZChain.supf zc
           msp1 : MinSUP A (ZChain.chain zc)
-          msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
+          msp1 = msp0 (cf nmx) (cf-is-<-monotonic nmx) as0 zc
           c : Ordinal
           c = MinSUP.sup msp1
 
@@ -1494,7 +1487,7 @@
          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 (SZ (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) )) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx (SZ (cf nmx) (cf-is-<-monotonic nmx) as0 (& A) )) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where