# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657269749 -32400
# Node ID 79616ba278c0e4a73ed3b95cf757bddbeeb8895d
# Parent  6a8d13b02a508e5d38259077062931f63088e5c9
new chain

diff -r 6a8d13b02a50 -r 79616ba278c0 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 03 18:59:49 2022 +0900
+++ b/src/zorn.agda	Fri Jul 08 17:42:29 2022 +0900
@@ -253,45 +253,25 @@
 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 →  HOD  → Set (Level.suc n) where
-    ch-init    : Chain A f mf  ay o∅  record { od = record { def = λ z → FClosure A f y z  } ; odmax = & A ; <odmax = λ {y} sy → ? }
-    ch-noax    : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f mf  ay (Oprev.oprev op) chain) → Chain A f mf  ay x chain
-    ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) 
-        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( h :  HasPrev A chain ax f ) → Chain A f mf ay x chain
-    ch-is-sup : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
-        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( nh :  ¬ HasPrev A chain  ax f ) ( sup : IsSup A chain   ax ) → Chain A f mf ay x 
-            record { od = record { def = λ z → odef A z ∧ (odef chain z ∨ (FClosure A f x z)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-    ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
-        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f mf ay x chain
-    ch-noax-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( noax : ¬ odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         → Chain A f mf ay x (UnionCF A x chainf )
-    ch-hasprev-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         → ( h :   HasPrev A (UnionCF A x chainf)  ax f ) 
-         → Chain A f mf ay x (UnionCF A x chainf )
-    ch-is-sup-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         →  ( nh :  ¬ HasPrev A (UnionCF A x chainf) ax f ) ( sup : IsSup A (UnionCF A x chainf) ax ) 
-         → Chain A f mf ay x 
-             record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f x z ) } 
-                ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-    ch-skip-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
-         →  (nh : ¬ HasPrev A (UnionCF A x chainf) ax f ) (nsup :  ¬ IsSup A (UnionCF A x chainf) ax ) 
-         → Chain A f mf ay x (UnionCF A x chainf) 
-
-ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f mf ay (& A) chain → (x : Ordinal) → x o< & A →  HOD
-ChainF A f mf {y} ay chain Ch x x<a = {!!}
+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    : (x z : Ordinal) → x ≡ o∅ → FClosure A f y z  → Chain A f mf  ay x z 
+    ch-is-sup : {x z : Ordinal }  ( ax : odef A x ) 
+         → ( is-sup : (x1 w : Ordinal) → 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
 
 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
-      chain : HOD
-      chain-uniq : Chain A f mf ay z chain 
+      psup :  Ordinal
+      p≤z : psup o≤ z 
+      pchain : {px : Ordinal} → px o≤ z → (w : Ordinal) →  Chain A f mf ay px w
+      chain-mono : (px : Ordinal) → (x≤p : px o≤ psup ) → (w : Ordinal ) →  Chain A f mf ay px w → Chain A f mf ay psup w 
+
+ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) 
+     → (z : Ordinal) →  ZChain1 A f mf ay (& A) →  HOD
+ChainF A f mf {y} ay z zc = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup zc) x } ; odmax = & A ; <odmax =  λ {y} sy → ∈∧P→o< sy } 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  (zc0 :  ZChain1 A f mf ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = ZChain1.chain zc0
+   chain = ChainF A f mf ay z zc0
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -449,32 +429,32 @@
           sc = prev px px<x
           sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = record { chain = chain sc ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc )  } 
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc ) ax f )   
-          ... | case1 pr = record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) 
-                                       record { y = HasPrev.y pr  ; ay = HasPrev.ay pr  ; x=fy = sc6 } } where
+          ... | no noax = ?
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A ? ax f )   
+          ... | case1 pr = ? where -- record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) 
+                                       -- record { y = HasPrev.y pr  ; ay = HasPrev.ay pr  ; x=fy = sc6 } } where
                 sc6 : x ≡ f (HasPrev.y pr)
                 sc6 = subst (λ k → k ≡ f (HasPrev.y pr) ) &iso  ( HasPrev.x=fy pr  )
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc ) ax )
-          ... | case1 is-sup = record { chain = schain ; chain-uniq = sc9 } where
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A ? ax )
+          ... | case1 is-sup = ? where -- record { chain = schain ; chain-uniq = sc9 } where
                 schain : HOD
-                schain = record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
-                    ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
-                sc7 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
+                schain = ? -- record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } 
+                    -- ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+                sc7 : ¬ HasPrev A ? (subst (λ k → odef A k) &iso ax) f
                 sc7 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
-                sc9 : Chain A f mf ay x schain
-                sc9 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc7
-                    record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-sup lt) }
-          ... | case2 ¬x=sup = record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } where
-                sc17 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
+                -- sc9 : Chain A f mf ay x schain
+                -- sc9 = ? -- ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc7
+                    -- record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-sup lt) }
+          ... | case2 ¬x=sup = ? where --- record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } where
+                sc17 : ¬ HasPrev A ? (subst (λ k → odef A k) &iso ax) f
                 sc17 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
-                sc10 : ¬ IsSup A (chain sc) (subst (λ k → odef A k) &iso ax)
+                sc10 : ¬ IsSup A ? (subst (λ k → odef A k) &iso ax)
                 sc10 not = ¬x=sup ( record { x<sup  = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) }  )
      ... | no ¬ox = sc4 where
           chainf : (z : Ordinal) → z o< x → HOD
-          chainf z z<x = ZChain1.chain ( prev z z<x )
-          chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
-          chainq z z<x = ZChain1.chain-uniq ( prev z z<x)
+          chainf z z<x = ? -- Chain1.chain ( prev z z<x )
+          -- chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
+          -- chainq z z<x = ? -- ZChain1.chain-uniq ( prev z z<x)
           sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
           ... | no noax = record { chain = UnionCF A x chainf ; chain-uniq = ? } -- ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ?  } 
@@ -493,7 +473,7 @@
           --
           px = Oprev.oprev op
           supf : Ordinal → HOD
-          supf x = ZChain1.chain zc0 
+          supf x = ? -- ZChain1.chain zc0 
           zc : ZChain A f mf ay zc0 (Oprev.oprev op)
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
@@ -661,7 +641,7 @@
      ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!}
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          supf : Ordinal → HOD
-         supf x = ZChain1.chain zc0 
+         supf x = ? -- Z?Chain1.chain zc0 
          uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf ay zc0 (UChain.u u)
          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
          Uz : HOD
@@ -678,7 +658,7 @@
          u-chain∋init = {!!} -- case2 ( init ay )
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
-         ... | tri< a ¬b ¬c = ZChain1.chain zc0 
+         ... | tri< a ¬b ¬c = ? -- ZChain1.chain zc0 
          ... | tri≈ ¬a b ¬c = Uz 
          ... | tri> ¬a ¬b c = Uz
          u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
@@ -690,11 +670,6 @@
          ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
          ... | tri≈ ¬a b ¬c = refl
          ... | tri> ¬a ¬b c = refl
-         seq<x : {b : Ordinal } → (b<x : b o< x ) →  ZChain1.chain zc0  ≡ supf0 b
-         seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = {!!} -- cong (λ k → (ZChain1.chain zc0) o<-irr --  b<x ≡ a
-         ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
-         ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
          ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y
          ord≤< {x} {y} {z} x<z z≤y  with  osuc-≡< z≤y
          ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z