# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670586839 -32400
# Node ID a281ad683577806b3a3f463aa309e80eb42a8eb9
# Parent  0b6cee971cba5f56bc72307bc395bacc276cbf3c
order connected

diff -r 0b6cee971cba -r a281ad683577 src/zorn.agda
--- a/src/zorn.agda	Fri Dec 09 11:38:13 2022 +0900
+++ b/src/zorn.agda	Fri Dec 09 20:53:59 2022 +0900
@@ -475,14 +475,30 @@
    ... | case2 lt = lt
    ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) 
 
-   supfeq : {a b : Ordinal } → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b 
-   supfeq = ?
+   supfeq : {a b : Ordinal } → a o≤ z →  b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b 
+   supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b)
+   ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
+             IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) 
+   ... | tri≈ ¬a b ¬c = b
+   ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
+             IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) 
 
-   unioneq : {a b : Ordinal } → z o≤ supf a → supf a o≤ supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b 
-   unioneq = ?
-
-   -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f supf (supf b)
-   --    the condition of cfcs is satisfied, this is obvious
+   union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b 
+   union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+          z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w
+          z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+          z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+              u<b : u o< b  
+              u<b = ordtrans u<a (supf-inject sa<sb )
+          z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w
+          z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+          z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+              u<a : u o< a 
+              u<a = supf-inject ( osucprev (begin
+                 osuc (supf u)  ≡⟨ cong osuc su=u ⟩
+                 osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+                 z  ≤⟨ z≤sa ⟩
+                 supf a ∎ )) where open o≤-Reasoning O
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -1184,6 +1200,31 @@
                         zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39) 
                            ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫  ))
 
+                 supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b 
+                 supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
+                 ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
+                         IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) 
+                 ... | tri≈ ¬a b ¬c = b
+                 ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
+                         IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) 
+
+                 union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b 
+                 union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+                      z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w
+                      z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+                      z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+                          u<b : u o< b  
+                          u<b = ordtrans u<a (supf-inject0 supf1-mono sa<sb )
+                      z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w
+                      z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ 
+                      z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+                          u<a : u o< a 
+                          u<a = supf-inject0 supf1-mono ( osucprev (begin
+                             osuc (supf1 u)  ≡⟨ cong osuc su=u ⟩
+                             osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+                             x  ≤⟨ z≤sa ⟩
+                             supf1 a ∎ )) where open o≤-Reasoning O
+
                  order : {a b : Ordinal} {w : Ordinal} →
                     b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
                  order {a} {b} {w} b≤x sa<sb fc = z20 where
@@ -1202,13 +1243,21 @@
                      ... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where 
                           z26 : odef ( UnionCF A f ay supf0 b ) w 
                           z26 with x<y∨y≤x (supf1 a) b
-                          ... | case2 b≤sa = ?
+                          ... | case2 b≤sa = ⊥-elim ( o<¬≡ ( supfeq1  ? ? ( union-max1 ? ? (subst (λ k → supf1 a o< k) ? sa<sb) )) 
+                               (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 ?)) ))) 
                           ... | case1 sa<b with cfcs a<b b≤x sa<b fc  
                           ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
                           ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? ? ⟫ 
                      ... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b
                      ... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc))) 
-                     ... | case2 b≤sa = ? -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
+                     ... | case2 b≤sa = ⊥-elim ( o<¬≡ ? sa<sb ) where -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
+                          b=x : b ≡ x
+                          b=x with trio< b x
+                          ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , zc-b<x _ a ⟫   ) -- px o< b o< x
+                          ... | tri≈ ¬a b ¬c = b
+                          ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b ≤ x
+                          z27 : supf1 a ≡ supf1 b
+                          z27 = supfeq1  ? ? ( union-max1 ? ? sa<sb ) 
 
      ... | no lim with trio< x o∅
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )