# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1661645752 -32400
# Node ID 1a5bb940fceb28ed9ace0af5c6a175abe62f7117
# Parent  8ceaf3455601c50f8c8051213234498eb4b653cd
...

diff -r 8ceaf3455601 -r 1a5bb940fceb src/zorn.agda
--- a/src/zorn.agda	Thu Aug 25 08:19:09 2022 +0900
+++ b/src/zorn.agda	Sun Aug 28 09:15:52 2022 +0900
@@ -746,8 +746,27 @@
           no-extension ¬sp=x = record { supf = supf1 ;  sup = ? ; supf-mono = {!!}
                ; initial = ? ; chain∋init = ? ; sup=u = ? ; supf-is-sup = ? ; csupf = {!!}
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = ? ;  f-total = ? }  where
-                 pchain0=1 : ?
-                 pchain0=1 = ?
+                 pchain0=1 : pchain ≡ pchain1
+                 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
+                     zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
+                     zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                     zc10 {z} ⟪ az , ch-is-sup u u≤px is-sup fc ⟫ = zc12 fc where
+                          zc12 : {z : Ordinal} →  FClosure A f (supf0 u) z → odef pchain1 z
+                          zc12 (fsuc x fc) with zc12 fc
+                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                          ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
+                          zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu  , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) ? (init ? ? ) ⟫ 
+                     zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
+                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                     zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where
+                          zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
+                          zc13 (fsuc x fc) with zc13 fc
+                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                          ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
+                          zc13 (init asu su=z ) with trio< u x
+                          ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (subst (λ k → u o< k) (sym (Oprev.oprev=x op))  a) ? (init ? ? ) ⟫ 
+                          ... | tri≈ ¬a b ¬c = ?
+                          ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c )
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf0 z)
                  sup {z} z≤x with trio< z px
                  ... | tri< a ¬b ¬c = SUP⊆ ? ( ZChain.sup zc (o<→≤   a) ) 
@@ -829,16 +848,16 @@
           ... | tri≈ ¬a b ¬c = ysp
           ... | tri> ¬a ¬b c = ysp
 
-          pchain0 : HOD
-          pchain0 = UnionCF A f mf ay supf0 x
+          pchain : HOD
+          pchain = UnionCF A f mf ay supf0 x
 
-          ptotal0 : IsTotalOrderSet pchain0
+          ptotal0 : IsTotalOrderSet pchain
           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
+          usup : SUP A pchain
+          usup = supP pchain (λ lt → proj1 lt) ptotal0
           spu = & (SUP.sup usup)
 
           supf1 : Ordinal → Ordinal
@@ -847,23 +866,23 @@
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
-          pchain : HOD
-          pchain = UnionCF A f mf ay supf1 x
+          pchain1 : HOD
+          pchain1 = UnionCF A f mf ay supf1 x
 
-          pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
+          pchain⊆A : {y : Ordinal} → odef pchain1 y →  odef A y
           pchain⊆A {y} ny = proj1 ny
-          pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
+          pnext : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a)
           pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫
           pnext {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) ⟫
-          pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
+          pinit :  {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
           ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= supf1 _
                zc7 = ChainP.fcy<sup is-sup (init ay refl)
-          pcy : odef pchain y
+          pcy : odef pchain1 y
           pcy = ⟪ ay , ch-init (init ay refl)    ⟫
-          ptotal : IsTotalOrderSet pchain
+          ptotal : IsTotalOrderSet pchain1
           ptotal {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)) 
@@ -884,23 +903,30 @@
                ; csupf = {!!} ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
-                 UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) 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⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf1 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
---                      UnionCF0⊆ {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) ⟫
+                 pchain0=1 : pchain ≡ pchain1
+                 pchain0=1 =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
+                     zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
+                     zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                     zc10 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc12 fc where
+                          zc12 : {z : Ordinal} →  FClosure A f (supf0 u) z → odef pchain1 z
+                          zc12 (fsuc x fc) with zc12 fc
+                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                          ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
+                          zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u u≤x ? (init ? ? ) ⟫ 
+                     zc11 :  {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z
+                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
+                     zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where
+                          zc13 : {z : Ordinal} →  FClosure A f (supf1 u) z → odef pchain z
+                          zc13 (fsuc x fc) with zc13 fc
+                          ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
+                          ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
+                          zc13 (init asu su=z ) with trio< u x
+                          ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u u≤x ? (init ? ? ) ⟫ 
+                          ... | tri≈ ¬a b ¬c = ?
+                          ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c )
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z≤x with trio< z x
-                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} )
+                 ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} )
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b c = {!!}
                  sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))