# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663004989 -32400
# Node ID 35a884f2bfde8eda432e72a0776a21fce3b665ca
# Parent  166bee3ddf4c79fb048e8f009ca96d1b8b6dab88
...

diff -r 166bee3ddf4c -r 35a884f2bfde src/zorn.agda
--- a/src/zorn.agda	Mon Sep 12 19:35:32 2022 +0900
+++ b/src/zorn.agda	Tue Sep 13 02:49:49 2022 +0900
@@ -365,6 +365,9 @@
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf : Ordinal → Ordinal
+   pchain : HOD
+   pchain = UnionCF A f mf ay supf z 
+   field
       sup : (x : Ordinal ) → SUP A (UnionCF A f mf ay (λ _ → z) x)
       supf-is-sup : {x : Ordinal } → supf x ≡ & (SUP.sup (sup x) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
@@ -376,28 +379,6 @@
 --    sup y   <       sup z1          <    sup z2
 --           o<                      o<
 
-smono→SUPU : (A : HOD) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)  
-   → {x z : Ordinal } → { supf : Ordinal → Ordinal } 
-   → ( supf x ≡ z ) → ( {x y : Ordinal } → x o≤  y → supf x o≤ supf y )
-                      → ( {x y : Ordinal } → x o≤  y → supf x <= supf y )
-   → (sz : SUP A (UnionCF A f mf ay (λ _ → z) x)) → (su : SUP A (UnionCF A f mf ay supf x)) → & (SUP.sup sz) ≡ & (SUP.sup su)
-smono→SUPU A f mf {y} ay {x} {z} {supf} sx=z mono mono< s = ? where
-      sup = SUP.sup s
-      x<sup : {w : HOD} → (UnionCF A f mf ay supf x) ∋ w → (w ≡ sup ) ∨ (w < sup )   
-      x<sup {w} ⟪ au , ch-init fc ⟫ = SUP.x<sup s ⟪ au , ch-init fc ⟫ 
-      x<sup {w} ⟪ au , ch-is-sup u u<x is-sup fc ⟫ with trio< u z
-      ... | tri< a ¬b ¬c = ?  where
-            zc01 :  {s : Ordinal} → (lt : supf s o< supf u ) → FClosure A f (supf s ) (& w) → ((& w) ≡ supf u ) ∨ ( (& w)  << supf u )
-            zc01 = ChainP.order is-sup 
-      ... | tri≈ ¬a b ¬c = ?
-      ... | tri> ¬a ¬b z<u = ⊥-elim ( o≤> u≤z z<u ) where
-            u≤z :  u o≤ z
-            u≤z = begin u ≡⟨ sym (ChainP.supu=u is-sup)  ⟩ 
-                  supf u  ≤⟨ mono (o<→≤ u<x  )  ⟩ 
-                  supf x  ≡⟨ sx=z ⟩ 
-                  z  ∎ where open  o≤-Reasoning O 
-
-
 zsupf : (A : HOD) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) 
     → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     →  (x : Ordinal)   → ZSupf A f mf ay x
@@ -407,8 +388,8 @@
     zc1 x prev with Oprev-p x
     ... | yes op = record { supf = ? ; sup = ? ; supf-is-sup = ? ; supf-mono = ? }  where
        px = Oprev.oprev op
-       pchain : HOD
-       pchain = UnionCF A f mf ay (ZSupf.supf ( prev px (pxo<x op) )) px
+       pchain0 : HOD
+       pchain0 = UnionCF A f mf ay (ZSupf.supf ( prev px (pxo<x op) )) px
        zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
        zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
@@ -418,18 +399,14 @@
        ... | tri≈ ¬a b ¬c = ZSupf.supf (prev z (subst (λ k → k o< x ) (sym b) (pxo<x op))) z
        ... | tri> ¬a ¬b px<x = ZSupf.supf (prev px (pxo<x op) ) px
 
