# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1665973777 -32400
# Node ID 620c2f3440f5dc3e3152cdb6ee92a0226a5a2b94
# Parent  c0cf2b383064585ed833473580ae263ac4449107
...

diff -r c0cf2b383064 -r 620c2f3440f5 src/zorn.agda
--- a/src/zorn.agda	Mon Oct 17 10:32:31 2022 +0900
+++ b/src/zorn.agda	Mon Oct 17 11:29:37 2022 +0900
@@ -1316,7 +1316,15 @@
 
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  → SUP A (UnionZF f mf ay )
      -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay)
-     sp0 f mf {x} ay = ? -- 
+     sp0 f mf {x} ay = ? -- supP ? ? ?
+
+     sp00 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         (zc : ZChain A f mf ay x ) → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
+     sp00 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
+        ztotal : IsTotalOrderSet (ZChain.chain zc) 
+        ztotal {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 (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  
             → f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 ))