# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663226671 -32400
# Node ID 2eaa61279c361457744ca15372a04eba437433e0
# Parent  f9fc8da87b5aeb58e8e1d90dd2d533f41a297b78
...

diff -r f9fc8da87b5a -r 2eaa61279c36 src/zorn.agda
--- a/src/zorn.agda	Thu Sep 15 03:32:06 2022 +0900
+++ b/src/zorn.agda	Thu Sep 15 16:24:31 2022 +0900
@@ -351,27 +351,6 @@
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
-zsupf0 : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)  
-        → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
-        → { z : Ordinal } → (odef A z) → SUP A (UnionCF A f mf ay (λ _ → z) z)
-zsupf0 A f mf ay supP {z} az =  supP chain (λ lt → proj1 lt ) f-total where
-    chain = UnionCF A f mf ay (λ _ → z) z
-    f-total : IsTotalOrderSet chain
-    f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay (λ _ → z) ( (proj2 ca)) ( (proj2 cb))
-
-record ZSupf ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
-        {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
-
 --
 --         f (f ( ... (sup y))) f (f ( ... (sup z1)))
 --        /          |         /             |
@@ -379,59 +358,6 @@
 --    sup y   <       sup z1          <    sup z2
 --           o<                      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
-zsupf A f mf {y} ay supP x = TransFinite { λ x →  ZSupf A f mf ay x } zc1 x where
-
-    zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZSupf A f mf ay y₁) → ZSupf A f mf ay x
-    zc1 x prev with Oprev-p x
-    ... | yes op = record { supf = ? ; sup = ? ; supf-is-sup = ? ; supf-mono = ? }  where
-       px = Oprev.oprev op
-       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 
-
-       supf : Ordinal → Ordinal
-       supf 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 = ZSupf.supf (prev px (pxo<x op) ) px
-
-       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 pchain0 ? f )   
-       ... | case1 pr = ?
-       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain0 ax )
-       ... | case2 ¬x=sup = ?
-       ... | case1 is-sup = ?
-
-    ... | no lim = ?  where
-
-       --  Range of supf is total order set, so it has SUP
-       supfmax :  Ordinal
-       supfmax = ?
-
-       supfx :  Ordinal
-       supfx with ODC.∋-p O A (* x)
-       ... | no noax = supfmax
-       ... | yes ax with ODC.p∨¬p O ( HasPrev A ? x f )   
-       ... | case1 pr = supfmax
-       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A ? ax )
-       ... | case2 ¬x=sup = supfmax
-       ... | case1 is-sup = ?
-
-       supf : Ordinal → Ordinal
-       supf z with trio< z x
-       ... | tri< a ¬b ¬c = ZSupf.supf (prev z a) z
-       ... | tri≈ ¬a b ¬c = supfx
-       ... | tri> ¬a ¬b px<x = supfx
-
-
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -447,9 +373,8 @@
            → 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-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
       csupf : {b : Ordinal } → supf b o≤ z → odef (UnionCF A f mf ay supf z) (supf b) 
-
-
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
    f-next : {a : Ordinal} → odef chain a → odef chain (f a)
@@ -466,6 +391,13 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay supf ( (proj2 ca)) ( (proj2 cb)) 
 
+   supf-<= : {x y : Ordinal } → supf x <= supf  y → supf x o≤ supf y
+   supf-<= {x} {y} (case1 sx=sy) = o≤-refl0 sx=sy
+   supf-<= {x} {y} (case2 sx<sy) with trio< (supf x) (supf y)
+   ... | tri< a ¬b ¬c = o<→≤ a
+   ... | tri≈ ¬a b ¬c = o≤-refl0 b
+   ... | tri> ¬a ¬b c = ⊥-elim (<-irr (case2 sx<sy ) (supf-< c) )
+
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y 
    supf-inject {x} {y} sx<sy with trio< x y
    ... | tri< a ¬b ¬c = a
@@ -474,7 +406,11 @@
    ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
-   -- ordering is proved here for totality and sup
+   supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x
+   supf-idem = ?
+
+   x≤supfx : {x : Ordinal } → x o≤ supf x
+   x≤supfx = ?
 
    supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
    supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
@@ -485,6 +421,7 @@
    ... | 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 )
 
+   -- ordering is not proved here but in ZChain1 
 
 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
@@ -494,36 +431,6 @@
           → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
 
-initial-segment : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
-        {a b y : Ordinal} (ay : odef A y)  (za : ZChain A f mf ay a ) (zb : ZChain A f mf ay b ) 
-        →  {z : Ordinal } → a o≤ b → z o≤ a
-        → ZChain.supf za z ≡ ZChain.supf zb z
-initial-segment A f mf {a} {b} {y} ay za zb {z} a≤b z≤a = TransFinite0 { λ x → x o≤ a → ZChain.supf za x ≡ ZChain.supf zb x } ind z z≤a where
-      ind :  (x : Ordinal) → ((z : Ordinal) → z o< x → z o≤ a → ZChain.supf za z ≡ ZChain.supf zb z ) →
-            x o≤ a → ZChain.supf za x ≡ ZChain.supf zb x
-      ind x prev x≤a = ? where
-          supfa = ZChain.supf za 
-          supfb = ZChain.supf zb 
-          zc10 : {w : Ordinal } → w o< z → UnionCF A f mf ay supfa w ≡ UnionCF A f mf ay supfb w 
-          zc10 = ?
-            -- w o< z → supfa w ≡ supfb w
-          supa : SUP A (UnionCF A f mf ay supfa x)
-          supa = ZChain.sup za x≤a
-          supb : SUP A (UnionCF A f mf ay supfb x)
-          supb = ZChain.sup zb (OrdTrans x≤a a≤b)
-          zc13 : UnionCF A f mf ay supfa x ≡ UnionCF A f mf ay supfb x 
-          zc13 = ? --
-             -- if x is sup of UCF px (or Union o< x ) , then supfa x ≡ x supfb x
-             -- if x is not sup of UCF px (or Union o< x ) or HasPrev, UCF x ≡ UCF px (or Union o< x)
-          zc15 : {B : HOD} → (a b : SUP A B) → SUP.sup a ≡ SUP.sup b
-          zc15 = ?
-          zc14 : supfa x ≡ supfb x
-          zc14 = begin 
-             supfa x ≡⟨ ? ⟩
-             & (SUP.sup supa) ≡⟨ ? ⟩
-             & (SUP.sup supb) ≡⟨ ? ⟩
-             supfb x ∎ where open ≡-Reasoning
-
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -637,11 +544,13 @@
                 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 ? is-sup fc ⟫ where
+                ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 zc08) is-sup fc ⟫ where
                     zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
                     zc07 = fc
                     zc06 : supf u ≡ u
                     zc06 = ChainP.supu=u is-sup
+                    zc08 : u o≤ supf s  
+                    zc08 = subst (λ k → k o≤ supf s) zc06 (ZChain.supf-<= zc (≤to<= ( s≤fc _ f mf fc )))
                     zc09 : u o≤ supf s  →  u o< b 
                     zc09 u≤s with osuc-≡< u≤s
                     ... | case1 u=ss = ZChain.supf-inject zc (subst (λ k → k o< supf b) (sym (trans zc06 u=ss)) ss<sb )
@@ -824,25 +733,15 @@
           supf0 = ZChain.supf zc
           pchain  : HOD
           pchain   = UnionCF A f mf ay supf0 px
-          pchain1 : HOD
-          pchain1  = UnionCF A f mf ay supf0 x
 
-          supfx : {z : Ordinal } → x o≤ z →  supf0 px ≡ supf0 z
-          supfx {z} x≤z with trio< z px
-          ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
-          ... | 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)
+          -- ¬ supf0 px ≡ px → UnionCF supf0 px ≡ UnionCF supf1 x 
+          --       supf1 x ≡ supf0 px
+          --   supf0 px ≡ px → ( UnionCF A f mf ay supf0 px ∪ FClosure px ) ≡ UnionCF supf1 x 
+          --       supf1 x ≡ sup of ( UnionCF A f mf ay supf0 px ∪ FClosure px (= UnionCF supf1 x))) ≥ supf0 px
 
           supf-mono : {a b : Ordinal } → a o≤ b → supf0 a o≤ supf0 b 
           supf-mono = ZChain.supf-mono zc
 
-          supf-max : {z : Ordinal} → x o≤ z → supf0 x ≡ supf0 z
-          supf-max {z} z≤x = trans ( sym zc02) zc01 where
-              zc02 : supf0 px ≡ supf0 x
-              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)
@@ -859,8 +758,41 @@
           --           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 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
