# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659865158 -32400
# Node ID c8a166abcae03cb842a6047df47ecc2b90eaf593
# Parent  9cf74877efab99c5acaba1b755d16a87c8a3bdd8
...

diff -r 9cf74877efab -r c8a166abcae0 src/zorn.agda
--- a/src/zorn.agda	Sat Aug 06 18:24:53 2022 +0900
+++ b/src/zorn.agda	Sun Aug 07 18:39:18 2022 +0900
@@ -191,7 +191,7 @@
    field
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << 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
+      supu=u   : supf u ≡ u
 
 -- Union of supf z which o< x
 --
@@ -229,50 +229,56 @@
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
       supf≤x :{x : Ordinal } → z o≤ x → supf z ≡  supf x
 
-   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 (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
+   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 (o<→≤ u<z) ) ) ))
-   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
+   ... | 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 )
 
-   supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
-   supf-mono {x} {y} x<y = sf<sy where
-      --     supf x <<  supf y →   supf x o< supf y
-      --     x o<  y →   supf x <= supf y
-      --   z o≤ x → supf x ≡ supf y ≡ supf z
-      --   x o< z → z o< y → supf x ≡ supf y ≡ supf z
-      sf<sy : supf x o≤ supf y
-      sf<sy with trio< x z
-      ... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y ) <-osuc ) ) )) 
-      ... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y) b (o<→≤ x<y)))) 
-      ... | tri< x<z ¬b ¬c with trio< (supf x) (supf y)
+   supf-mono : {x y1 : Ordinal } → x o< y1 → supf x o≤ supf y1
+   supf-mono {x} {y1} x<y1 = sf<sy1 where
+      --     supf x <<  supf y1 →   supf x o< supf y1
+      --     x o<  y1 →   supf x <= supf y1
+      --   z o≤ x → supf x ≡ supf y1 ≡ supf z
+      --   x o< z → z o< y1 → supf x ≡ supf y1 ≡ supf z
+      supy : {x : Ordinal } → x o≤ z → FClosure A f y (supf x) → supf x ≡ y
+      supy {x} x≤z fcx = ? where
+          zc06 : ( * y  ≡  SUP.sup (sup x≤z )) ∨ ( * y  < SUP.sup ( sup x≤z ) )
+          zc06 = SUP.x<sup (sup x≤z) ⟪ subst (λ k → odef A k ) (sym &iso)  ay , ch-init (init ay (sym &iso) ) ⟫
+      sf<sy1 : supf x o≤ supf y1
+      sf<sy1 with trio< x z
+      ... | tri> ¬a ¬b c = o≤-refl0 (( trans (sym (supf≤x (o<→≤ c))) (supf≤x (ordtrans (ordtrans c x<y1 ) <-osuc ) ) )) 
+      ... | tri≈ ¬a b ¬c = o≤-refl0 (trans (sym (supf≤x (o≤-refl0 (sym b)))) (supf≤x (subst (λ k → k o< osuc y1) b (o<→≤ x<y1)))) 
+      ... | tri< x<z ¬b ¬c with trio< (supf x) (supf y1)
       ... | tri< a ¬b ¬c = o<→≤ a
       ... | tri≈ ¬a b ¬c = o≤-refl0 b
-      ... | tri> ¬a ¬b sy<sx with trio< z y
+      ... | tri> ¬a ¬b sy1<sx with trio< z y1
       ... | tri< a ¬b ¬c = ?
       ... | tri≈ ¬a b ¬c = ?
-      ... | tri> ¬a ¬b y<z = ?
-      zc04 : x o< z → y o< z → supf x o≤ supf y
-      zc04 x<z y<z with csupf (o<→≤ x<z) | csupf (o<→≤ y<z) 
-      ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy
+      ... | tri> ¬a ¬b y1<z = ?
+      zc04 : x o< z → y1 o≤ z → supf x o≤ supf y1
+      zc04 x<z y1≤z with csupf (o<→≤ x<z) | csupf y1≤z 
+      ... | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ with fcy<sup (o<→≤ x<z) fcy1
       ... | case1 eq = o≤-refl0 (sym eq)
