# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657354250 -32400
# Node ID 9ab62416dbdd4dc5099717785944ff3643847402
# Parent  6a9a98904f7ac09d34a4642d1b728f3a557bfe18
...

diff -r 6a9a98904f7a -r 9ab62416dbdd src/zorn.agda
--- a/src/zorn.agda	Sat Jul 09 16:34:04 2022 +0900
+++ b/src/zorn.agda	Sat Jul 09 17:10:50 2022 +0900
@@ -260,14 +260,14 @@
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
-      psup :  Ordinal
-      p≤z : psup o≤ z 
-      p≤a : psup o≤ & A 
-      chainf : {px : Ordinal} → px o≤ z → (w : Ordinal) →  Chain A f mf ay px w
+      psup :  Ordinal → Ordinal 
+      psup<z : (x : Ordinal ) →   psup x o< & A 
+      chainf : (x w : Ordinal) → x o< z  →  Chain A f mf ay (psup x ) w
+      psup-mono : (x y : Ordinal) → x o≤ y → psup x o≤ psup y 
 
 ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) 
      → (z : Ordinal) →  ( ( x : Ordinal ) → ZChain1 A f mf ay x ) →  HOD
-ChainF A f mf {y} ay z zc = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup (zc z) ) x } 
+ChainF A f mf {y} ay z zc = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup (zc (& A)) x ) x } 
          ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy } 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
@@ -432,18 +432,18 @@
           sc : ZChain1 A f mf ay px
           sc = prev px px<x
           pchain : HOD
-          pchain  = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup sc ) x } 
+          pchain  = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup sc ? ) x } 
              ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy } 
 
           sc4 : ZChain1 A f mf ay x
           sc4 with o≤? x o∅
-          ... | yes x=0 = record { psup =  o∅ ; p≤z = ? ; p≤a = ? ; chainf = ? }
+          ... | yes x=0 = record { psup =  ? ; p≤z = ? ; p≤a = ? ; chainf = ? }
           ... | no 0<x with ODC.∋-p O A (* x)
           ... | no noax = record { psup = ZChain1.psup sc ; p≤z = ? ; p≤a = ? ; chainf = ? }
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
           ... | case1 pr = record { psup = ZChain1.psup sc ; p≤z = ? ; p≤a = ? ; chainf = ? }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { psup = x ; p≤z = ? ; p≤a = ? ; chainf = ? } where
+          ... | case1 is-sup = record { psup = ?  ; p≤z = ? ; p≤a = ? ; chainf = ? } 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 }
@@ -464,7 +464,7 @@
           -- chainq z z<x = ? -- ZChain1.chain-uniq ( prev z z<x)
           sc4 : ZChain1 A f mf ay x
           sc4 with o≤? x o∅
-          ... | yes x=0 = record { psup =  o∅ ; p≤z = ? ; p≤a = ? ; chainf = ? }
+          ... | yes x=0 = record { psup =  ? ; p≤z = ? ; p≤a = ? ; chainf = ? }
           ... | no 0<x with ODC.∋-p O A (* x)
           ... | no noax = record { psup = ? ; p≤z = ? ; p≤a = ? ; chainf = ? } 
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )   
@@ -505,7 +505,7 @@
                             * a < * b → odef (ZChain.chain (zc ?) ) b ) → ZChain A f mf ay zc0 x
           no-extenion is-max with o≤? x (& A)
           ... | no n = ? where
-          ... | yes x≤a with ZChain1.chainf (zc0 (& A)) x≤a x
+          ... | yes x≤a with ZChain1.chainf (zc0 (& A)) ?  ? ?
           ... | ch-init _ _  x=0 fc = ?
           ... | ch-is-sup ax is-sup fc = ? where
           -- = record { chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)