# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658643908 -32400
# Node ID 359f1577f947f0fee165d45eb464c3110bb8a75c
# Parent  60a2340e892db011d34d9b398d32d1950a808452
...

diff -r 60a2340e892d -r 359f1577f947 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 24 12:07:11 2022 +0900
+++ b/src/zorn.agda	Sun Jul 24 15:25:08 2022 +0900
@@ -564,21 +564,35 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
           c = & (SUP.sup sp1)
 
+     uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
+     uchain f mf {y} ay = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = 
+             λ {z} cz → subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (A∋fc y f mf cz ))) }
+
+     utotal : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 
+        → IsTotalOrderSet (uchain f mf ay)
+     utotal f mf {y} ay {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 = fcn-cmp y f mf ca cb
+
+     ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 
+       →  SUP A (uchain f mf ay)
+     ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
+
      inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
      inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy ; csupf = ? ; fcy<sup = ? 
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
           isupf : Ordinal → Ordinal
-          isupf z = ? ---  Sup of fc y, is in chain, and fcy<sup
+          isupf z =  & (SUP.sup (ysup f mf ay))
           cy : odef (UnionCF A f mf ay isupf o∅) y
           cy = ⟪ ay , ch-init (init ay)  ⟫
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ? )
           inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
           inext {a} ua with (proj2 ua)
           ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
+          ... | ch-is-sup u u≤x is-sup fc = ⊥-elim ( <-irr (case1 refl) ? )
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           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) )