# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655433721 -32400
# Node ID 5039d228838c7a441a70a7b7dda95f736689d6e6
# Parent  6655f03984f929046e01659582feb85a20f57cb1
...

diff -r 6655f03984f9 -r 5039d228838c src/zorn.agda
--- a/src/zorn.agda	Fri Jun 17 11:28:06 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 11:42:01 2022 +0900
@@ -570,8 +570,8 @@
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
-                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!}
-                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} }  where
+                   record { zc = record { chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!}
+                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} }}  where
                       -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0)   ab →
@@ -582,7 +582,7 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = {!!} where
+     ... | no ¬ox = record { zc = UnionZ ; supf = {!!} } where
        UnionZ : ZChain A y f {!!} x
        UnionZ = record { chain = Uz ; chain⊆A = {!!} ; f-total = {!!}  ; f-next = {!!} ; chain∋sup = {!!}
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
@@ -593,7 +593,9 @@
                chain∋z : odef (ZChain.chain (ZChain1.zc (prev u u<x {y} ay ))) z
          Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
          Uz⊆A {z} u = ZChain.chain⊆A (ZChain1.zc ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay )) (UZFChain.chain∋z u)
-         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f {!!} (UZFChain.u u)
+         uzc1 : {z : Ordinal} → (u : UZFChain z) → ZChain1 A y f (UZFChain.u u)
+         uzc1 {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) {y} ay
+         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (ZChain1.supf (uzc1 u)) (UZFChain.u u)
          uzc {z} u =  ZChain1.zc (prev (UZFChain.u u) (UZFChain.u<x u) {y} ay)
          Uz : HOD
          Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
@@ -604,23 +606,23 @@
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = {!!} ; chain∋z = ZChain.chain∋x (ZChain1.zc (prev y {!!} ay )) }
-         u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f {!!} a) (zb : ZChain A y f {!!} b) → ZChain.chain za  ⊆' ZChain.chain zb
-         u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain za) i → odef (chain zb) i } uind i zai where
+         u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain1 A y f a) (zb : ZChain1 A y f b) → ZChain.chain (ZChain1.zc za)  ⊆' ZChain.chain (ZChain1.zc zb)
+         u-mono a b b<x a≤b za zb {i} zai = TransFinite0 {λ i → odef (chain (ZChain1.zc za)) i → odef (chain (ZChain1.zc zb)) i } uind i zai where
             open ZChain
             uind :  (i : Ordinal)
-                 → ((j : Ordinal) → j o< i →  odef (chain za) j → odef (chain zb) j)
-                 → odef (chain za) i → odef (chain zb) i
+                 → ((j : Ordinal) → j o< i →  odef (chain (ZChain1.zc za)) j → odef (chain (ZChain1.zc zb)) j)
+                 → odef (chain (ZChain1.zc za)) i → odef (chain (ZChain1.zc zb)) i
             uind i previ zai = um01 where
-                um01 : odef (chain zb) i
+                um01 : odef (chain (ZChain1.zc zb)) i
                 um01 = {!!}
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
          ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)
-            (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+            (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc1 ux) (uzc1 uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
          ... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-            (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy))
+            (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy))
          ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-            (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
+            (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy)) 
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain1 A y f (& A)
      SZ f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain1 A y f z  } (ind f mf) (& A)