-      ... | case2 lt with fcy<sup y<z fcx
+      ... | case2 lt with fcy<sup y1≤z fcx
       ... | case1 eq = o≤-refl0 eq
       ... | case2 lt1 = ⊥-elim ( <-irr (case2 lt) lt1 )
-      zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ with fcy<sup x<z fcy
+      zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ with fcy<sup (o<→≤ x<z) fcy1
       ... | case1 eq = o≤-refl0 (sym eq)
-      ... | case2 lt with ChainP.fcy<sup is-sup-x fcy 
-      ... | case1 eq with s≤fc (supf ux) f mf fcx 
-      ... | case1 eq1 = o≤-refl0 ( trans ( subst₂ (λ j k → j ≡ k ) &iso &iso (sym (cong (&) eq1))) (sym eq) )
-      ... | case2 lt1 = ?    --  ux << sx, sy << sx
-      zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-init fcy ⟫ | case2 lt1 = ? -- sy << sx
-      zc04 x<z y<z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ? 
-      zc04 x<z y<z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay , ch-is-sup uy uy≤z is-sup-y fcy ⟫ = ?
+      ... | case2 lt with trio< (supf x) (supf y1)
+      ... | tri< a ¬b ¬c = o<→≤ a
+      ... | tri≈ ¬a b ¬c = o≤-refl0 b
+      ... | tri> ¬a ¬b y1<z = ? where
+           zc05 : ( supf y1 ≡ supf ux ) ∨ (supf y1 << supf ux )
+           zc05 = ChainP.fcy<sup is-sup-x fcy1
+      zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-init fcy1 ⟫ | case2 lt1 = ? -- sy1 << sx
+      zc04 x<z y1≤z | ⟪ ax , ch-init fcx ⟫ | ⟪ ay1 , ch-is-sup uy1 uy1≤z is-sup-y1 fcy1 ⟫ = ? 
+      zc04 x<z y1≤z | ⟪ ax , ch-is-sup ux ux≤z is-sup-x fcx ⟫ | ⟪ ay1 , ch-is-sup uy1 uy1≤z is-sup-y1 fcy1 ⟫ = ?
       -- ... | tri< a ¬b ¬c = csupf (o<→≤ a)
       -- ... | tri≈ ¬a b ¬c = csupf (o≤-refl0 b)
-      -- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay supf x) k ) ? (csupf ? )
-      -- csy : odef (UnionCF A f mf ay supf y) (supf y) 
-      -- csy = csupf ?
+      -- ... | tri> ¬a ¬b c = subst (λ k → odef (UnionCF A f mf ay1 supf x) k ) ? (csupf ? )
+      -- csy1 : odef (UnionCF A f mf ay1 supf y1) (supf y1) 
+      -- csy1 = csupf ?
        
    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 sf<sb fc = zc04 where
@@ -496,12 +502,12 @@
               m05 = sym ( ZChain.sup=u zc ab (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 b<A fcz
+              m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ 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 ; supu=u = λ _ → ZChain.sup=u zc ab b<A {!!} } 
+              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) →
@@ -515,7 +521,7 @@
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-              m07 {z} fc = ZChain.fcy<sup zc m09 fc
+              m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
               m08 : {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
               m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
@@ -523,7 +529,7 @@
               m05 = sym (ZChain.sup=u zc ab 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 m09 {!!} }
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -642,7 +648,7 @@
                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} ; supu=u = λ lt → ⊥-elim ( o<¬≡ refl lt ) }
+               uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} ; supu=u = ? }
 
      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)    }
@@ -732,7 +738,7 @@
                          ... | 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
+                 ... | 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 = {!!}
@@ -797,13 +803,6 @@
           ... | tri≈ ¬a b ¬c = spu 
           ... | tri> ¬a ¬b c = spu
 
-          fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → (w ≡ supf1 u) ∨ (w << supf1 u)
-          fcy<sup {u} {w} u<x fc with trio< u x 
-          ... | tri< a ¬b ¬c = ZChain.fcy<sup uzc <-osuc fc where
-               uzc = pzc (osuc u) (ob<x lim a)
-          ... | tri≈ ¬a b ¬c = ⊥-elim (¬a u<x)
-          ... | tri> ¬a ¬b c = ⊥-elim (¬a u<x)
-
           pchain : HOD
           pchain = UnionCF A f mf ay supf1 x