-       supf1 : Ordinal → Ordinal
-       supf1 z with trio< z px
-       ... | tri< a ¬b ¬c = ZSupf.supf (prev z (ordtrans a (pxo<x op))) z
-       ... | tri≈ ¬a b ¬c = ZSupf.supf (prev z (subst (λ k → k o< x ) (sym b) (pxo<x op))) z
-       ... | tri> ¬a ¬b px<x = & (SUP.sup (zsupf0 A f mf ay supP ax))
+       sp1 =  & (SUP.sup (zsupf0 A f mf ay supP ? )) 
 
        zc2 : ZSupf A f mf ay x
        zc2 with ODC.∋-p O A (* x)
        ... | no noax = ?
-       ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain z f )   
+       ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain0 ? f )   
        ... | case1 pr = ?
-       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
+       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain0 ax )
        ... | case2 ¬x=sup = ?
        ... | case1 is-sup = ?
 
@@ -459,6 +436,7 @@
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal 
+      asupf :  {x : Ordinal } → odef A (supf x)
    chain : HOD
    chain = UnionCF A f mf ay supf z
    chain⊆A : chain ⊆' A
@@ -469,8 +447,7 @@
            → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      supf-max : {x : Ordinal } → z o< x  → supf (osuc z) ≡ supf x
-      csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf (supf b)) (supf b) 
+      order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
@@ -507,35 +484,6 @@
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
 
-   csupf-fc : {b s z1 : Ordinal} → b o≤ z → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
-   csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05  where
-            s<b : s o< b
-            s<b = supf-inject ss<sb
-            s≤<z : s o≤ z
-            s≤<z = ordtrans s<b b≤z
-            zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
-            zc04 = csupf s≤<z 
-            zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
-            zc05 with zc04
-            ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-            ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u<x ) is-sup fc ⟫ where
-                zc06 : supf u ≡ u
-                zc06 = ChainP.supu=u is-sup
-                zc09 : u o< supf s  →  u o< b 
-                zc09 u<s = ordtrans (supf-inject (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b
-   csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
-            zc04 : odef (UnionCF A f mf ay supf b) (f x)
-            zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
-            ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
-            ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 
-   order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-   order {b} {s} {z1} b<z ss<sb fc = zc04 where
-      zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z) ) )
-      zc00 = SUP.x<sup (sup (o<→≤  b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
-      zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
-      zc04 with zc00
-      ... | 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
@@ -673,6 +621,9 @@
         ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , 
                  subst (λ k → UChain A f mf ay (ZChain.supf zc) x k )
                       (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x is-sup (fsuc _ fc))  ⟫ 
+
+        supf1 = ZChain.supf zc
+
         zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZChain1 A f mf ay zc y₁) → ZChain1 A f mf ay zc x
         zc1 x prev with Oprev-p x
         ... | yes op = record { is-max = is-max } where
@@ -847,12 +798,6 @@
           ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
           ... | tri> ¬a ¬b c = ? --  ZChain.supf-max zc (o<→≤ c)
 
-          supf∈A : {b : Ordinal} → b o≤ x → odef A (supf0 b)
-          supf∈A {b} b≤z with trio< b px
-          ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a ))
-          ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b ))
-          ... | tri> ¬a ¬b c = ? -- subst (λ k → odef A k ) (ZChain.supf-max zc (o<→≤ c)) ? -- (proj1 ( ZChain.csupf zc o≤-refl))
-
           supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b 
           supf-mono = ZChain.supf-mono zc
 
@@ -862,6 +807,7 @@
               zc02 = ? -- ZChain.supf-max zc (o<→≤ (pxo<x op))
               zc01 : supf0 px ≡ supf0 z
               zc01 = ? -- ZChain.supf-max zc (OrdTrans (o<→≤ (pxo<x op)) z≤x)
+
           zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
           zc04 {b} b≤x with trio< b px 
           ... | tri< a ¬b ¬c = case1 (o<→≤ a)
@@ -878,8 +824,8 @@
           --           supf0 px ≡ supf0 x 
 
           no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
