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

diff -r a48845e246e4 -r 6a9a98904f7a src/zorn.agda
--- a/src/zorn.agda	Sat Jul 09 11:16:57 2022 +0900
+++ b/src/zorn.agda	Sat Jul 09 16:34:04 2022 +0900
@@ -262,20 +262,21 @@
    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
-      chain-mono1 : (px : Ordinal) → (x≤p : px o≤ psup ) → (w : Ordinal ) →  Chain A f mf ay px w → Chain A f mf ay psup w 
 
 ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) 
-     → (z : Ordinal) →  ZChain1 A f mf ay (& A) →  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) x } ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy } 
+     → (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 } 
+         ; 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)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = ChainF A f mf ay z (zc0 (& A))
+   chain = ChainF A f mf ay z zc0 
    field
       chain-mono : (px py : Ordinal) → (px≤py : px o≤ py ) (y≤x : py o≤ z ) → (w : Ordinal ) 
-          → Chain A f mf ay (ZChain1.psup (zc0 (& A))) px → Chain A f mf ay (ZChain1.psup (zc0 (& A))) py
+          → ChainF A f mf ay px zc0  ⊆' ChainF A f mf ay py zc0 
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
@@ -430,16 +431,19 @@
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
           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 } 
+             ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy } 
+
           sc4 : ZChain1 A f mf ay x
-          sc4 with ODC.∋-p O A (* x)
-          ... | no noax = ?
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A ? ax f )   
-          ... | case1 pr = ? where -- 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 ? ax )
-          ... | case1 is-sup = ? where -- record { chain = schain ; chain-uniq = sc9 } where
+          sc4 with o≤? x o∅
+          ... | yes x=0 = record { psup =  o∅ ; 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
                 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 }
@@ -447,8 +451,8 @@
                 sc7 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
                 -- 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 = ? where --- record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } where
+                    -- record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-kjjkjjsup lt) }
+          ... | case2 ¬x=sup = record { psup = ZChain1.psup sc ; p≤z = ? ; p≤a = ? ; chainf = ? } where
                 sc17 : ¬ HasPrev A ? (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 ? (subst (λ k → odef A k) &iso ax)
@@ -459,10 +463,12 @@
           -- 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
-          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) ?  } 
+          sc4 with o≤? x o∅
+          ... | yes x=0 = record { psup =  o∅ ; 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 )   
-          ... | case1 pr = record { chain = UnionCF A x chainf  ; chain-uniq = ? } -- ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? } 
+          ... | case1 pr = record { psup = ? ; p≤z = ? ; p≤a = ? ; chainf = ? } 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax )
           ... | case1 is-sup = ?
           ... | case2 ¬x=sup = ?
@@ -479,7 +485,7 @@
               --
               px = Oprev.oprev op
               supf : Ordinal → HOD
-              supf x =  ChainF A f mf ay x (zc0 (& A))
+              supf x =  ChainF A f mf ay x zc0 
               -- zc : ZChain A f mf ay zc0 (Oprev.oprev op)
               -- zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
               px<x : px o< x
@@ -494,8 +500,8 @@
 
           -- 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 →
+          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain (zc z<x )) a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A (ZChain.chain (zc z<x) ) ab f ∨  IsSup A (ZChain.chain (zc z<x) ) ab →
                             * 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
@@ -526,24 +532,26 @@
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
           zc4 : ZChain A f mf ay zc0 x 
-          zc4 with ODC.∋-p O A (* x)
+          zc4 with o≤? x o∅
+          ... | yes x=0 = ?
+          ... | no 0<x with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1  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
-                zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
+                zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A (ZChain.chain (zc ?) ) ab f ∨  IsSup A (ZChain.chain (zc z<x) ) ab →
+                            * a < * b → odef (ZChain.chain (zc z<x) ) b
+                zc1 {a} {b} z<x 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 (zc ?) za ?  ab P a<b
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain (zc ?) ) ax f )   
+                ... | case2 lt = ZChain.is-max (zc z<x) za ?  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
-                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 →
-                            * a < * b → odef (ZChain.chain (zc ?) ) b
-                zc7 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max (zc ?) za ? 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 (zc ?) (HasPrev.ay pr))
+                chain0 = ZChain.chain (zc ? ) 
+                zc7 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) →
+                            HasPrev A (ZChain.chain (zc z<x) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) ) ab →
+                            * a < * b → odef (ZChain.chain (zc z<x) ) b
+                zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
+                ... | case2 lt = ZChain.is-max (zc z<x) za ? 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 (zc z<x) (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain (zc ?) ) ax )
           ... | case1 is-sup = -- x is a sup of (zc ?) 
                 record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!}
@@ -646,15 +654,15 @@
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
           ... | case2 ¬x=sup =  no-extenion z18 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
-                z18 {a} {b} za b<x ab p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max (zc ?) za ? ab p a<b 
+                z18 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) →
+                            HasPrev A (ZChain.chain (zc ?) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) )   ab →
+                            * a < * b → odef (ZChain.chain (zc z<x) ) b
+                z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x
+                ... | case2 lt = ZChain.is-max (zc z<x) za ? 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 ) } )
+                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = ? ; 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)  } ) 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup ? )  } ) 
          
      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