# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658739198 -32400
# Node ID bbf12d61143f21a7c7fe1fd83ad1c8231ca60e2d
# Parent  9aa0fc917100f66a46aa69c8b5d1883a60297228
< is wrong

diff -r 9aa0fc917100 -r bbf12d61143f src/zorn.agda
--- a/src/zorn.agda	Mon Jul 25 16:36:36 2022 +0900
+++ b/src/zorn.agda	Mon Jul 25 17:53:18 2022 +0900
@@ -269,7 +269,7 @@
 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
-    ch-is-sup  : (u : Ordinal) {z : Ordinal } (u≤x : u o≤ x ) ( is-sup : ChainP A f mf ay supf u z) 
+    ch-is-sup  : (u : Ordinal) {z : Ordinal }  ( is-sup : ChainP A f mf ay supf u z) 
         ( fc : FClosure A f (supf u) z ) → UChain A f mf ay supf x z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -319,21 +319,21 @@
 chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → UChain A f mf ay supf xa a → UChain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init fca) (ch-init fcb) = fcn-cmp y f mf fca fcb
-     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub ub<x supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+     ct-ind xa xb {a} {b} (ch-init fca) (ch-is-sup ub supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * (supf ub)
           ct00 = ChainP.fcy<sup supb fca
           ct01 : * a < * b 
           ct01 with s≤fc (supf ub) f mf fcb
           ... | case1 eq =  subst (λ k → * a < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-init fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-init fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * (supf ua)
           ct00 = ChainP.fcy<sup supa fcb
           ct01 : * b < * a 
           ct01 with s≤fc (supf ua) f mf fca
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< ua ub
      ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * (supf ub)
           ct03 = ChainP.order supb  a₁ (ChainP.csupz supa)
@@ -428,33 +428,27 @@
             odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ ua , ch-init fc  ⟫ = 
             ⟪ ua , ch-init fc  ⟫ 
-        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa ,  ch-is-sup ua u≤x is-sup fc  ⟫ = 
-            ⟪ uaa , ch-is-sup ua (OrdTrans u≤x a≤b) is-sup fc  ⟫ 
+        chain-mono2 x {a} {b} {c} a≤b b≤x ⟪ uaa ,  ch-is-sup ua is-sup fc  ⟫ = 
+            ⟪ uaa , ch-is-sup ua  is-sup fc  ⟫ 
         chain<ZA : {x : Ordinal } → UnionCF A f mf ay (ZChain.supf zc) x ⊆' UnionCF A f mf ay (ZChain.supf zc) (& A)
         chain<ZA {x} ux with proj2 ux
         ... | ch-init fc = ⟪ proj1 ux , ch-init fc ⟫
-        ... | ch-is-sup u pu≤x is-sup fc = ⟪ proj1 ux , ch-is-sup u (o<→≤ u≤x) is-sup fc ⟫ where
-            u<A : (& ( * ( ZChain.supf zc u)))  o< & A
-            u<A = c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fcs _ f mf fc) )
-            u≤x :  u o< & A
-            u≤x = subst (λ k → k o< & A ) (trans &iso (ChainP.supfu=u is-sup)) u<A
+        ... | ch-is-sup u is-sup fc = ⟪ proj1 ux , ch-is-sup u  is-sup fc ⟫ 
         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 → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
         ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
