# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651365404 -32400
# Node ID 666377324edde4a6e13334bf244adc1407ee8b0d
# Parent  4d8a54e2861e69a0893cab84ed973f3e1fe7553a
...

diff -r 4d8a54e2861e -r 666377324edd src/zorn.agda
--- a/src/zorn.agda	Sun May 01 05:35:36 2022 +0900
+++ b/src/zorn.agda	Sun May 01 09:36:44 2022 +0900
@@ -110,10 +110,10 @@
 fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where
      fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → * x ≡ * y
      fc00 zero zero refl (init _) (init x₁) i=x i=y = refl
-     fc00 zero zero refl (init sa) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init sa) cy i=x i=y )
-     fc00 zero zero refl (fsuc x cx) (init sa) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
-     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init sa) i=x i=y )
+     fc00 zero zero refl (init as) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
+     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as) cy i=x i=y )
+     fc00 zero zero refl (fsuc x cx) (init as) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
+     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as) i=x i=y )
      fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
      ... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy  i=x i=y )
      fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
@@ -184,7 +184,7 @@
            cxx :  FClosure A f s (f x)
            cxx = fsuc x cx 
            fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx  ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx))
-           fc16 x (init sa) with proj1 (mf s sa )
+           fc16 x (init as) with proj1 (mf s as )
            ... | case1 _ = case1 refl
            ... | case2 _ = case2 refl
            fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) )
@@ -206,13 +206,10 @@
 IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b)  → Tri (a < b) (a ≡ b) (b < a )
 
 ⊆-IsTotalOrderSet : { A B : HOD } →  B ⊆ A  → IsTotalOrderSet A → IsTotalOrderSet B
-⊆-IsTotalOrderSet = {!!}
+⊆-IsTotalOrderSet {A} {B} B⊆A T  ax ay = T (incl B⊆A ax) (incl B⊆A ay)
 
-record Maximal ( A : HOD )  : Set (Level.suc n) where
-   field
-      maximal : HOD
-      A∋maximal : A ∋ maximal
-      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
+_⊆'_ : ( A B : HOD ) → Set n
+_⊆'_ A B = {x : Ordinal } → odef A x → odef B x
 
 --
 -- inductive maxmum tree from x
@@ -225,16 +222,34 @@
       ay : odef B y
       x=fy :  x ≡ f y 
 
-_⊆'_ : ( A B : HOD ) → Set n
-_⊆'_ A B = (x : Ordinal ) → odef A x → odef B x
-
-record IsSup (A : HOD) (T : IsTotalOrderSet A) {x : Ordinal }
-    (xa : odef A x)  (sup : (C : HOD ) → ( C ⊆ A) → IsTotalOrderSet C → Ordinal) ( f : Ordinal → Ordinal )  : Set n where
+record IsSup (A B : HOD) (T : IsTotalOrderSet B) {x : Ordinal } ( B⊆A :  B ⊆' A )
+    (xa : odef A x)  (sup : (C : HOD ) → ( C ⊆' A) → IsTotalOrderSet C → Ordinal) ( f : Ordinal → Ordinal )  : Set n where
    field
       chain : Ordinal
-      chain⊆A : (* chain) ⊆' A
+      chain⊆B : (* chain) ⊆' B
+      x=sup :  x ≡ sup  (* chain) ( λ lt → B⊆A (chain⊆B lt ) ) 
+                   ( ⊆-IsTotalOrderSet {B} {* chain} record { incl = chain⊆B } T ) 
       -- ¬prev : ¬ HasPrev A (* chain) xa f
-      x=sup :  x ≡ sup  (* chain)  record { incl = λ {x} → chain⊆A (& x) } ( ⊆-IsTotalOrderSet {A} {* chain} record { incl = λ {x} → chain⊆A (& x) } T ) 
+
+record ZChain ( A : HOD )  {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
+                 (sup : (C : HOD ) → ( C ⊆' A) → IsTotalOrderSet C → Ordinal) ( z : Ordinal ) : Set (Level.suc n) where
+   field
+      chain : HOD
+      chain⊆A : chain ⊆' A
+      chain∋x : odef chain x
+      initial : {y : Ordinal } → odef chain y → * x ≤ * y
+      f-total : IsTotalOrderSet chain 
+      f-next : {a : Ordinal } → odef chain a → odef chain (f a)
+      f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
+      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 f-total chain⊆A ab sup f       --  ((sup  chain  chain⊆A  f-total) ≡ b )
+          → * a < * b  → odef chain b
+
+record Maximal ( A : HOD )  : Set (Level.suc n) where
+   field
+      maximal : HOD
+      A∋maximal : A ∋ maximal
+      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
@@ -245,26 +260,12 @@
 SupCond : ( A B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → Set (Level.suc n)
 SupCond A B _ _ = SUP A B  
 
-record ZChain ( A : HOD )  {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
-                 (sup : (C : HOD ) → ( C ⊆ A) → IsTotalOrderSet C → Ordinal) ( z : Ordinal ) : Set (Level.suc n) where
-   field
-      chain : HOD
-      chain⊆A : chain ⊆ A
-      chain∋x : odef chain x
-      initial : {y : Ordinal } → odef chain y → * x ≤ * y
-      f-total : IsTotalOrderSet chain 
-      f-next : {a : Ordinal } → odef chain a → odef chain (f a)
-      f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
-      is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ba : odef A b) 
-          → HasPrev A chain ba f ∨  ((sup  chain  chain⊆A  f-total) ≡ b )
-          → * a < * b  → odef chain b
-
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
-    → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
+    → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A 
 Zorn-lemma {A}  0<A supP = zorn00 where
-     supO : (C : HOD ) → C ⊆ A → IsTotalOrderSet C → Ordinal
+     supO : (C : HOD ) → C ⊆' A → IsTotalOrderSet C → Ordinal
      supO C C⊆A TC = & ( SUP.sup ( supP  C  C⊆A TC ))
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      z01 {a} {b} A∋a A∋b = <-irr
@@ -272,10 +273,10 @@
      z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      s : HOD
      s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
-     sa : A ∋ * ( & s  )
-     sa =  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 ))  )
+     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 ))  )
      s<A : & s o< & A
-     s<A = c<→o< (subst (λ k → odef A (& k) ) *iso sa )
+     s<A = c<→o< (subst (λ k → odef A (& k) ) *iso as )
      HasMaximal : HOD
      HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) →  odef A m → ¬ (* x < * m)) }  ; odmax = & A ; <odmax = z07 } 
      no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
