# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656835735 -32400
# Node ID 5f85e71b2490c17da04bc2abd7d03273804deb1b
# Parent  a45ec34b9fa761bff7a72788225e6a681be2404d
...

diff -r a45ec34b9fa7 -r 5f85e71b2490 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 03 14:20:22 2022 +0900
+++ b/src/zorn.agda	Sun Jul 03 17:08:55 2022 +0900
@@ -250,6 +250,9 @@
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
+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 ) {y : Ordinal} (ay : odef A y) : Ordinal →  HOD  → Set (Level.suc n) where
     ch-noax    : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f ay (Oprev.oprev op) chain) → Chain A f ay x chain
     ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) 
@@ -259,14 +262,26 @@
             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 ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f ay x chain
-    ch-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
+    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 ay z ( chainf z z<x ))
+         → Chain A f 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 ay z ( chainf z z<x ))
+         → ( h :   HasPrev A (UnionCF A x chainf)  ax f ) 
+         → Chain A f 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 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 ay x 
-             record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y z ) } 
+             record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y x ) } 
                 ; 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 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 ay x (UnionCF A x chainf) 
 
 ChainF : (A : HOD) →  ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f ay (& A) chain → (x : Ordinal) → x o< & A →  HOD
-ChainF A f {y} ay chain Ch x x<a = ?
+ChainF A f {y} ay chain Ch x x<a = {!!}
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -275,7 +290,7 @@
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init)  (zc0 :  ZChain1 A f ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = ?
+   chain = {!!}
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -440,28 +455,30 @@
                 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
-                -- A∋sc -- x is a sup of zc 
-                sup0 : SUP A (ZChain1.chain sc  )
-                sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → (ZChain1.chain sc ) ∋ y → (y ≡ * x) ∨ (y < * x)
-                        x21 {y} zy with IsSup.x<sup is-sup zy 
-                        ... | case1 y=x = case1 (subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x)  )
-                        ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x  )
-                sp : HOD
-                sp = SUP.sup sup0 
                 schain : HOD
-                schain = record { od = record { def = λ x → odef A x ∧ ( odef (ZChain1.chain sc ) x ∨ (FClosure A f (& sp) x)) } 
+                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 }
-                sc8 : Chain A f ay ? ?
-                sc8 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) ? ?  
+                sc7 : ¬ HasPrev A (chain sc) (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 ay x schain
-                sc9 = ?
-          ... | case2 ¬x=sup = {!!}
-     ... | no ¬ox = ? where
-          supf : (z : Ordinal) → z o< x → HOD
-          supf = ?
-          sc5 : HOD
-          sc5 = record { od = record { def = λ z → odef A z ∧ (UChain x supf z ∨ FClosure A f y z)} ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+                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
+                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 not = ¬x=sup ( record { x<sup  = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) }  )
+     ... | no ¬ox = {!!} where
+          chainf : (z : Ordinal) → z o< x → HOD
+          chainf z z<x = ZChain1.chain ( prev z z<x )
+          sc4 : ZChain1 A f 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) ?  } 
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )   
+          ... | case1 pr = record { chain = UnionCF A x chainf  ; chain-uniq = ? } -- ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? } 
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax )
+          ... | case1 is-sup = ?
+          ... | case2 ¬x=sup = ?
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 :  ZChain1 A f ay (& A)) 
          → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x
@@ -484,11 +501,11 @@
           --
           no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
-                            * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay ?  x
-          no-extenion is-max = record { chain⊆A = ? -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
+                            * a < * b → odef (ZChain.chain zc) b ) → ZChain A f ay {!!}  x
+          no-extenion is-max = record { chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
                      ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc)
                      ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc) 
-                     ; f-total = ? 
+                     ; f-total = {!!} 
                      ; chain∋init  = subst (λ k → odef k y ) {!!} (ZChain.chain∋init  zc) 
                      ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
                                  HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) {!!} is-max } where
@@ -637,24 +654,24 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = ?
+     ... | 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 
-         uzc : {z : Ordinal} → (u : UChain x ? z) → ZChain A f ay zc0 (UChain.u u)
+         uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f ay zc0 (UChain.u u)
          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
          Uz : HOD
-         Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z ? x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = ?  }
+         Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
          u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
-         u-next {z} = ?
+         u-next {z} = {!!}
          -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u)  }
          -- u-next {z} (case2 u) = case2 ( fsuc _ u )
          u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
-         u-initial {z} = ?
+         u-initial {z} = {!!}
          -- (case1 u) = ZChain.initial ( uzc u )  (UChain.chain∋z u)
          -- u-initial {z} (case2 u) = s≤fc _ f mf u
          u-chain∋init :  odef Uz y
-         u-chain∋init = ? -- case2 ( init ay )
+         u-chain∋init = {!!} -- case2 ( init ay )
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
          ... | tri< a ¬b ¬c = ZChain1.chain zc0 
@@ -662,7 +679,7 @@
          ... | tri> ¬a ¬b c = Uz
          u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
          u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
-         ... | s | t = ?
+         ... | s | t = {!!}
 
          seq : Uz ≡ supf0 x
          seq with trio< x x
@@ -671,7 +688,7 @@
          ... | 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 = {!!} -- 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