# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656937538 -32400
# Node ID 431d074311f51b4e1d66f4f0d6ed2dc06f0f07ea
# Parent  1002866230b8d4a450d83d34b2a9a2db11ac7a34
do all in sind

diff -r 1002866230b8 -r 431d074311f5 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 04 07:41:30 2022 +0900
+++ b/src/zorn.agda	Mon Jul 04 21:25:38 2022 +0900
@@ -254,7 +254,7 @@
 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  HOD  → Set (Level.suc n) where
-    ch-init    : Chain A f mf  ay o∅  record { od = record { def = λ z → FClosure A f y z  } ; odmax = & A ; <odmax = λ {y} sy → ? }
+    ch-init    : (x : Ordinal) → x ≡ o∅ → Chain A f mf  ay x  record { od = record { def = λ z → FClosure A f y z  } ; odmax = & A ; <odmax = λ {y} sy → ? }
     ch-noax    : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f mf  ay (Oprev.oprev op) chain) → Chain A f mf  ay x chain
     ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) 
         ( c : Chain A f mf ay (Oprev.oprev op) chain) ( h :  HasPrev A chain ax f ) → Chain A f mf ay x chain
@@ -289,10 +289,9 @@
       chain : HOD
       chain-uniq : Chain A f mf ay z chain 
 
-record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) ( z : Ordinal ) (zc0 :  ZChain1 A f mf ay z )  : Set (Level.suc n) where
-   chain : HOD
-   chain = ZChain1.chain zc0
+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
+      chain : HOD
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
@@ -365,7 +364,7 @@
      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 mf as0 (& A) ) (zc : ZChain A f mf as0 (& A) zc0  ) 
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A) ) (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 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
@@ -374,7 +373,7 @@
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A)) (zc : ZChain A f mf as0 (& A) zc0 )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A)) (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
@@ -423,7 +422,7 @@
      -- 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) (cf-is-≤-monotonic nmx)  as0 (& A)) (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) zc0 ) 
+     z04 :  (nmx : ¬ Maximal A ) → (zc0 : ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 (& 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 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
@@ -438,25 +437,25 @@
      --
 
      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
+         → ((z : Ordinal) → z o< x → ZChain1 A f mf ay z ∧ ZChain A f mf ay z ) → ZChain1 A f mf ay x  ∧ ZChain A f mf 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 mf ay px
-          sc = prev px px<x
-          sc4 : ZChain1 A f mf ay x
+          sc : ZChain1 A f mf ay px 
+          sc = proj1 (prev px px<x)
+          sc4 : ZChain1 A f mf ay x ∧ ZChain A f mf ay x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = record { chain = chain sc ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc )  } 
+          ... | no noax = ⟪ record { chain = chain sc ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc )  }  , ? ⟫
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc ) ax f )   
-          ... | case1 pr = record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) 
-                                       record { y = HasPrev.y pr  ; ay = HasPrev.ay pr  ; x=fy = sc6 } } where
+          ... | case1 pr = ⟪ record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) 
+                                       record { y = HasPrev.y pr  ; ay = HasPrev.ay pr  ; x=fy = sc6 } } , ? ⟫ where
                 sc6 : x ≡ f (HasPrev.y pr)
                 sc6 = subst (λ k → k ≡ f (HasPrev.y pr) ) &iso  ( HasPrev.x=fy pr  )
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc ) ax )
-          ... | case1 is-sup = record { chain = schain ; chain-uniq = sc9 } where
+          ... | case1 is-sup = ⟪ record { chain = schain ; chain-uniq = sc9 } , ? ⟫ where
                 schain : HOD
                 schain = record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
                     ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
@@ -465,27 +464,27 @@
                 sc9 : Chain A f mf ay x schain
                 sc9 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc7
                     record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-sup lt) }
-          ... | case2 ¬x=sup = record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } where
+          ... | case2 ¬x=sup = ⟪ record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } , ? ⟫ where
                 sc17 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
                 sc17 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
                 sc10 : ¬ IsSup A (chain sc) (subst (λ k → odef A k) &iso ax)
                 sc10 not = ¬x=sup ( record { x<sup  = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) }  )
      ... | no ¬ox = sc4 where
           chainf : (z : Ordinal) → z o< x → HOD
-          chainf z z<x = ZChain1.chain ( prev z z<x )
+          chainf z z<x = ZChain1.chain ( proj1 (prev z z<x ) )
           chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