@@ -309,12 +310,12 @@
      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 sa f mf supO (& A) ) → SUP A  (ZChain.chain zc) 
+     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A as f mf supO (& 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 sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A) ) 
+     A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A as (cf nmx) (cf-is-≤-monotonic nmx) supO (& 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 (subst (λ k → odef A k ) &iso sa ) f mf supO (& A) ) → SUP A (ZChain.chain zc)
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso as ) f mf supO (& A) ) → SUP A (ZChain.chain zc)
      sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) 
      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)
@@ -322,13 +323,13 @@
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
-     z03 :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO (& A) )
+     z03 :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso as ) f mf supO (& A) )
             → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
      z03 f mf zc = z14 where
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
-              →  HasPrev A chain ab f ∨  (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
+              →  HasPrev A chain ab f ∨  IsSup A chain (ZChain.f-total zc) (ZChain.chain⊆A zc) ab supO f -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
            z10 = ZChain.is-max zc
            z11 : & (SUP.sup sp1) o< & A
@@ -336,11 +337,13 @@
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)  (case2 refl ) z13 where
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)  (case2 z19 ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 ( ZChain.chain∋x zc )
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
+               z19 : IsSup A chain (ZChain.f-total zc) (ZChain.chain⊆A zc) (SUP.A∋maximal sp1) supO f
+               z19 = {!!}
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
            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
@@ -362,7 +365,7 @@
      -- ZChain forces fix point on any ≤-monotonic function (z03)
      -- ¬ 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 (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (subst (λ k → odef A k ) &iso as ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥
      z04 nmx zc = z01  {* (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 (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc )))
@@ -385,42 +388,42 @@
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
           zc4 : ZChain A ay f mf supO x 
           zc4 with ODC.∋-p O A (* x)
-          ... | no noapx =  -- ¬ A ∋ p, just skip
+          ... | 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
                      ; 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 → (ba : odef A b) →
-                    HasPrev A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
+                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) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f  →
                             * a < * b → odef (ZChain.chain zc0) b
-                zc11 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
-                ... | case1 eq = ⊥-elim ( noapx (subst (λ k → odef A k) (trans eq (sym &iso)) ba ) )
-                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt )  ba P a<b
-          ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO x
+                zc11 {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 zc0 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 zc0) ax f )   -- we have to check adding x preserve is-max ZChain A ay 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
                 chain = ZChain.chain zc0
-                zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-                            HasPrev A (ZChain.chain zc0) ba f ∨ (supO (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0) ≡ b) →
+                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) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f →
                             * a < * b → odef (ZChain.chain zc0) b
-                zc17 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt) ba P a<b
+                zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
+                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt) ab P a<b
                 ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
                 zc9 :  ZChain A ay f mf supO 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
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
-          ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ax supO f)
           ... | case1 x=sup = -- previous ordinal is a sup of a smaller ZChain
