# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657482825 -32400
# Node ID 33f90b48321170dc9428192d3bcba76b181ea638
# Parent  34650e39e553c92b24ac4cb20270be325e0b71f4
Chain with chainf

diff -r 34650e39e553 -r 33f90b483211 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 10 18:30:02 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 04:53:45 2022 +0900
@@ -253,23 +253,39 @@
 UnionCF : (A : HOD) (x : Ordinal) (chainf : (z : Ordinal ) → z o< x → HOD ) → HOD
 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
-data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  Ordinal → Set n where
-    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay y z 
-    ch-is-sup : {x z : Ordinal } (init<x : y << x) (lty : y o< x ) ( ax : odef A x ) 
-         → ( is-sup : (x1 w : Ordinal) →  ( x1 ≡ y ) ∨ ( (y << x1) ∧ (x1 o< x) )  → Chain A f mf ay x1 w → w << x )  
-         → ( fc : FClosure A f x z ) → Chain A f mf ay x z
+--
+--  sup and its fclosure is in a chain HOD
+--    chain HOD is sorted by sup as Ordinal and <-ordered
+--    whole chain is a union of separated Chain
+--    minimum index is y not ϕ 
+--
+
+record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD) (sup z : Ordinal) : Set n where
+   field
+      asup    : odef A sup
+      y<sup   : y o< sup
+      y<<sup  : y << sup
+      sup<x   : sup o< x
+      csupz   : odef (chainf sup sup<x) z
+      order : (sup1 z1 : Ordinal) → (lt : sup1 o< sup ) → odef (chainf sup1 (ordtrans lt sup<x ) ) z1 → z1 << z
+
+data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD) : Ordinal →  Ordinal → Set n where
+    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay chainf y z 
+    ch-is-sup : {sup z : Ordinal } 
+         → ( is-sup : ChainP A f mf ay chainf sup z)
+         → ( fc : FClosure A f sup z ) → Chain A f mf ay chainf sup z
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       psup :  Ordinal → Ordinal 
       p≤z : (x : Ordinal ) →   odef A (psup x)
-      chainf : (x : Ordinal) → HOD
-      is-chain : (x w : Ordinal) → odef (chainf x) w → Chain A f mf ay (psup x) w 
+      chainf : (x : Ordinal) → x o< z  → HOD
+      is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x x<z) w → Chain A f mf ay chainf (psup x) w 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x )  
+   chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x ? )  
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -293,29 +309,29 @@
 --
 -- data Chain is total
 
-chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) 
-   {s s1 a b : Ordinal } ( ca : Chain A f mf ay s a ) ( cb : Chain A f mf ay s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {y} ay {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
-     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay xa a → Chain A f mf ay xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
+chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD)
+   {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
+chain-total A f mf {x} {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
+     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
-     ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup y<xb ltyb axb supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+     ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * xb
-          ct00 = supb _ _ (case1 refl) (ch-init a fca)  
+          ct00 = ?
           ct01 : * a < * b 
           ct01 with s≤fc xb 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 y<x ltya ax supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
+     ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * xa
-          ct00 = supa _ _ (case1 refl) (ch-init b fcb)  
+          ct00 = ?
           ct01 : * b < * a 
           ct01 with s≤fc xa 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 y<xa ltya axa supa fca) (ch-is-sup y<xb ltyb axb supb fcb) with trio< xa xb
+     ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-is-sup supb fcb) with trio< xa xb
      ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * xb
-          ct03 = supb _ _ (case2 ⟪ y<xa , a₁ ⟫) (ch-is-sup y<xa ltya axa supa fca)
+          ct03 = ?
           ct02 : * a < * b 
           ct02 with s≤fc xb f mf fcb 
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
@@ -323,7 +339,7 @@
      ... | tri≈ ¬a  refl ¬c = fcn-cmp xa f mf fca fcb
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * xa
-          ct05 = supa _ _ (case2 ⟪ y<xb , c ⟫) (ch-is-sup y<xb ltyb axb supb fcb)
+          ct05 = ?
           ct04 : * b < * a 
           ct04 with s≤fc xa f mf fca 
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
@@ -466,7 +482,7 @@
           sc : ZChain1 A f mf ay px
           sc = prev px px<x
           pchain : HOD
-          pchain  = chainf sc px
+          pchain  = chainf sc px ?
 
           no-ext :  ZChain1 A f mf ay x
           no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 }  where
@@ -478,10 +494,10 @@
             p≤z1 z with o≤? z x
             ... | yes _  = ZChain1.p≤z sc z
             ... | no _  = ZChain1.p≤z sc x
-            chainf1 : (z : Ordinal ) → HOD
-            chainf1 z with o≤? z x
-            ... | yes _  = ZChain1.chainf sc z
-            ... | no _ = ZChain1.chainf sc x
+            chainf1 : (z : Ordinal ) → z o< x → HOD
+            chainf1 z z<x with o≤? z x
+            ... | yes _  = ZChain1.chainf sc z ?
+            ... | no _ = ZChain1.chainf sc x ?
             is-chain1 : {!!}
             is-chain1 = {!!}
           sc4 : ZChain1 A f mf ay x
@@ -497,7 +513,7 @@
           ... | case2 ¬x=sup = no-ext
      ... | no ¬ox = sc4 where
           pchainf : (z : Ordinal) → z o< x → HOD
-          pchainf z z<x = ZChain1.chainf (prev z z<x) z
+          pchainf z z<x = ZChain1.chainf (prev z z<x) z ? 
           pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
           pzc z z<x = prev z z<x
           UZ : HOD
@@ -505,8 +521,9 @@
           total-UZ : IsTotalOrderSet UZ
           total-UZ {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 (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  (UChain.chain∋z (proj2 ca))) 
-                                            (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  (UChain.chain∋z (proj2 cb)))
+               uz01 = chain-total A f mf ay pchainf
+                   (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  ? (UChain.chain∋z (proj2 ca))) 
+                   (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  ? (UChain.chain∋z (proj2 cb)))
           usup : SUP A UZ
           usup = supP UZ (λ lt → proj1 lt) total-UZ 
           spu = & (SUP.sup usup)
@@ -527,7 +544,7 @@
             is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay (psup1 z ) w
             is-chain1 z w lt with o≤? x z
             ... | no z<x = ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w lt
-            is-chain1 z w ⟪ ax , ux ⟫ | yes _ = ch-is-sup y<spu lty aspu {!!} ux where
+            is-chain1 z w ⟪ ax , ux ⟫ | yes _ = ch-is-sup {!!} ux where
                 y<spu : y << spu
                 y<spu = {!!}
                 lty : y o< spu