changeset 608:6655f03984f9

mutual tranfinite in zorn
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Jun 2022 11:28:06 +0900
parents 74c0ae81e482
children 5039d228838c
files src/zorn.agda
diffstat 1 files changed, 68 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Jun 16 09:58:13 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 11:28:06 2022 +0900
@@ -240,14 +240,10 @@
       asup : odef A sup
       supf-isSup :  IsSup A (* chain) asup
 
-record ChainMono (A chain : HOD) (z : Ordinal) : Set n where
-      supf : (x : Ordinal) → SupF A 
-      supfz=chain : SupF.chain z ≡ & chain
-      supf-mono : {x y : Ordinal} → x o< y → y o< osuc z →  SupF.sup (supf x ) o< SupF.sup (supf y )
-
-record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (supf : Ordinal → SupF A) ( z : Ordinal ) : Set (Level.suc n) where
+   chain : HOD
+   chain = * (SupF.chain (supf z ))
    field
-      chain : HOD
       chain⊆A : chain ⊆' A
       chain∋x : odef chain x
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
@@ -257,7 +253,12 @@
       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
-      fc∨sup : ChainMono A chain z
+      supf-mono : {x y : Ordinal} → x o< y → y o< osuc z →  SupF.sup (supf x ) o< SupF.sup (supf y )
+
+record ZChain1 ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal )  ( z : Ordinal ) : Set (Level.suc n) where
+   field
+      supf : Ordinal → SupF A
+      zc : ZChain A x f supf z
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -289,6 +290,8 @@
      s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
      as : A ∋ * ( & s  )
      as =  subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))  )
+     as0 : odef A  (& s  )
+     as0 =  subst (λ k → odef A k ) &iso as
      s<A : & s o< & A
      s<A = c<→o< (subst (λ k → odef A (& k) ) *iso as )
      HasMaximal : HOD
@@ -328,24 +331,27 @@
      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) →  (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∋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) 
+     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) ( ZChain.f-total zc  )   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) (ZChain.f-total zc)   where
+           zc = ZChain1.zc zc1
      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) )
-            → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
-     fixpoint f mf zc = z14 where
+     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
            chain = ZChain.chain zc
-           sp1 = sp0 f mf zc
+           sp1 = sp0 f mf zc1
            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
@@ -368,7 +374,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))) ≡ & (SUP.sup (sp0 f mf zc))
+           z14 :  f (& (SUP.sup (sp0 f mf zc1))) ≡ & (SUP.sup (sp0 f mf zc1))
            z14 with ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
@@ -389,20 +395,21 @@
      -- 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)) → ⊥
-     z04 nmx zc = <-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 : 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))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc1 ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where          -- x < f x
-          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
+          zc = ZChain1.zc zc1
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc1
           c = & (SUP.sup sp1)
 
      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 = ys ay f mf ; chain⊆A = λ fx →  A∋fc y f mf fx
-                     ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx ; chain∋sup = {!!}
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = is-max ; fc∨sup = {!!} } where
+     init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain1 A y f  x
+     init-chain {y} {x} ay f mf x≤y = record { zc = record { chain⊆A = λ fx →  A∋fc y f mf {!!}
+                     ; f-total = {!!} ; f-next = λ {x} sx → {!!} 
+                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} } ; supf = {!!} } 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 →
@@ -416,8 +423,9 @@
      --
      -- create all ZChains under o< x
      --
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
-            ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A y f z ) → { y : Ordinal } → (ya : odef A y) → ZChain A y f x
+
+     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
      ind f mf x prev {y} ay with Oprev-p x
      ... | yes op = zc4 where
           --
@@ -426,19 +434,21 @@
           open ZChain
           
           px = Oprev.oprev op
-          zc0 : ZChain A y f (Oprev.oprev op)
-          zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
+          supf : Ordinal → SupF A
+          supf = ZChain1.supf (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 
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 
-          zc4 : ZChain A y f x 
+          zc4 : ZChain1 A y f x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
-                 record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
-                     ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 ; chain∋sup = {!!}
-                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} }  where -- no extention
+                 record { zc = record { chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
+                     ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11  } }  where -- no extention
                 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
@@ -446,7 +456,7 @@
                 ... | 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 = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+          ... | case1 pr = {!!}  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 →
@@ -454,14 +464,13 @@
                 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))
-                zc9 :  ZChain A y f x
-                zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
-                     ; chain∋sup = {!!}
-                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!}  } 
+                zc9 :  ZChain1 A y f x
+                zc9 = record { zc = record { chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!} -- no extention
+                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} } }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
-                record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext ; chain∋sup = {!!}
-                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = {!!} } where 
+                record { zc = record { chain = schain ; chain⊆A = {!!}  ; f-total = {!!} ; f-next = {!!} ; chain∋sup = {!!}
+                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} } } where 
                 sup0 : SUP A (ZChain.chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -573,19 +582,19 @@
                 ... | 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 = UnionZ where
-       UnionZ : ZChain A y f x
-       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next ; chain∋sup = {!!}
-                     ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
+     ... | no ¬ox = {!!} where
+       UnionZ : ZChain A y f {!!} x
+       UnionZ = record { chain = Uz ; chain⊆A = {!!} ; f-total = {!!}  ; f-next = {!!} ; chain∋sup = {!!}
+                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  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 {y} ay )) z
+               chain∋z : odef (ZChain.chain (ZChain1.zc (prev u u<x {y} ay ))) 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) {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⊆A {z} u = ZChain.chain⊆A (ZChain1.zc ( 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 =  ZChain1.zc (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))) }
@@ -594,8 +603,8 @@
          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 (prev y {!!} ay ) }
-         u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
+         u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (ZChain1.zc (prev y {!!} ay )) }
+         u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f {!!} a) (zb : ZChain A y f {!!} b) → ZChain.chain za  ⊆' ZChain.chain zb
          u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain za) i → odef (chain zb) i } uind i zai where
             open ZChain
             uind :  (i : Ordinal)
@@ -603,7 +612,7 @@
                  → odef (chain za) i → odef (chain zb) i
             uind i previ zai = um01 where
                 um01 : odef (chain zb) i
-                um01 = ?
+                um01 = {!!}
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
          ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)
@@ -613,6 +622,9 @@
          ... | 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)
+
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
@@ -629,10 +641,8 @@
          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) ) ⟫
-         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (& A)
-         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) (& A)
-         zorn04 : ZChain A (& s) (cf nmx)  (& A)
-         zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
+         zorn04 : ZChain1 A (& s) (cf nmx) (& A)
+         zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 
 -- usage (see filter.agda )
 --