# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1654719198 -32400
# Node ID b1e76b7991b0bd152f61ec0e7b0dfbb56302f778
# Parent  cc416fc0ef846bcda6fc64123730b6d6293013f4
give up

diff -r cc416fc0ef84 -r b1e76b7991b0 src/zorn.agda
--- a/src/zorn.agda	Thu Jun 09 03:16:59 2022 +0900
+++ b/src/zorn.agda	Thu Jun 09 05:13:18 2022 +0900
@@ -254,7 +254,6 @@
       chainf :  (b : Ordinal) → HOD
       zchain : ZChain A x f chainf z
       chain-mono :  {a b : Ordinal} → a o< b → b o< osuc z  → chainf a  ⊆' chainf b
-      chain=zchain : chainf z ≡ ZChain.chain zchain 
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -397,7 +396,7 @@
           → ((z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChain∧Chain A y f z) →
             {y : Ordinal} → odef A y → ZChain∧Chain A y f x
      ind f mf x prevzc {y} ay with Oprev-p x
-     ... | yes op = record { zchain = zc4 ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } where
+     ... | yes op = record { zchain = zc4 ; chainf = chainf ; chain-mono = {!!} } where
           --
           -- we have previous ordinal to use induction
           --
@@ -411,7 +410,16 @@
           zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
-          zc4 : ZChain A y f {!!} x 
+          chainf : Ordinal → HOD 
+          chainf z with ODC.∋-p O A (* x)
+          ... | no noax =  {!!}
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf supO x
+          ... | case1 pr = {!!}
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
+          ... | case1 is-sup = {!!} -- x is a sup of zc0 
+          ... | case2 ¬x=sup = {!!}  -- x is not f y' nor sup of former ZChain from y
+
+          zc4 : ZChain A y f chainf x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
                  record {  chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
@@ -432,9 +440,9 @@
                 zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
                 ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
-                zc9 :  ZChain A y f {!!} x
-                zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
-                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!}   }
+                zc9 :  ZChain A y f chainf x
+                zc9 = {!!} -- record {  chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!} -- no extention
+                     -- ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!}   }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
                 record { chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext 
@@ -538,7 +546,7 @@
                      ... | case1 y=b  = subst (λ k → odef chain k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
-                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
+                   record {  chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} }  where
                       -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -554,14 +562,14 @@
      ... | tri< a ¬b ¬c = record { zchain = 
             record { chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!}
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }
-            ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} }
+            ; chainf = {!!} ; chain-mono = {!!} }
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b y<x = record { zchain = UnionZ 
-            ; chainf = {!!} ; chain-mono = {!!} ; chain=zchain = {!!} } where
+            ; chainf = {!!} ; chain-mono = {!!} } where
        prev : (z : Ordinal) → (z<x : z o< x )→ {y : Ordinal} → (ay : odef A y) → ZChain A y f (ZChain∧Chain.chainf (prevzc z z<x ay))  z
        prev z z<x ay = ZChain∧Chain.zchain (prevzc z z<x ay)
        UnionZ : ZChain A y f {!!} x
-       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
+       UnionZ = record { chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
                      ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
@@ -590,15 +598,10 @@
              u0y = prevzc (UZFChain.u uy) (UZFChain.u<x uy) {y} ay
              u03 : odef (ZChain∧Chain.chainf u0y (UZFChain.u ux)) (& x) → odef (ZChain∧Chain.chainf u0y (UZFChain.u uy)) (& x)
              u03 = ZChain∧Chain.chain-mono u0y x<y {!!}
-             u02 : ZChain∧Chain.chainf u0x (UZFChain.u ux) ≡ ZChain.chain (ZChain∧Chain.zchain u0x)
-             u02 = ZChain∧Chain.chain=zchain u0x  
              u04 : ZChain∧Chain.chainf u0y (UZFChain.u ux) ≡ ZChain.chain (ZChain∧Chain.zchain u0x)
              u04 = {!!}
              u01 : odef (ZChain.chain (uzc ux)) (& x) → odef (ZChain.chain (uzc uy)) (& x)
-             u01 = subst₂ (λ j k → odef j (& x) → odef k (& x))
-                u04
-                (ZChain∧Chain.chain=zchain u0y)
-                ( ZChain∧Chain.chain-mono u0y x<y {!!} )
+             u01 =  {!!} -- ZChain∧Chain.chain-mono u0y x<y {!!} 
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy with trio< (UZFChain.u ux) (UZFChain.u uy)
          ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-total1 ux uy a (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)