# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1654710321 -32400
# Node ID 6e0789af0d63c61036356a3646b764ad1ba9abfb
# Parent  40090ce9232c9c192339a9ea2c80f7f0b38da74c
...

diff -r 40090ce9232c -r 6e0789af0d63 src/zorn.agda
--- a/src/zorn.agda	Wed Jun 08 08:47:52 2022 +0900
+++ b/src/zorn.agda	Thu Jun 09 02:45:21 2022 +0900
@@ -252,8 +252,8 @@
    field
       zchain : ZChain A x f z
       chainf :  (b : Ordinal) → HOD
-      chain-mono :  {a b : Ordinal} → a o< b → chainf a  ⊆' chainf b
-      chain=zchain : {b : Ordinal} → chainf z ≡ ZChain.chain zchain 
+      chain-mono :  {a b : Ordinal} → a o< b → b o< osuc z  → chainf a  ⊆' chainf b
+      chain=zchain : chainf z ≡ ZChain.chain zchain 
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -579,16 +579,25 @@
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
          u-total1 : {x y : HOD } → (ux : odef Uz (& x)) → (uy : odef Uz (& y))
-             → & x o< & y → odef (ZChain.chain (uzc ux)) (& x) → odef (ZChain.chain (uzc uy)) (& x)
-         u-total1 {x} {y} ux uy  x<y =  ZChain∧Chain.chain-mono {!!} x<y where
-             u00 : ZChain∧Chain A {!!} f {!!}
-             u00 = prevzc {!!} {!!} {!!}
-             u02 : HOD
-             u02 = ZChain∧Chain.chainf u00 {!!}
-             u01 : odef {!!} (& x) → odef {!!} (& y)
-             u01 = ZChain∧Chain.chain-mono u00 x<y 
+             → UZFChain.u ux o< UZFChain.u uy → odef (ZChain.chain (uzc ux)) (& x) → odef (ZChain.chain (uzc uy)) (& x)
+         u-total1 {x} {y1} ux uy  x<y =  u01 where
+             u0x : ZChain∧Chain A y f (UZFChain.u ux)
+             u0x = prevzc (UZFChain.u ux) (UZFChain.u<x ux) {y} ay
+             u0y : ZChain∧Chain A y f (UZFChain.u uy)
+             u0y = prevzc (UZFChain.u uy) (UZFChain.u<x uy) {y} ay
+             u03 : odef (ZChain∧Chain.chainf u0y (UZFChain.u ux)) (& x) → odef (ZChain∧Chain.chainf u0y (UZFChain.u uy)) (& x)
+             u03 = ZChain∧Chain.chain-mono u0y x<y {!!}
+             u02 : ZChain∧Chain.chainf u0x (UZFChain.u ux) ≡ ZChain.chain (ZChain∧Chain.zchain u0x)
+             u02 = ZChain∧Chain.chain=zchain u0x  
+             u04 : ZChain∧Chain.chainf u0y (UZFChain.u ux) ≡ ZChain.chain (ZChain∧Chain.zchain u0x)
+             u04 = {!!}
+             u01 : odef (ZChain.chain (uzc ux)) (& x) → odef (ZChain.chain (uzc uy)) (& x)
+             u01 = subst₂ (λ j k → odef j (& x) → odef k (& x))
+                u04
+                (ZChain∧Chain.chain=zchain u0y)
+                ( ZChain∧Chain.chain-mono u0y x<y {!!} )
          u-total : IsTotalOrderSet Uz
-         u-total {x} {y} ux uy with trio< (& x) (& y)
+         u-total {x} {y} ux uy with trio< (UZFChain.u ux) (UZFChain.u uy)
          ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-total1 ux uy a (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
          ... | tri≈ ¬a b ¬c =  tri≈ {!!} {!!} {!!}
          ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-total1 uy ux c (UZFChain.chain∋z uy))