-              ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
+          no-extension P with osuc-≡< (ZChain.x≤supfx zc)
+          ... | case1 sfpx=px = ?
+                 pchainpx : HOD
+                 pchainpx = record { od = record { def = λ z →  UChain A f mf ay supf0 z x ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
+                      zc00 : {z : Ordinal } → UChain A f mf ay supf0 z x ∨ FClosure A f px z → z o< & A
+                      zc00 = ?
+
+                 sup1 : SUP A (pchainpx sfpx=px )
+                 sup1 = supP ? ? ?
+
+                 sp1 : Ordinal
+                 sp1 = & (SUP.sup (sup1 sfpx=px ))
+
+                 supf1 : Ordinal → Ordinal
+                 supf1 z with trio< z px 
+                 ... | tri< a ¬b ¬c = supf0 z
+                 ... | tri≈ ¬a b ¬c = supf0 z
+                 ... | tri> ¬a ¬b c = sp1 sfpx=px
+
+                 pchainp : HOD
+                 pchainp = UnionCF A f mf ay (supfp sfpx=px  ) x
+
+
+          ... | case2 px<spfx = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
+              ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
+
+                 supfp : Ordinal → Ordinal
+                 supfp lt z with trio< z px 
+                 ... | tri< a ¬b ¬c = supf0 z
+                 ... | tri≈ ¬a b ¬c = supf0 z
+                 ... | tri> ¬a ¬b c = supf0 px
+
+                 pchain1 : (sfpx=px : px o< supfp px ) → HOD
+                 pchain1 lt  = UnionCF A f mf ay supfp x
+
                  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  ⟫
@@ -980,32 +912,12 @@
                 record {  supf = supf1 
                    ; sup=u = {!!} ; supf-mono = {!!}
                    ; sup = {!!} ; supf-is-sup = {!!}   }  where
-             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 = x --- SUP A (UnionCF A f mf ay supf0 px) ≡ SUP A (UnionCF A f mf ay supf1 px) 
-
-             pchainx : HOD
-             pchainx = UnionCF A f mf ay supf1 x
 
              supf0px=x : (ax : odef A x) → IsSup A (ZChain.chain zc ) ax → x ≡  & (SUP.sup (ZChain.sup zc o≤-refl ) )
              supf0px=x is-sup = ? where
                  zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
                  zc50 = ZChain.supf-is-sup zc ?
 
-             supf-monox : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b
-             supf-monox {i} {j} i≤j with trio< i px | trio< j px
-             ... | tri< a ¬b ¬c | tri< ja ¬jb ¬jc  = ?
-             ... | tri< a ¬b ¬c | tri≈ ¬ja jb ¬jc  = ?
-             ... | tri< a ¬b ¬c | tri> ¬ja ¬jb jc  = ?
-             ... | tri≈ ¬a b ¬c | tri< ja ¬jb ¬jc  = ?
-             ... | tri≈ ¬a b ¬c | tri≈ ¬ja jb ¬jc  = ?
-             ... | tri≈ ¬a b ¬c | tri> ¬ja ¬jb jc  = ?
-             ... | tri> ¬a ¬b c | tri< ja ¬jb ¬jc  = ?
-             ... | tri> ¬a ¬b c | tri≈ ¬ja jb ¬jc  = ?
-             ... | tri> ¬a ¬b c | tri> ¬ja ¬jb jc  = ?
-
              pchain⊆x : UnionCF A f mf ay supf0 px ⊆'  UnionCF A f mf ay supf1 x
              pchain⊆x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
              pchain⊆x ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ au , ch-is-sup u ? ? ? ⟫ 
@@ -1039,19 +951,12 @@
 
           ysp =  & (SUP.sup (ysup f mf ay))
 
-          initial-segment0 : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x)  → a o< b  → z o≤ a 
-             → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z
-          initial-segment0 = ?
-
           supf0 : Ordinal → Ordinal
           supf0 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
           ... | tri≈ ¬a b ¬c = ysp
           ... | tri> ¬a ¬b c = ysp
 
-          
-          -- Union of UnionCF z, z o< x undef initial-segment condition                                                                 
-          --   this is not a ZChain because supf0 is not monotonic
           pchain : HOD
           pchain = UnionCF A f mf ay supf0 x