# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656967407 -32400
# Node ID 7d227d624aad834f64759bd39d1ecc1023664f2e
# Parent  f403887019302ae62bda19b5c9b344097e6244e4
...

diff -r f40388701930 -r 7d227d624aad src/zorn.agda
--- a/src/zorn.agda	Tue Jul 05 05:10:27 2022 +0900
+++ b/src/zorn.agda	Tue Jul 05 05:43:27 2022 +0900
@@ -239,24 +239,27 @@
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
--- Union of supf z which o< x
---
-record UChain (x : Ordinal) (chain : (z : Ordinal ) → z o< x → HOD)  (z : Ordinal) : Set n where 
-   field
-      u : Ordinal
-      u<x : u o< x
-      chain∋z : odef (chain u u<x) z
-
 ∈∧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 ) (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
+    ch-noax : {x z p : Ordinal }  ( ax : ¬ odef A x ) → p o< x → ( prev : Chain A f mf ay p z ) →  Chain A f mf ay x z
+    ch-nosup : {x z p : Ordinal }  ( ax : odef A x ) 
+         → ( nosup : ¬ ( (x1 w : Ordinal) → x1 o< x → Chain A f mf ay x1 w → w << x ) ) → ( prev : Chain A f mf ay p z ) → Chain A f mf ay x z
+
+-- Union of supf z which o< x
+--
+record UChain (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (x : Ordinal)   (z : Ordinal) : Set n where 
+   field
+      u : Ordinal
+      u<x : u o< x
+      chain∋z : Chain A f mf ay u z
+
+UnionCF : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (x : Ordinal) (chainf : (z : Ordinal ) →  Chain A f mf ay z z ) → HOD
+UnionCF A f mf ay x chainf = record { od = record { def = λ z → odef A z ∧  UChain A f mf ay x z } ; 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) ( z : Ordinal )  : Set (Level.suc n) where
    chain : HOD
@@ -415,10 +418,8 @@
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
-          supf : Ordinal → HOD
-          supf x = ? -- ZChain.chain zc0 
           zc : ZChain A f mf ay (Oprev.oprev op) 
-          zc = ? -- prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
+          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
           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
           px<x : px o< x
@@ -447,7 +448,7 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!}
+                record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!} ; chainf = ?
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!}   } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
@@ -467,7 +468,7 @@
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
-                ... | tri< a ¬b ¬c = supf z
+                ... | tri< a ¬b ¬c = ?
                 ... | tri≈ ¬a b ¬c = schain 
                 ... | tri> ¬a ¬b c = schain
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
@@ -540,11 +541,6 @@
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
                 ... | tri≈ ¬a b ¬c = refl
                 ... | tri> ¬a ¬b c = refl
-                seq<x : {b : Ordinal } → b o< x →  supf b  ≡ supf0 b
-                seq<x {b} b<x with trio< b x
-                ... | tri< a ¬b ¬c = refl
-                ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
-                ... | tri> ¬a ¬b c  = ? -- ⊥-elim (¬a  b<x zc0 )
 
           ... | case2 ¬x=sup = ? where -- x is not f y' nor sup of former ZChain from y -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
@@ -564,7 +560,7 @@
           -- chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
           -- chainq z z<x = ZChain.chain-uniq (  prev z z<x )
           uzc : HOD
-          uzc = UnionCF A x ? 
+          uzc = UnionCF A f mf ay x ? 
           -- c-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → (w<x : w o< x ) → chainf z ? ⊆' chainf w w<x
           -- c-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
           -- ... | s | t = {!!}