# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658774245 -32400
# Node ID 7679fef530738bab457a40d2a6a08e8089578b62
# Parent  798d8b8c36b161c6e70a6152b15208b2d3085f06
...

diff -r 798d8b8c36b1 -r 7679fef53073 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 26 00:09:11 2022 +0900
+++ b/src/zorn.agda	Tue Jul 26 03:37:25 2022 +0900
@@ -630,7 +630,7 @@
 
      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 = λ {z} → csupf {z} ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 )
+      ; csupf = λ {z} → csupf {z} ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 ) ; supf-mono = λ _ → o≤-refl
       ; 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
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
@@ -793,10 +793,18 @@
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
                 zc11 with zc12
                 ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup z 
-                     zc14 (subst (λ k → FClosure A f k (ZChain.supf ozc z)) (sym eq1) (init az))  ⟫  where
-                      zc14 :  ChainP A f mf ay psupf z (ZChain.supf ozc z)
-                      zc14 = ?
+                ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , z13 fc is-sup ⟫ where
+                   z13 : FClosure A f (ZChain.supf ozc u ) (ZChain.supf ozc z ) →  ChainP A f mf ay (ZChain.supf ozc) u (ZChain.supf ozc z )
+                       →  UChain A f mf ay psupf x (ZChain.supf ozc z )
+                   z13 fc is-sup = ?
+
+                -- ch-is-sup z 
+                --     zc14 (subst (λ k → FClosure A f k (ZChain.supf ozc z)) (sym eq1) (init az))  ⟫  where
+                --      zc14 :  ChainP A f mf ay psupf z (ZChain.supf ozc z)
+                --      zc14 = record { csupz = ? ; supfu=u = ? ; fcy<sup = ? ; order = ? } where
+                --          csupz : FClosure A f (psupf z) (ZChain.supf ozc z)
+                --          csupz = ?
+
           ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc15 
                   (subst (λ k → FClosure A f k spu) zc17  (init (SUP.A∋maximal usup)))  ⟫ where
                 zc15 : ChainP A f mf ay psupf x spu