# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650794371 -32400
# Node ID 920a5c0568c3b784afbc50d2bc04a91c1921c6bc
# Parent  adbac273d2a65be0a46780a805353c9c31b8e471
...

diff -r adbac273d2a6 -r 920a5c0568c3 src/zorn.agda
--- a/src/zorn.agda	Sun Apr 24 16:33:21 2022 +0900
+++ b/src/zorn.agda	Sun Apr 24 18:59:31 2022 +0900
@@ -301,6 +301,11 @@
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc 
           c = & (SUP.sup sp1)
+     -- Union of ZFChain
+     UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) 
+            → ( (y : Ordinal) → y o< B → ZChain A sa f mf supO y ) → HOD
+     UZFChain f mf B prev = record { od = record { def = λ y → odef A y ∧ (y o< B)  ∧ ( (y<b : y o< B) → odef (ZChain.chain (prev y y<b)) y) }
+         ; odmax = & A ; <odmax = z07 }
      -- ZChain is not compatible with the SUP condition
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa f mf supO y )
          →  ZChain A sa f mf supO x 
@@ -323,12 +328,30 @@
           --   x has no y which y < x 
           zc4 : ZChain A sa f mf supO x
           zc4 with ODC.p∨¬p O ( Prev< A ax f )
-          ... | case1 y = record { chain = zc5 ; chain⊆A = record { incl = λ lt → proj1 lt  }
-                    ; f-total = {!!} ; f-next = {!!} ; chain∋x  = ⟪ subst (λ k → odef A (& k)) *iso sa , case1 (ZChain.chain∋x zc0)  ⟫ ; is-max = {!!} } where
-                zc5 : HOD
-                zc5 = record { od = record { def = λ z → odef A z ∧ (odef (ZChain.chain zc0) z ∨ (z ≡ x) ∨ (z ≡ f x)) } ; odmax = & A ; <odmax = z07 }
-          ... | case2 not = {!!}
-          --  zc4 = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; chain∋x  = {!!} ; is-max = {!!} }
+          ... | case1 y = zc7 where
+                zc7 :  ZChain A sa f mf supO x
+                zc7 with ODC.∋-p O  (ZChain.chain zc0) (* ( f x ) )
+                ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 
+                     ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
+                ... | no not = record { chain = zc5 ; chain⊆A =  ⊆-zc5
+                    ; f-total = zc6 ; f-next = {!!} ; chain∋x  = ⟪ subst (λ k → odef A (& k)) *iso sa , case1 (ZChain.chain∋x zc0)  ⟫ ; is-max = {!!} } where
+                --   extend with f x
+                    zc5 : HOD
+                    zc5 = record { od = record { def = λ z → odef A z ∧ (odef (ZChain.chain zc0) z ∨ (z ≡ f x)) } ; odmax = & A ; <odmax = z07 }
+                    ⊆-zc5 : zc5 ⊆ A 
+                    ⊆-zc5 = record { incl = λ lt → proj1 lt  }
+                    IPO = ⊆-IsPartialOrderSet  ⊆-zc5 PO
+                    fx>zc : ( z : Ordinal ) → (odef (ZChain.chain zc0) z → * z < * ( f x )
+                    fx>zc = ?
+                    cmp : Trichotomous _ _ 
+                    cmp record { elm = a ; is-elm = aa } record { elm = b ; is-elm = ab } = ?
+                    zc6 : IsTotalOrderSet zc5
+                    zc6 =  record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}
+                        ; compare = cmp }
+          ... | case2 not with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) ))
+          ... | case1 y = {!!}
+          ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 
+                     ; chain∋x  = {!!} ; is-max = {!!} }  -- no extention
      ind f mf x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
               ; chain∋x  = {!!}  ; is-max = {!!} } where