# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659658967 -32400
# Node ID bcc241fbb390f18ac70a54e10b4aefdf097577cd
# Parent  150e1c7097ce60f9bad7c175f9ad69386bcaea0d
...

diff -r 150e1c7097ce -r bcc241fbb390 src/zorn.agda
--- a/src/zorn.agda	Thu Aug 04 06:59:40 2022 +0900
+++ b/src/zorn.agda	Fri Aug 05 09:22:47 2022 +0900
@@ -276,7 +276,8 @@
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u : Ordinal) : Set n where
    field
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 
-      order    : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+      order    : {s z1 : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
+      supu=u   : o∅ o< u → supf u ≡ u
 
 -- Union of supf z which o< x
 --
@@ -492,21 +493,26 @@
      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  ) ⟫
 
+     chain-mono :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 
+       {a b c : Ordinal} → a o≤ b
+            → odef (UnionCF A f mf ay supf a) c → odef (UnionCF A f mf ay supf b) c
+     chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
+            ⟪ ua , ch-init fc  ⟫ 
+     chain-mono f mf ay supf {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
+            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (osucc a≤b )) is-sup fc  ⟫ 
+
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) ) 
         (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
      sp0 f mf 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
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
-     SZ1 :( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+     SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
-     SZ1 A f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
-        chain-mono1 : (x : Ordinal) {a b c : Ordinal} → a o≤ b
+     SZ1 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
+        chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
-        chain-mono1 x {a} {b} {c} a≤b ⟪ ua , ch-init fc  ⟫ = 
-            ⟪ ua , ch-init fc  ⟫ 
-        chain-mono1 x {a} {b} {c} a≤b ⟪ uaa ,  ch-is-sup ua ua<x is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua (ordtrans<-≤ ua<x (osucc a≤b )) is-sup fc  ⟫ 
+        chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
             b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f → 
@@ -533,14 +539,14 @@
               b<A = z09 ab
               m05 : b ≡ ZChain.supf zc b
               m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 x (osucc b<x) uz )  }  )
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz )  }  )
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
               m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
               m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record {  fcy<sup = m08  ; order = m09 } 
+              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = λ _ → ZChain.sup=u zc ab b<A ? } 
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -549,7 +555,7 @@
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
            ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
-           ... | case2 y<b = chain-mono1 x (osucc b<x) 
+           ... | case2 y<b = chain-mono1 (osucc b<x) 
              ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫ where
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
@@ -560,9 +566,9 @@
               m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
               m05 : b ≡ ZChain.supf zc b
               m05 = sym (ZChain.sup=u zc ab m09
-                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 x (osucc b<x) lt )} )   -- ZChain on x
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} )   -- ZChain on x
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record { fcy<sup = m07 ;  order = m08 }
+              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = λ _ → ZChain.sup=u zc ab m09 ? }
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -576,7 +582,7 @@
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & 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
-           z10 = ZChain1.is-max (SZ1 A f mf as0 zc (& A) )
+           z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z11 : & (SUP.sup sp1) o< & A
            z11 = c<→o< ( SUP.A∋maximal sp1)
            z12 : odef chain (& (SUP.sup sp1))
@@ -641,8 +647,8 @@
        →  SUP A (uchain f mf ay)
      ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
-     inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = ? ; supf-is-sup = ? 
+     initChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
+     initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = ? ; supf-is-sup = ? 
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; supf-mono = mono ; csupf = csupf } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
@@ -681,8 +687,10 @@
                uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
                uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
                uz02 :  ChainP A f mf ay isupf o∅
-               uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
+               uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = λ lt → ⊥-elim ( o<¬≡ refl lt ) }
 
+     SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
+     SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; A∋maximal = SUP.A∋maximal sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
 
      --
      -- create all ZChains under o< x
@@ -725,25 +733,26 @@
 
           supf0 = ZChain.supf zc
 
+          sup1 : SUP A (UnionCF A f mf ay supf0 x)
+          sup1 = supP pchain pchain⊆A ptotal
+          sp1 = & (SUP.sup sup1 )
+          supf1 : Ordinal → Ordinal
+          supf1 z with trio< z px
+          ... | tri< a ¬b ¬c = ZChain.supf zc z
+          ... | tri≈ ¬a b ¬c = ZChain.supf zc z
+          ... | tri> ¬a ¬b c = sp1
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
-          no-extension : ZChain A f mf ay x
-          no-extension = record { supf = supf1 ; supf-mono = ? ; sup = sup
+          no-extension : ¬  sp1 ≡ x → ZChain A f mf ay x
+          no-extension ¬sp=x = record { supf = supf1 ; supf-mono = ? ; sup = sup
                ; initial = ? ; chain∋init = ?  ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? 
               ;  chain⊆A = ? ;  f-next = ? ;  f-total = ? }  where
-                 sup1 : SUP A (UnionCF A f mf ay supf0 x)
-                 sup1 = supP pchain pchain⊆A ptotal
-                 sp1 = & (SUP.sup sup1 )
-                 supf1 : Ordinal → Ordinal
-                 supf1 z with trio< z px
-                 ... | tri< a ¬b ¬c = ZChain.supf zc z
-                 ... | tri≈ ¬a b ¬c = ZChain.supf zc z
-                 ... | tri> ¬a ¬b c = sp1
                  UnionCF⊆ : UnionCF A f mf ay supf1 x ⊆' UnionCF A f mf ay supf0 x 
                  UnionCF⊆ ⟪ as , ch-init fc ⟫ = UnionCF⊆ ⟪ as , ch-init fc ⟫ 
-                 UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1  }  fc ⟫ with trio< u px
-                 ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 } fc ⟫  where
+                 UnionCF⊆ ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = o1 ; supu=u = su=u1 }  fc ⟫ with trio< u px
+                 ... | tri< a ¬b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 ; supu=u = ? } fc ⟫  where
                      order0 : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 
                         → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
                      order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
