# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660017177 -32400
# Node ID 7c6612b753b9564944b1c1b2d42692bc3e949f90
# Parent  358c33d3a2bd827839d0454cdb782a1b061ef53d
...

diff -r 358c33d3a2bd -r 7c6612b753b9 src/zorn.agda
--- a/src/zorn.agda	Tue Aug 09 08:43:03 2022 +0900
+++ b/src/zorn.agda	Tue Aug 09 12:52:57 2022 +0900
@@ -245,7 +245,7 @@
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
 --    whole chain is a union of separated Chain
---    minimum index is y not ϕ 
+--    minimum index is sup of y not ϕ 
 --
 
 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
@@ -254,9 +254,6 @@
       order    : {s z1 : Ordinal} → (lt : s o< u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
       supu=u   : supf u ≡ u
 
--- Union of supf z which o< x
---
-
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
     ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain A f mf ay supf x z
@@ -266,6 +263,8 @@
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
+-- Union of supf z which o< x
+--
 UnionCF : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) 
     ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
 UnionCF A f mf ay supf x
@@ -285,16 +284,17 @@
       f-total : IsTotalOrderSet chain
 
       sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
-      sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
+      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
 
+   -- ordering is proved here for totality and sup
+
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
-
        
    order : {b s z1 : Ordinal} → b o< z → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z s<b fc = zc04 where
@@ -318,7 +318,6 @@
       ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  (o<→≤ b<z) ) ) (cong (&) eq) )
       ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z) ) )))  lt )
 
-
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -477,6 +476,10 @@
      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)
 
+     --
+     -- Second TransFinite Pass for maximality
+     --
+
      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 f mf {y} ay zc x = TransFinite { λ x →  ZChain1 A f mf ay zc x } zc1 x where
@@ -508,7 +511,7 @@
               b<A : b o< & A
               b<A = z09 ab
               m05 : b ≡ ZChain.supf zc b
-              m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
+              m05 = sym ( ZChain.sup=u zc ab (o<→≤ (z09 ab)) 
                       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 (o<→≤ b<A) fcz
@@ -516,7 +519,7 @@
                            → 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 ; supu=u = ZChain.sup=u zc ab b<A 
+              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A )
                       record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz ) } }  
         ... | 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 →
@@ -536,10 +539,10 @@
                        → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
               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
+              m05 = sym (ZChain.sup=u zc ab (o<→≤ m09)
                       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 ; supu=u = ZChain.sup=u zc ab m09 
+              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab (o<→≤ m09)
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} } 
 
      ---
@@ -621,7 +624,7 @@
 
      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) ; csupf = {!!} } where
+      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ? ; csupf = {!!} } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
           isupf z = spi
@@ -712,13 +715,27 @@
           ... | tri≈ ¬a b ¬c = ZChain.supf zc z
           ... | tri> ¬a ¬b c = sp1
 
+          pchain1 : HOD
+          pchain1  = UnionCF A f mf ay supf1 x
+          pcy1 : odef pchain1 y
+          pcy1 = ⟪ ay , ch-init (init ay refl)    ⟫
+          pinit1 :  {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁
+          pinit1 {a} ⟪ aa , ua ⟫  with  ua
+          ... | ch-init fc = s≤fc y f mf fc
+          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
+               zc7 : y <= supf1 u 
+               zc7 = ChainP.fcy<sup is-sup (init ay refl)
+          pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
+          pnext1 {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
+          pnext1 {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
+
           -- 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 : ¬  sp1 ≡ x → ZChain A f mf ay x
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
-               ; initial = {!!} ; chain∋init = {!!}  ; sup=u = {!!} ; supf-is-sup = {!!} ; csupf = {!!} 
-              ;  chain⊆A = {!!} ;  f-next = ? ;  f-total = {!!} }  where
+               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = {!!} 
+              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = {!!} }  where
                  UnionCF⊆ : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 x 
                  UnionCF⊆ {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
                  UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
@@ -731,6 +748,13 @@
                  ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ ? ) (ZChain.sup zc ? )
                  ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCF⊆ ? ) (ZChain.sup zc ? )
                  ... | tri> ¬a ¬b c = SUP⊆ (λ lt  → chain-mono f mf ay _ ? (UnionCF⊆ ? lt )) sup1
+                 sup=u : {b : Ordinal} (ab : odef A b) →
+                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                 sup=u {b} ab b<x is-sup with trio< b px
+                 ... | tri< a ¬b ¬c = ? where
+                     zc11 = ZChain.sup=u zc ab ? ?
+                 ... | tri≈ ¬a b ¬c = ? 
+                 ... | tri> ¬a ¬b c = ?
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -849,9 +873,9 @@
                  ... | tri> ¬a ¬b c with osuc-≡< z≤x
                  ... | case1 eq = ⊥-elim ( ¬b eq )
                  ... | case2 lt = ⊥-elim ( ¬a lt )
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o< x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
                  sup=u {b} ab b<x is-sup with trio< b x
-                 ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab <-osuc record { x<sup = {!!} }
+                 ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab ? record { x<sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b c = {!!}
                  csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)