-          no-extension P = record { supf = supf0 ;  sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono ; supf-max = ?
-              ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) ; csupf = csupf }  where
+          no-extension P = record { supf = supf0 ;  asupf = ? ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
+              ; order = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
                  zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                  zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup  fc  ⟫
@@ -919,7 +865,7 @@
                         zc12 : supf0 x ≡ u1
                         zc12 = subst  (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup)
                         zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
-                        zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl)
+                        zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc)
                                  ; is-sup = record { x<sup = x<sup } }
                  zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where
                         eq : u1 ≡ x 
@@ -957,7 +903,7 @@
                      ... | case1 lt = SUP.x<sup zc32 lt 
                      ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
-                     zc33 = trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
+                     zc33 = ? -- trans (sym (supfx (o≤-refl0 (sym zc30)))) ( ZChain.supf-is-sup zc o≤-refl  )
                      zc36 : ¬ (supf0 px ≡ px) → STMP z≤x
                      zc36 ne = record { tsup = record { sup = SUP.sup zc32 ; as = SUP.as zc32 ; x<sup = zc34 ne } ; tsup=sup = zc33  } 
                      zc35 : STMP z≤x
@@ -987,12 +933,6 @@
                      zc31 (case2 hasPrev ) with zc30
                      ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev 
                                 ; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } ) 
-                 csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf0 (supf0 b)) (supf0 b)
-                 csupf {b} b≤x with zc04 b≤x 
-                 ... | case2 b=x = subst (λ k → odef (UnionCF A f mf ay supf0 k) k) ? ( ZChain.csupf zc o≤-refl ) where
-                     zc05 : px o≤ b
-                     zc05 = subst (λ k → px o≤ k) (sym b=x) (o<→≤ (pxo<x op) )
-                 ... | case1 b≤px = ZChain.csupf zc b≤px 
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -1002,8 +942,8 @@
           ... | case1 pr = no-extension (case2 pr) -- 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 = supf1 ; supf-max = ?
-                   ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!}
+                record {  supf = supf1 
+                   ; sup=u = {!!} ; supf-mono = {!!}
                    ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supf1 : Ordinal → Ordinal
              supf1 z with trio< z px 
@@ -1050,13 +990,6 @@
                      zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                      zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ?
 
-             csupf :  {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b)
-             csupf {b} b≤x with zc04 b≤x 
-             ... | case2 b=x = ⟪ ? , ch-is-sup x ? ? (init ? ? ) ⟫
-             ... | case1 b≤px with ZChain.csupf zc b≤px 
-             ... | ⟪ au , ch-init fc ⟫ = ⟪ ? , ch-init ? ⟫ 
-             ... | ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ? , ch-is-sup u ? ? ? ⟫ 
-
 
           ... | case2 ¬x=sup =  no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention
              nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x 
@@ -1119,8 +1052,8 @@
           zc70 pr xsup = ?
 
           no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
-          no-extension ¬sp=x  = record { supf = supf1  ; sup=u = sup=u 
-               ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; csupf = csupf } where
+          no-extension ¬sp=x  = record { supf = supf1  ; sup=u = sup=u  ; order = ? 
+               ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
                  pchain0=1 : pchain ≡ pchain1
@@ -1160,15 +1093,6 @@
                  ... | tri< a ¬b ¬c = ? -- ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x<sup = {!!} }
                  ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
-                 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 (supf1 z)) (supf1 z)
-                 csupf {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = ?  where
-                     zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
-                     zc9 = {!!}
-                     zc8 : odef (UnionCF A f mf ay (supfu a) z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
-                     zc8 = {!!} -- ZChain.csupf  (pzc (osuc z) (ob<x lim a)) ? -- (o<→≤ <-osuc )
-                 ... | tri≈ ¬a b ¬c = {!!}
-                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x )) 
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
@@ -1178,7 +1102,7 @@
           ... | case1 pr = no-extension {!!} 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = record { supf = supf1  ; sup=u = {!!} 
-               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  csupf = {!!}  } -- where -- x is a sup of (zc ?) 
+               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = {!!};  asupf = {!!}  } -- where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)