-          chainq z z<x = ZChain1.chain-uniq ( prev z z<x)
-          sc4 : ZChain1 A f mf ay x
+          chainq z z<x = ZChain1.chain-uniq ( proj1 ( prev z z<x) )
+          sc4 : ZChain1 A f mf ay x ∧ ZChain A f mf ay x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = record { chain = UnionCF A x chainf ; chain-uniq = ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ? ? } 
+          ... | no noax = ⟪ record { chain = UnionCF A x chainf ; chain-uniq = ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ? ? }  , ? ⟫
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )   
-          ... | case1 pr = record { chain = UnionCF A x chainf  ; chain-uniq = ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? ? } 
+          ... | case1 pr = ⟪ record { chain = UnionCF A x chainf  ; chain-uniq = ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? ? } , ? ⟫
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax )
           ... | case1 is-sup = ?
           ... | case2 ¬x=sup = ?
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
-         → ((z : Ordinal) → z o< x → (zc1 : ZChain1 A f mf ay z) → ZChain A f mf ay z zc1 ) → (zc0 :  ZChain1 A f mf ay x ) → ZChain A f mf ay x zc0 
+         → ((z : Ordinal) → z o< x → (zc1 : ZChain1 A f mf ay z) → ZChain A f mf ay z ) → (zc0 :  ZChain1 A f mf ay x ) → ZChain A f mf ay x 
      ind f mf {y} ay x prev zc0 with Oprev-p x
      ... | yes op = zc4 where
           --
@@ -494,7 +493,7 @@
           px = Oprev.oprev op
           supf : Ordinal → HOD
           supf x = ZChain1.chain zc0 
-          zc : ZChain A f mf ay (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 ) 
           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 
@@ -503,35 +502,10 @@
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          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 mf ay x {!!}  
-          no-extenion is-max = record { chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A 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) 
-                     ; 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
-                supf0 z with trio< z x
-                ... | tri< a ¬b ¬c = supf z
-                ... | 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 
-                ... | tri> ¬a ¬b c = refl 
-                seq<x : {b : Ordinal } → b o< x →  supf b  ≡ supf0 b
-                seq<x {b} b<x with trio< b x
-                ... | tri< a ¬b ¬c = refl
-                ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
-                ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
-          zc4 : ZChain A f mf ay x zc0 
+          zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
+          ... | no noax = ? 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
@@ -539,7 +513,7 @@
                 ... | 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
-          ... | case1 pr = no-extenion zc7  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 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 →
@@ -646,9 +620,9 @@
                 seq<x {b} b<x with trio< b x
                 ... | tri< a ¬b ¬c = refl
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
-                ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
+                ... | tri> ¬a ¬b c  = ? -- ⊥-elim (¬a  b<x zc0 )
 
-          ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
+          ... | case2 ¬x=sup = ? where -- x is not f y' nor sup of former ZChain from y -- no extention
                 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
@@ -658,53 +632,51 @@
                 ... | 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 = {!!}
-                     ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
-         supf : Ordinal → HOD
-         supf x = ZChain1.chain zc0 
-         uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf 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 z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
-         u-next : {z : Ordinal} → odef Uz z → odef Uz (f 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} = {!!}
-         -- (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 )
-         supf0 : Ordinal → HOD
-         supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain1.chain zc0 
-         ... | 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 = {!!}
+     ... | no ¬ox = zc5 where --- limit ordinal case
+          chainf : (zc : ZChain1 A f mf ay x ) → (z : Ordinal) → z o< x → HOD
+          chainf zc z z<x = ?
+          uzc : HOD
+          uzc = UnionCF A x (chainf zc0)
+          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 uzc ax f )   -- we have to check adding x preserve is-max ZChain A y f mf zc0 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 uzc ax )
+          ... | case1 is-sup = ? -- x is a sup of zc 
+          ... | case2 ¬x=sup = ? where -- x is not f y' nor sup of former ZChain from y -- no extention
+              chainf0 : (zc : ZChain1 A f mf ay x ) → (z : Ordinal) → z o< x → HOD
+              chainf0 zc z z<x with ZChain1.chain-uniq zc0
+              ... | t = ?
+              supf : Ordinal → HOD
+              supf x = ZChain1.chain zc0 
+              Uz : HOD
+              Uz = UnionCF A x ( chainf0 zc0 )
+              u-next : {z : Ordinal} → odef Uz z → odef Uz (f 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} = {!!}
+              -- (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 )
+              supf0 : Ordinal → HOD
+              supf0 z with trio< z x
+              ... | tri< a ¬b ¬c = ZChain1.chain zc0 
+              ... | 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  ≡ supf0 b
-         seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = {!!} -- cong (λ k → (ZChain1.chain zc0) 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
          
-     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
+     SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x ∧ ZChain A f mf ay x
+     SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z ∧ ZChain 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 (& A) (SZ0 f mf ay (& A))  
-     SZ f mf {y} ay = TransFinite {λ z → (zc1 : ZChain1 A f mf ay z ) → ZChain A f mf ay z zc1  } (λ x zc0 → ind f mf ay x zc0   ) (& A) (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 → (zc1 : ZChain1 A f mf ay z ) → ZChain A f mf ay z } (λ x zc0 → ind f mf ay x zc0   ) (& A) ?
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -723,8 +695,8 @@
               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 (& A) (zc0 (& A)) 
+         zc0 x = proj1 ( 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 (& 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