# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657486249 -32400
# Node ID 38103b4e6780377044e4121973284f0c8bb0103e
# Parent  46d05d12df5789d96fc0f38a990535cb4510c1d4
...

diff -r 46d05d12df57 -r 38103b4e6780 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 11 05:18:41 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 05:50:49 2022 +0900
@@ -263,10 +263,9 @@
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) (sup z : Ordinal) : Set n where
    field
       asup    : odef A sup
-      y<sup   : y o< sup
-      y<<sup  : y << sup
+      fcy<sup  : {z : Ordinal } → FClosure A f y z → z << sup
       csupz   : odef (chainf sup) z
-      order : (sup1 z1 : Ordinal) → (lt : sup1 o< sup ) → odef (chainf sup1 ) z1 → z1 << z
+      order : {sup1 z1 : Ordinal} → (lt : sup1 o< sup ) → odef (chainf sup1 ) z1 → z1 << sup
 
 data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) : Ordinal →  Ordinal → Set n where
     ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay chainf y z 
@@ -315,14 +314,14 @@
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * xb
-          ct00 = {!!}
+          ct00 = ChainP.fcy<sup supb fca
           ct01 : * a < * b 
           ct01 with s≤fc xb f mf fcb 
           ... | case1 eq =  subst (λ k → * a < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * xa
-          ct00 = {!!}
+          ct00 = ChainP.fcy<sup supa fcb
           ct01 : * b < * a 
           ct01 with s≤fc xa f mf fca 
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
@@ -330,7 +329,7 @@
      ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-is-sup supb fcb) with trio< xa xb
      ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * xb
-          ct03 = {!!}
+          ct03 = ChainP.order supb a₁ (ChainP.csupz supa)
           ct02 : * a < * b 
           ct02 with s≤fc xb f mf fcb 
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
@@ -338,7 +337,7 @@
      ... | tri≈ ¬a  refl ¬c = fcn-cmp xa f mf fca fcb
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * xa
-          ct05 = {!!}
+          ct05 = ChainP.order supa c (ChainP.csupz supb)
           ct04 : * b < * a 
           ct04 with s≤fc xa f mf fca 
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
@@ -517,10 +516,14 @@
           pzc z z<x = prev z z<x
           UZ : HOD
           UZ = UnionCF A x pchainf
+          chainf0 : (z : Ordinal ) → HOD
+          chainf0 z with o≤? x z
+          ... | yes _  = UZ
+          ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
           total-UZ : IsTotalOrderSet UZ
           total-UZ {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 {!!} {!!} {!!}
+               uz01 = chain-total A f mf ay chainf0 {!!} {!!}
                    -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  (UChain.chain∋z (proj2 ca))) 
                    -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  (UChain.chain∋z (proj2 cb)))
           usup : SUP A UZ