# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658129161 -32400
# Node ID 322dd65690725ec2e30baf545c5a91322a515b29
# Parent  b2e2cd12e38f32d89d10f17dcd578c3a8ab9c028
...

diff -r b2e2cd12e38f -r 322dd6569072 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 18 15:30:35 2022 +0900
+++ b/src/zorn.agda	Mon Jul 18 16:26:01 2022 +0900
@@ -300,9 +300,6 @@
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
-      is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< z  → (ab : odef A b) 
-          → HasPrev A chain ab f ∨  IsSup A chain ab  
-          → * a < * b  → odef chain b
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -310,14 +307,6 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
--- IsSup→Maximal : {A B : HOD} → {s : Ordinal } → ( B⊆A : B ⊆' A ) → ( bs : odef B s )→ IsSup A B (B⊆A bs) → Maximal A
--- IsSup→Maximal {A} {B} {s}  B⊆A bs is-sup 
---       = record { maximal = * s ; A∋maximal = subst (λ k → odef A k ) (sym &iso) (B⊆A bs) ;  ¬maximal<x = is00 } where
---    is00 : {z : HOD} → A ∋ z → ¬ (* s < z)
---    is00 = ?
-
--- data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
---
 -- data Chain is total
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
@@ -421,6 +410,15 @@
      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)
 
+     ZChain-is-max :( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+        {init : Ordinal} (ay : odef A init)   (zc : ZChain A f mf ay (& A)) → 
+         {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) a ) →  b o< & A  → (ab : odef A b) 
+          → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) (& A)) ab  
+          → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) (& A))) b
+     ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case1 has-prev) a<b = 
+          subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) (& A)) k ) (sym (HasPrev.x=fy has-prev)) ( ZChain.f-next zc (HasPrev.ay has-prev) )
+     ZChain-is-max A f mf {y} ay zc {a} {b} ca b<a ab (case2 is-sup) a<b = ?
+
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
@@ -433,7 +431,7 @@
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
               →  HasPrev A chain ab f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
-           z10 = ZChain.is-max zc
+           z10 = ZChain-is-max A f mf as0 zc
            z11 : & (SUP.sup sp1) o< & A
            z11 = c<→o< ( SUP.A∋maximal sp1)
            z12 : odef chain (& (SUP.sup sp1))
@@ -561,20 +559,9 @@
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          no-extension : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
-                    HasPrev A pchain ab f ∨  IsSup A pchain ab →
-                            * a < * b → odef pchain b ) → ZChain A f mf ay x
-          no-extension is-max  = record { initial = pinit ; chain∋init = pcy 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; is-max = is-max }
-
-          zcp : {a b : Ordinal} → odef pchain a 
-              → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op )
-              → b o< px → (ab : odef A b) 
-              → HasPrev A pchain ab f ∨  IsSup A pchain ab 
-              → * a < * b → odef pchain b
-          zcp {a} {b} za cheq b<x ab P a<b = subst (λ k → odef k b ) (sym cheq) ( 
-                   ZChain.is-max zc (subst (λ k → odef k a) cheq za) b<x ab 
-                       (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) cheq P)  a<b )
+          no-extension : ZChain A f mf ay x
+          no-extension = record { initial = pinit ; chain∋init = pcy 
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
           chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = zc11 ; uchain = UChain.uchain (proj2 za)  }  ⟫ where
@@ -601,83 +588,15 @@
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* px)
-          ... | no noapx = no-extension zc1 where -- ¬ A ∋ p, just skip
-                zc1 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
-                    HasPrev A pchain ab f ∨  IsSup A pchain ab →
-                            * a < * b → odef pchain b
-                zc1 {a} {b} za b<x ab P a<b with trio< b px
-                ... | tri< lt ¬b ¬c = zcp za (chain-≡ (chain-x zc14)) lt ab P a<b where
-                      zc14 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px
-                      zc14 {z} ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ upx 
-                          = ⊥-elim ( noapx ( subst (λ k → odef A k ) (trans upx (sym &iso) )  (ChainP.au is-sup ) ))
-                ... | tri≈ ¬a b=px ¬c = ⊥-elim ( noapx (subst (λ k → odef A k ) (trans b=px (sym &iso))  ab ) )
-                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
+          ... | no noapx = no-extension -- ¬ A ∋ p, just skip
           ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-                zc7 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
-                    HasPrev A pchain ab f ∨  IsSup A pchain ab →
-                            * a < * b → odef pchain b
-                zc7 {a} {b} za b<x ab P a<b with trio< b px
-                ... | tri< lt ¬b ¬c = zcp za (chain-≡ (chain-x zc14)) lt ab P a<b where
-                      zc14 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px
-                      zc14 {z} ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ upx 
-                        = ChainP.¬u=fx is-sup (subst (λ k → k ≡ _ ) (trans &iso (sym upx) )  (HasPrev.x=fy pr) )
-                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
-                ... | tri≈ ¬a b=px ¬c = zc15 where
-                       zc14 : f (HasPrev.y pr) ≡ b
-                       zc14 = begin f (HasPrev.y pr)  ≡⟨ sym (HasPrev.x=fy pr) ⟩ 
-                          & (* px)                   ≡⟨ &iso ⟩ 
-                          px                         ≡⟨ sym b=px ⟩ 
-                          b ∎ where open   ≡-Reasoning 
-                       zc15 : odef pchain b
-                       zc15 with  ZChain.f-next zc (HasPrev.ay pr) 
-                       ... | ⟪ az , record  { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫ 
-                           = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case2 refl 
-                              ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc)  } ⟫ 
-                       ... | ⟪ az , record  { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ 
-                           = ⟪ subst (λ k → odef A k ) zc14 az , record { u = u ; u<x = case1 (b<x→0<x b<x ) 
-                            ; uchain = ch-init _ (subst (λ k → FClosure A f y k ) zc14 fc) } ⟫ 
+          ... | case1 pr = no-extension -- 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 ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
-                     ; initial = pinit ; chain∋init  = pcy ; is-max = p-ismax } where
-                p-ismax :  {a b : Ordinal} → odef pchain  a →
-                    b o< x → (ab : odef A b) →
-                    ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
-                        * a < * b → odef pchain b
-                p-ismax {a} {b} za b<x ab P a<b with trio< b px
-                ... | tri< lt ¬b ¬c = zcp za (chain-≡ ? ) lt ab P a<b 
-                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
-                ... | tri≈ ¬a b=px ¬c with P
-                ... | case1 hasp = ?
-                ... | case2 sup  = ?
-          ... | case2 ¬x=sup =  no-extension z18 where -- px is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
-                            HasPrev A pchain ab f ∨ IsSup A pchain   ab →
-                            * a < * b → odef pchain b
-                z18 {a} {b} za b<x ab P a<b with P
-                ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
-                ... | case2 b=sup with trio< b px
-                ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op))  b<x  ⟫ )
-                ... | tri≈ ¬a b=px ¬c = ⊥-elim ( ¬x=sup record { 
-                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso)) 
-                          (IsSup.x<sup b=sup (chain-mono zy) )  } ) 
-                ... | tri< b<px ¬b ¬c = chain-mono (ZChain.is-max zc pa b<px ab (case2 record { x<sup = sup1 }) a<b) where
-                   -- if b=sup and ¬ Isup>b , then b is Maximal
-                   --   px o< sup (fc u) ∈ pchain contradicts b=sup ( x o< sup x )
-                   z19 : {z : Ordinal} (az : odef pchain z) → ¬ UChain.u (proj2 az) ≡ px
-                   z19 {z} za@record {proj1 =  az ; proj2 =  record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } } 
-                         with trio< (UChain.u (proj2 za))  px
-                   ... | tri> ¬a ¬b₁ c = ¬b₁
-                   ... | tri< a₁ ¬b₁ ¬c₁ = ¬b₁
-                   ... | tri≈ ¬a u=px ¬c₁ with IsSup.x<sup b=sup ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫
-                   ... | case1 z=b = ?
-                   ... | case2 z<b = ?
-                   pa : odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) a
-                   pa =  chain-x z19 za
-                   sup1 : {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op)) z → (z ≡ b) ∨ (z << b)
-                   sup1 {z} uz = IsSup.x<sup b=sup ( chain-mono uz  )
+                     ; initial = pinit ; chain∋init  = pcy } 
+          ... | case2 ¬x=sup =  no-extension -- px is not f y' nor sup of former ZChain from y -- no extention
      ... | no op = zc5 where
 
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
@@ -699,9 +618,6 @@
           ... | tri< a ¬b ¬c with o<-irr z<x a 
           ... | refl = refl
 
-          psupf-mono : {z x1 : Ordinal} → (z<x1 : z o< x1) → x1 o≤ x → psupf0 z ≡ ZChain.supf (pzc z z<x1) z
-          psupf-mono {z} z<x1 x1≤x =?
-
           ptotal : IsTotalOrderSet pchain
           ptotal {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) )
@@ -726,11 +642,9 @@
           pcy : odef pchain y
           pcy = ⟪ ay , record { u =  o∅ ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
-          no-extension : ( {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
-                    HasPrev A pchain ab f ∨  IsSup A pchain ab →
-                            * a < * b → odef pchain b ) → ZChain A f mf ay x
-          no-extension is-max  = record { initial = pinit ; chain∋init = pcy 
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; is-max = is-max }
+          no-extension : ZChain A f mf ay x
+          no-extension  = record { initial = pinit ; chain∋init = pcy 
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal
@@ -778,34 +692,15 @@
                    uzc00 : ChainP A f mf ay psupf0 u b
                    uzc00 = ?
 
-
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
-          ... | no noax = no-extension ? where -- ¬ A ∋ p, just skip
+          ... | no noax = no-extension where -- ¬ A ∋ p, just skip
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extension ? 
-                 -- subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
+          ... | case1 pr = no-extension  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 
-          ... | case2 ¬x=sup =  no-extension z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) →
-                            HasPrev A pchain ab f ∨ IsSup A pchain   ab →
-                            * a < * b → odef pchain b
-                z18 {a} {b} za b<x ab P a<b with P
-                ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
-                ... | case2 b=sup with za
-                ... | ⟪ aa , record { u = _ ; u<x = u<x ; uchain = ch-init .a fca } ⟫ = uzc-mono z30 where
-                    ob<x : osuc b o< x
-                    ob<x = ?
-                    z30 : odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b
-                    z30 = ZChain.is-max (pzc _ ob<x) ⟪ aa , record { u = _ ; u<x = case2 refl ; uchain = ch-init a fca } ⟫ <-osuc  ab (case1 ?) a<b 
-                ... | ⟪ aa , record { u = u ; u<x = case2 u=0 ; uchain = ch-is-sup is-sup fc } ⟫ = ?
-                ... | ⟪ aa , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = uzc-mono z30 where
-                    ob<x : osuc b o< x
-                    ob<x = ?
-                    z30 : odef (UnionCF A f mf ay (ZChain.supf (prev (osuc b) ob<x))(osuc b)) b
-                    z30 = ZChain.is-max (pzc _ ob<x) ⟪ aa , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup ? ? } ⟫ <-osuc  ab (case1 ?) a<b 
+          ... | 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)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay   z  } (λ x → ind f mf ay x   ) (& A)