-                 record { chain = schain ; chain⊆A = record { incl = A∋schain } ; f-total = scmp ; f-next = scnext 
-                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax } where -- x is sup
+                 record { chain = schain ; chain⊆A = {!!}  ; f-total = scmp ; f-next = scnext 
+                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup
                 sup0 = supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) 
                 sp = SUP.sup sup0 
                 chain = ZChain.chain zc0
                 sc<A : {y : Ordinal} → odef chain y ∨ FClosure A f (& sp) y → y o< & A
-                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx )))
+                sc<A {y} (case1 zx) = {!!} -- subst (λ k → k o< (& A)) &iso ( c<→o< ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx )))
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
-                A∋schain (case1 zx ) = subst (λ k → odef A k ) &iso (incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx ))
+                A∋schain (case1 zx ) = {!!} -- subst (λ k → odef A k ) &iso (incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx ))
                 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
                 cmp  : {a b : HOD} (za : odef chain (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
                 cmp {a} {b} za fb  with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb  
@@ -455,7 +458,7 @@
                 ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x )
                 ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) )
                 A∋za : {a : Ordinal } → odef chain a → odef A a
-                A∋za za = (subst (λ k → odef A k ) &iso (incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k ) (sym &iso) za) ) )
+                A∋za za = {!!} -- (subst (λ k → odef A k ) &iso (incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k ) (sym &iso) za) ) )
                 za<sup :  {a : Ordinal } → odef chain a → ( * a ≡ sp ) ∨  ( * a < sp )
                 za<sup za =  SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) za )
                 simm : {a b : Ordinal}  → odef schain a → odef schain b → ¬ (* a < * b) ∧ (* b < * (f a))
@@ -475,34 +478,34 @@
                 ... | case2 sp<a | case1 b=sp = <-irr (case2 (subst ( λ  k → k < * a ) (trans *iso (sym b=sp)) sp<a  )) (proj1 p )
                 ... | case2 sp<a | case2 b<sp = <-irr (case2 (ptrans b<sp (subst (λ k → k < * a) *iso sp<a ))) (proj1 p )
                 simm {a} {b} (case2 sa) (case2 sb) p = fcn-imm {A} (& sp) {a} {b} f mf sa sb p
-                s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ba : odef A b) →
-                    HasPrev A schain ba f ∨ (& (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b)
+                s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A schain ab f ∨ IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f
                      → * a < * b → odef schain b
-                s-ismax {a} {b} (case1 za) b<x ba (case1 p) a<b with osuc-≡< b<x
-                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
+                s-ismax {a} {b} (case1 za) b<x ab (case1 p) a<b with osuc-≡< b<x
+                ... | case1 b=x = case2 {!!} -- (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
                 ... | case2 b<x = z21 p where
-                     z21 : HasPrev A schain ba f → odef schain b
+                     z21 : HasPrev A schain ab f → odef schain b
                      z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 
-                           case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
+                           case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
                      z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
-                s-ismax {a} {b} (case1 za) b<x ba (case2 p) a<b with osuc-≡< b<x
-                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
+                s-ismax {a} {b} (case1 za) b<x ab (case2 p) a<b with osuc-≡< b<x
+                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) {!!} (init (SUP.A∋maximal sup0) ))
                 ... | case2 b<x = z22 p  where
-                     z22 : & (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b → odef schain b
+                     z22 : IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f → odef schain b
                      z22 p = {!!}
-                -- case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba {!!} a<b )
-                s-ismax {a} {b} (case2 sa) b<x ba p a<b = {!!}
+                -- case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ab {!!} a<b )
+                s-ismax {a} {b} (case2 sa) b<x ab p a<b = {!!}
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
                    record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 }  where -- no extention
-                z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-                            HasPrev A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
+                z18 :  {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) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f →
                             * a < * b → odef (ZChain.chain zc0) b
-                z18 {a} {b} za b<x ba p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  lt ) ba p a<b 
+                z18 {a} {b} za b<x ab p a<b with osuc-≡< b<x
+                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  lt ) ab p a<b 
                 ... | case1 b=x with p
                 ... | 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 (sym (trans  b=sup  b=x )) )
+                ... | case2 b=sup = ⊥-elim ( ¬x=sup {!!} )
      ... | no ¬ox =  {!!}  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
@@ -533,8 +536,8 @@
               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 ya f mf supO (& A)
          zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A ya f mf supO z } (ind f mf) (& A)
-         zorn04 : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)
-         zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso sa )
+         zorn04 : ZChain A (subst (λ k → odef A k ) &iso as ) (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)
+         zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 
 -- usage (see filter.agda )
 --