# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657666513 -32400
# Node ID 799963f352d64977cd59275bbf080e697d1c578c
# Parent  01a88eeb9d00acac9db4e291a36b3c486927428b
init chain

diff -r 01a88eeb9d00 -r 799963f352d6 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 12 23:05:31 2022 +0900
+++ b/src/zorn.agda	Wed Jul 13 07:55:13 2022 +0900
@@ -267,7 +267,7 @@
        (supf : Ordinal → Ordinal) (x : Ordinal)  (z : Ordinal) : Set n where 
    field
       u : Ordinal
-      u<x : u o< x
+      u<x : (u o< x ) ∨ ( x o≤ y )
       chain∋z : Chain A f mf ay supf u z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -472,6 +472,33 @@
      -- create all ZChains under o< x
      --
 
+     inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
+         → x o≤ y  → ZChain A f mf ay x
+     inititalChain f mf {y} ay x x≤y = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
+      ; initial = isy ; f-next = inext ; f-total = itotal ; is-max = ? } where
+          isupf : Ordinal → Ordinal
+          isupf z = y
+          cy : odef (UnionCF A f mf ay isupf x) y
+          cy = ⟪ ay , record { u = y ; u<x = case2 x≤y ; chain∋z = ch-init _ (init ay)  } ⟫
+          isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf x) z → * y ≤ * z
+          isy {z} ⟪ az , uz ⟫ with UChain.chain∋z uz 
+          ... | ch-init z fc = s≤fc y f mf fc 
+          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf x) a → odef (UnionCF A f mf ay isupf x) (f a)
+          inext {a} ua with UChain.chain∋z (proj2 ua)
+          ... | ch-init a fc = ⟪ proj2 (mf _ (proj1 ua))  , record { u = y ; u<x = case2 x≤y ; chain∋z = ch-init _ (fsuc _ fc ) } ⟫
+          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          itotal : IsTotalOrderSet (UnionCF A f mf ay isupf x) 
+          itotal {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 isupf (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+          imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf x) a →
+            b o< osuc x → (ab : odef A b) →
+            HasPrev A (UnionCF A f mf ay isupf x) ab f ∨ IsSup A (UnionCF A f mf ay isupf x) ab →
+            * a < * b → odef (UnionCF A f mf ay isupf x) b
+          imax {a} {b} ua b<ox ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf x) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
+          imax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
+
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
      ind f mf {y} ay x prev with trio< y x
@@ -518,7 +545,7 @@
                zc7 : y << psupf (UChain.u ua)
                zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  y ; u<x = y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , record { u =  y ; u<x = case1 y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
@@ -599,7 +626,7 @@
                zc7 : y << psupf0 (UChain.u ua)
                zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  y ; u<x = y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , record { u =  y ; u<x = case1 y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
 
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal