# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660285010 -32400
# Node ID 2141154c521bec6920f9585ab9159047a5e2dff1
# Parent  473825abd7673604d906b3fdc147c74ef755f59d
...

diff -r 473825abd767 -r 2141154c521b src/zorn.agda
--- a/src/zorn.agda	Fri Aug 12 12:56:15 2022 +0900
+++ b/src/zorn.agda	Fri Aug 12 15:16:50 2022 +0900
@@ -688,6 +688,10 @@
           pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
           pnext1 {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 (mf a aa) , ch-init (fsuc _ fc)  ⟫
           pnext1 {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
+          ptotal1 : IsTotalOrderSet pchain1
+          ptotal1 {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 supf1 ( (proj2 ca)) ( (proj2 cb)) 
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
@@ -698,26 +702,40 @@
                ax : odef A x
                not-sup : IsSup A (UnionCF A f mf ay supf0 x) ax
 
+          UnionCF⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf0 u ⊆' UnionCF A f mf ay supf1 x 
+          UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
+          UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
+                  UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+          ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+          ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+          UnionCFR⊆ : {u x : Ordinal} → (a : u o≤ x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay supf0 x 
+          UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
+          UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
+                  UnionCFR⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+          ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+          ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
           no-extension : ¬ xSUP → ZChain A f mf ay x
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
-               ; initial = ? ; chain∋init = ? ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
-              ;  chain⊆A = λ lt → proj1 lt ;  f-next = ? ;  f-total = ? }  where
+               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf
+              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ? }  where
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z px
-                 ... | tri< a ¬b ¬c = ? -- ZChain.sup zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = ? -- ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ ?) ( ZChain.sup zc (o<→≤ a) )
+                 ... | tri≈ ¬a b ¬c = SUP⊆ (UnionCFR⊆ ?) ( ZChain.sup zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
                  ... | tri> ¬a ¬b c = ?
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
                  sup=u {b} ab b<x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ? -- ZChain.sup=u zc ab (o<→≤ a) is-sup
-                 ... | tri≈ ¬a b ¬c = ? --  ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) is-sup
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) ?
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (subst (λ k → k o≤ px) (sym b) o≤-refl ) ?
                  ... | tri> ¬a ¬b c = ?
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px 
-                 ... | tri< a ¬b ¬c = ? --  ZChain.csupf zc (o<→≤ a)
-                 ... | tri≈ ¬a b ¬c = ? --  ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl )
-                 ... | tri> ¬a ¬b px<b =  ? where
+                 ... | tri< a ¬b ¬c = UnionCF⊆ o≤-refl ( ZChain.csupf zc (o<→≤ a) )
+                 ... | tri≈ ¬a b ¬c = UnionCF⊆ o≤-refl ( ZChain.csupf zc (subst (λ k → k o≤ px) (sym b) o≤-refl ))
+                 ... | tri> ¬a ¬b px<b =  ⟪ ? , ch-is-sup b  o≤-refl ? ? ⟫  where
                      --   px< b ≤ x
                      -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1
                      zc30 : x ≡ b
@@ -740,7 +758,7 @@
              supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
              spx = & (SUP.sup supx )
              x=spx : x ≡ spx
-             x=spx = {!!}
+             x=spx = sym &iso
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf zc z