# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661235366 -32400
# Node ID 106492766e36cb851e46af80018d9a05aa915b0c
# Parent  6bf0899a6150a34a1ad67dfc831c99e34a51d036
...

diff -r 6bf0899a6150 -r 106492766e36 src/zorn.agda
--- a/src/zorn.agda	Tue Aug 23 11:25:55 2022 +0900
+++ b/src/zorn.agda	Tue Aug 23 15:16:06 2022 +0900
@@ -695,6 +695,19 @@
 
           supf0 = ZChain.supf zc
 
+          sup1 : SUP A (UnionCF A f mf ay supf0 px)
+          sup1 = supP pchain pchain⊆A ptotal
+          sp1 = & (SUP.sup sup1 )
+          supf1 : Ordinal → Ordinal
+          supf1 z with trio< z px
+          ... | tri< a ¬b ¬c = ZChain.supf zc z
+          ... | tri≈ ¬a b ¬c = sp1 
+          ... | tri> ¬a ¬b c = sp1 
+
+          pchain1 : HOD
+          pchain1  = UnionCF A f mf ay supf1 x
+
+
           -- if previous chain satisfies maximality, we caan reuse it
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
@@ -774,29 +787,39 @@
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
 
-          record Usupf : Set n where
-             field
-                umax : Ordinal → Ordinal
-                umax<x : {z : Ordinal } → umax z o< x
-             supf : Ordinal → Ordinal
-             supf z = ZChain.supf (pzc (osuc (umax z)) (ob<x lim umax<x )) z
-             field
-                supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 
+          ysp =  & (SUP.sup (ysup f mf ay))
 
-          initial-segment : {a b z : Ordinal } → (a<x : a o< x )   → (b<x : b o< x )   
-              →  a o≤ b 
-              →  ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z o≤  ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z
+          initial-segment : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x)  → a o< b  → z o≤ a 
+             → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.(umax z)) (ob<x lim b<x )) z
           initial-segment = ?
 
-          is01 : {a b : Ordinal } → (a<x : a o< x )   → (b<x : b o< x )   
-              →  a o≤ b 
-              UnionCF A f mf ay (ZChain.supf (pzc (osuc a) (ob<x lim a<x ))) x ⊆'
-              UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim b<x ))) x 
-          is01 = ?
+          initial-segment1 : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x)  → a o< b  → 
+             → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) x ≡ ZChain.(umax z)) (ob<x lim b<x )) x
+          initial-segment1 = ?
+
+          supf0 : Ordinal → Ordinal
+          supf0 z with trio< z x
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+          ... | tri≈ ¬a b ¬c = {!!}
+          ... | tri> ¬a ¬b c = {!!}
+
+          pchain0 : HOD
+          pchain0 = UnionCF A f mf ay supf0 x
+
+          ptotal0 : IsTotalOrderSet pchain0
+          ptotal0 {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 supf0 ( (proj2 ca)) ( (proj2 cb)) 
+
+          usup : SUP A pchain0
+          usup = supP pchain0 (λ lt → proj1 lt) ptotal0
+          spu = & (SUP.sup usup)
 
           supf1 : Ordinal → Ordinal
-          supf1 z = ?
-          -- ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+          supf1 z with trio< z x
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
+          ... | tri≈ ¬a b ¬c = {!!}
+          ... | tri> ¬a ¬b c = {!!}
 
           pchain : HOD
           pchain = UnionCF A f mf ay supf1 x