# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666150809 -32400
# Node ID babd8ac79a911e1fb4f73e3273188064a96aee0f
# Parent  a48dc906796cae6a45f58ac6b74bb4746c3bfb68
...

diff -r a48dc906796c -r babd8ac79a91 src/zorn.agda
--- a/src/zorn.agda	Wed Oct 19 09:10:27 2022 +0900
+++ b/src/zorn.agda	Wed Oct 19 12:40:09 2022 +0900
@@ -1303,23 +1303,33 @@
      data ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) 
             ( supf : Ordinal → Ordinal )  (z : Ordinal) : Set n where
           zchain : (uz : Ordinal ) → odef (UnionCF A f mf ay supf uz) z → ZChainP f mf ay supf z
+     
+     auzc :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
+            (supf : Ordinal → Ordinal )  → {x : Ordinal } → ZChainP f mf ay supf x → odef A x
+     auzc f mf {y} ay supf {x} (zchain uz ucf) = proj1 ucf
+
+     zc⊆uzc :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
+            (supf : Ordinal → Ordinal )  → {x z ux : Ordinal } → UChain A f mf ay supf ux x → supf x o< supf z  → ZChainP f mf ay supf x
+     zc⊆uzc f mf {y} ay supf {x} ( ch-init fc ) _ = zchain x ⟪ A∋fc y f mf fc ,  ch-init fc ⟫
+     zc⊆uzc f mf {y} ay supf {x} {z} ( ch-is-sup u1 u1<x u1-is-sup fc ) sx<sz 
+        = zchain z ⟪ A∋fc (supf u1) f mf fc ,  ch-is-sup u1 ? u1-is-sup fc ⟫
 
      UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
             (supf : Ordinal → Ordinal )  → HOD
      UnionZF f mf {y} ay supf = record { od = record { def = λ x → ZChainP f mf ay supf x } 
-         ; odmax = & A ; <odmax = λ lt →  ∈∧P→o< ? }
+         ; odmax = & A ; <odmax = λ lt →  ∈∧P→o< ⟪ auzc f mf ay supf lt , lift true ⟫ }
      
-     uztotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
+     uzctotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
          → ( supf : Ordinal → Ordinal )
          → IsTotalOrderSet (UnionZF f mf ay supf )
-     uztotal f mf ay sz {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+     uzctotal f mf ay sz {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 = ?
 
      usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          → ( supf : Ordinal → Ordinal )
          → SUP A (UnionZF f mf ay supf )
-     usp0 f mf {x} ay supf  = supP (UnionZF f mf ay supf ) (λ lt → ? ) (uztotal f mf ay supf )
+     usp0 f mf {x} ay supf  = supP (UnionZF f mf ay supf ) (λ lt → auzc f mf ay supf lt ) (uzctotal f mf ay supf )
 
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          → (zc : ZChain A f mf ay x )