@@ -752,7 +761,7 @@
                      ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
                                                                           (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
                      ... | tri> ¬a ¬b c | record {eq = eq1} = ?
-                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0 } fc ⟫ where
+                 ... | tri≈ ¬a b ¬c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = f1 ; order = order0  ; supu=u = ?} fc ⟫ where
                      order0 : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 
                         → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
                      order0 {s} {z1} ss<su fc with trio< s px | inspect supf1 s
@@ -760,41 +769,48 @@
                                                                           (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
                      ... | tri≈ ¬a b ¬c | record {eq = eq1} = o1 {s} {z1} (subst (λ k → k o< supf0 u) (sym eq1) ss<su )  
                                                                           (subst (λ k → FClosure A f k z1 ) (sym eq1) fc )
-                     ... | tri> ¬a ¬b c | record {eq = eq1} = ?
-                 ... | tri> ¬a ¬b c = ⟪ as , ch-is-sup u {z} u≤x record { fcy<sup = fcy<sup ; order = order } fc0 ⟫  where
-                     --    px o< u , u o< osuc x → u ≡ x
-                     --    supf0 x ≡ sp1 ≡ x
-                     --         u≤x → supf0 u < x
-                     fc1 :  FClosure A f sp1 z
-                     fc1 = fc
-                     fc0 :  FClosure A f (supf0 u) z
-                     fc0 = ?
-                     fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u)
-                     fcy<sup {z} fc = ?
-                     order : {s z1 : Ordinal}  → supf0 s o< supf0 u → FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u)
-                     order = ?
+                     ... | tri> ¬a ¬b px<s | record {eq = eq1} = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x ? )) where
+                         s≤u : s o≤ u
+                         s≤u = ?
+                         u=x : u ≡ x
+                         u=x with trio< u x
+                         ... | tri< a ¬b ¬c = ?
+                         ... | tri≈ ¬a b ¬c = b
+                         ... | tri> ¬a ¬b c = ?
+                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ k ) u=x (su=u1 ?) )) where
+                      u=x : u ≡ x
+                      u=x with trio< u x
+                      ... | tri< a ¬b ¬c = ?
+                      ... | tri≈ ¬a b ¬c = b
+                      ... | tri> ¬a ¬b c = ?
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = ? -- ZChain.sup zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup zc (o≤-refl0 b)
-                 ... | tri> ¬a ¬b c = ? --  sp1
+                 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup zc (o<→≤ a))
+                 ... | tri≈ ¬a b ¬c = SUP⊆ ? (ZChain.sup zc (o≤-refl0 b))
+                 ... | tri> ¬a ¬b c = SUP⊆ ? sup1
 
           zc4 : ZChain A f mf ay x 
-          zc4 with ODC.∋-p O A (* px)
-          ... | no noapx = no-extension -- ¬ A ∋ p, just skip
-          ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f )   
+          zc4 with ODC.∋-p O A (* x)
+          ... | no noax = no-extension ? -- ¬ A ∋ p, just skip
+          ... | 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 x
-          ... | case1 pr = no-extension -- 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 (ZChain.chain zc ) apx )
+          ... | case1 pr = no-extension ? -- 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 (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} 
                    ; supf-mono = {!!} ; initial = {!!} ; chain∋init  = {!!} ; sup = ? ; supf-is-sup = ? ; supf-mono = ? }  where
+             supx : SUP A (UnionCF A f mf ay supf0 x)
+             supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) ? ax ; x<sup = ? }
+             spx = & (SUP.sup supx )
+             x=spx : x ≡ spx
+             x=spx = ?
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf zc z
              ... | tri≈ ¬a b ¬c = x
              ... | tri> ¬a ¬b c = x
-          ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
+
+          ... | case2 ¬x=sup =  no-extension ? -- px is not f y' nor sup of former ZChain from y -- no extention
 
      ... | no lim = zc5 where
 
@@ -856,7 +872,7 @@
                       ... | case1 eq = case1 (trans eq (sym eq1) )
                       ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
                       cp1 : ChainP A f mf ay psupf z 
-                      cp1 = record {  fcy<sup = zc20   ; order = ? } 
+                      cp1 = record {  fcy<sup = zc20   ; order = ?  ; supu=u = ?} 
                      ---  u = supf u = supf z 
           ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? {!!} {!!} {!!} ⟫ where
                 sa = SUP.A∋maximal usup