-        ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , 
+        ... | ⟪ ab0 , ch-is-sup u 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 (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
+                      (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
         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
            px = Oprev.oprev op
            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 
-           -- fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
-           -- fcy<sup {u} {w} u≤x fc = ?
            is-max :  {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 ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
@@ -472,9 +466,9 @@
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
                     m03 with proj2 ua
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-                    ... | ch-is-sup u u≤x is-sup-a fc with trio< u px
-                    ... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup-a fc ⟫ -- u o< osuc x
-                    ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup-a fc ⟫
+                    ... | ch-is-sup u is-sup-a fc with trio< u px
+                    ... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫ -- u o< osuc x
+                    ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫
                     ... | tri> ¬a ¬b c = ⊥-elim (<-irr u≤a (ptrans a<b b<u) ) where
                          --  a and b is a sup of chain, order forces minimulity of sup
                          su=u : ZChain.supf zc u ≡ u
@@ -493,7 +487,7 @@
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
+                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
                     b<A : b o< & A
                     b<A = z09 ab
                     m05 : b ≡ ZChain.supf zc b
@@ -529,7 +523,7 @@
                  m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 
                        ; supfu=u = sym m05 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc) m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
+                 m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -611,8 +605,12 @@
      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 ; csupf = ? ; fcy<sup = ? 
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
+          spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
-          isupf z =  & (SUP.sup (ysup f mf ay))
+          isupf z with trio< z spi
+          ... | tri< a ¬b ¬c = y
+          ... | tri≈ ¬a b ¬c = spi
+          ... | tri> ¬a ¬b c = spi
           sp = ysup f mf ay
           cy : odef (UnionCF A f mf ay isupf o∅) y
           cy = ⟪ ay , ch-init (init ay)  ⟫
@@ -621,24 +619,29 @@
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc)
+          ... | ch-is-sup u is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf ? )
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u u≤x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u u≤x (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫
+          ... | ch-is-sup u is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u (ChainP-next A f mf ay isupf is-sup) (fsuc _ fc) ⟫
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {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 isupf (proj2 ca) (proj2 cb)  
 
           csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z)
-          csupf {z} = ⟪ SUP.A∋maximal sp   , ch-is-sup o∅ o≤-refl uz02 (init ( SUP.A∋maximal sp))  ⟫ where
-               uz02 : ChainP A f mf ay isupf o∅ (isupf z)
-               uz02 = record { csupz = init (SUP.A∋maximal sp) ; supfu=u = ? ; fcy<sup = ? ; order = ? }
-               uz03 : {z : Ordinal} → FClosure A f y z → z << isupf o∅
-               uz03 = ? 
-               uz04 : {sup1 z1 : Ordinal} → sup1 o< o∅ → FClosure A f (isupf sup1) z1 → z1 << isupf o∅
-               uz04 = ?
+          csupf {z} with trio< z spi
+          ... | tri< a ¬b ¬c = ⟪ ay , ch-init (init ay ) ⟫ 
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ⟪ SUP.A∋maximal sp   , ch-is-sup spi ? ? ⟫ where
+               uz03 : {z : Ordinal} → FClosure A f y z → z << isupf spi
+               uz03 {z} fcz with SUP.x<sup sp (subst (λ k → FClosure A f y k) (sym &iso) fcz) 
+               ... | case2 lt = ? -- subst (λ k → * z < k ) (sym *iso) lt
+               ... | case1 eq = ? -- ⊥-elim (<-irr (case1 e)
+               uz04 : {sup1 z1 : Ordinal} → sup1 o< spi → FClosure A f (isupf sup1) z1 → z1 << isupf spi
+               uz04 {_} {z} _ fcz = ?
+               uz02 : ChainP A f mf ay isupf spi spi
+               uz02 = ? -- record { csupz = init (SUP.A∋maximal sp) ; supfu=u = refl ; fcy<sup = uz03 ; order = uz04 }
 
      --
      -- create all ZChains under o< x
@@ -669,11 +672,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc ) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
                zc7 : y << (ZChain.supf zc) u 
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
@@ -684,7 +687,7 @@
           csupf : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) (supf0 z)
           csupf {z} with ZChain.csupf zc {z}
           ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-          ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u (OrdTrans u<px (o<→≤ px<x)) is-sup fc ⟫ 
+          ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫ 
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
@@ -764,17 +767,17 @@
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
                 zc11 with zc12
                 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                ... | ⟪ az , ch-is-sup u u<z is-sup fc ⟫ = ⟪ az , ch-is-sup z (o<→≤ z<x)
+                ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup z 
                      zc14 (subst (λ k → FClosure A f k (ZChain.supf ozc z)) (sym eq1) (init az))  ⟫  where
                       zc14 :  ChainP A f mf ay psupf z (ZChain.supf ozc z)
                       zc14 = ?
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x <-osuc zc15 
+          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc15 
                   (subst (λ k → FClosure A f k spu) zc17  (init (SUP.A∋maximal usup)))  ⟫ where
                 zc15 : ChainP A f mf ay psupf x spu
                 zc15 = ?
                 zc17 : spu ≡ psupf x 
                 zc17 = subst (λ k → spu ≡ psupf k  ) b (sym eq1) 
-          ... | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x <-osuc zc16
+          ... | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc16
                   (subst (λ k → FClosure A f k spu) psupf=x (init (SUP.A∋maximal usup)))  ⟫ where
                 zc16 : ChainP A f mf ay psupf x spu
                 zc16 = ?
@@ -786,11 +789,11 @@
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
-          pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫
+          pnext {a} ⟪ aa , ch-is-sup u is-sup fc ⟫ = ⟪  proj2 ( mf a aa ) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
                zc7 : y << psupf _
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
@@ -806,9 +809,9 @@
                 * a < * b → odef (UnionCF A f mf ay supf x) b
           is-max-hp supf x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
           ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ 
-          ... | ⟪ ab0 , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ ab , 
+          ... | ⟪ ab0 , ch-is-sup u is-sup fc ⟫ = ⟪ ab , 
                      subst (λ k → UChain A f mf ay supf x k )
-                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u≤x (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
+                          (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u (ChainP-next A f mf ay _ is-sup) (fsuc _ fc))  ⟫ 
 
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?