# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668928045 -32400
# Node ID 7c39cae23803a6def6f3d0c72f027e2075fa1a74
# Parent  47c0f8fa7b0c67c8ced1aac8e2b6ec427ca38b2a
...

diff -r 47c0f8fa7b0c -r 7c39cae23803 src/Ordinals.agda
--- a/src/Ordinals.agda	Sun Nov 20 09:29:56 2022 +0900
+++ b/src/Ordinals.agda	Sun Nov 20 16:07:25 2022 +0900
@@ -26,7 +26,7 @@
      <-osuc   : { x : ord  } → x o< osuc x
      osuc-≡<  : { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      Oprev-p  : ( x : ord  ) → Dec ( Oprev ord osuc x )
-     o<-irr   : { x y : ord } → ( lt lt1 : x o< y ) → lt ≡ lt1
+     o<-irr   : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1
      TransFinite : { ψ : ord  → Set (suc n) }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
diff -r 47c0f8fa7b0c -r 7c39cae23803 src/ordinal.agda
--- a/src/ordinal.agda	Sun Nov 20 09:29:56 2022 +0900
+++ b/src/ordinal.agda	Sun Nov 20 16:07:25 2022 +0900
@@ -200,12 +200,12 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
-OrdIrr : {n : Level } {x y : Ordinal {suc n} } (lt lt1 : x o< y) → lt ≡ lt1
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case1 x₁) = cong case1 (NP.<-irrelevant _ _ )
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case2 x₁) = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case2 x) (case1 x₁) = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
-OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} (case2 Φ<) (case2 Φ<) = refl
-OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} (case2 (s< x)) (case2 (s< x₁)) = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
+OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
+OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl
+OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
       lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
       lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl
       lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y )
diff -r 47c0f8fa7b0c -r 7c39cae23803 src/zorn.agda
--- a/src/zorn.agda	Sun Nov 20 09:29:56 2022 +0900
+++ b/src/zorn.agda	Sun Nov 20 16:07:25 2022 +0900
@@ -553,13 +553,49 @@
                     open o≤-Reasoning O
                     z53 : {z : Ordinal } →  odef (UnionCF A f mf ay (ZChain.supf zb) x) z →  odef (UnionCF A f mf ay (ZChain.supf za) x) z
                     z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
-                    z53 ⟪ as , ch-is-sup u u<x is-sup fc ⟫ =  ⟪ as , ch-is-sup u u<x ? ?  ⟫ 
+                    z53 {z} ⟪ as , ch-is-sup u u<x is-sup fc ⟫ =  ⟪ as , ch-is-sup u u<x z54 z55  ⟫ where
+                        ua=ub : supfa u ≡ supfb u
+                        ua=ub = prev u u<x (ordtrans u<x x≤xa )
+                        order :  {s z1 : Ordinal} → ZChain.supf za s o< ZChain.supf za u → FClosure A f (ZChain.supf za s) z1 →
+                            (z1 ≡ ZChain.supf za u) ∨ (z1 << ZChain.supf za u)
+                        order {s} {z1} lt fc = subst (λ k → z1 <= k) (sym ua=ub) 
+                             (ChainP.order is-sup (subst₂ ( λ j k → j o< k ) z56 ua=ub lt ) (subst (λ k → FClosure A f k z1 ) z56 fc )) where
+                             s<x : s o< x
+                             s<x = ordtrans (ZChain.supf-inject za lt) u<x
+                             z56 : supfa s ≡ supfb s
+                             z56 = prev s s<x (ordtrans s<x x≤xa)
+                        z54 : ChainP A f mf ay (ZChain.supf za) u  
+                        z54 = record { fcy<sup = λ {w} fc → subst (λ k → w <= k ) (sym ua=ub) (ChainP.fcy<sup is-sup fc )
+                          ; order = order
+                          ; supu=u = trans ua=ub (ChainP.supu=u is-sup) } 
+                        z55 : FClosure A f (ZChain.supf za u) z
+                        z55 = subst (λ k → FClosure A f k z ) (sym ua=ub) fc
            ... | tri> ¬a ¬b c = ⊥-elim ( o≤> (
                begin
                  supfa x  ≡⟨ sax=spa ⟩
-                 spa  ≤⟨ MinSUP.minsup ma (MinSUP.asm mb) (λ uza → MinSUP.x≤sup mb ?) ⟩
+                 spa  ≤⟨ MinSUP.minsup ma (MinSUP.asm mb) (λ uza → MinSUP.x≤sup mb (z53 uza)) ⟩
                  spb  ≡⟨ sym sbx=spb ⟩
-                 supfb x ∎ ) c ) where open o≤-Reasoning O
+                 supfb x ∎ ) c ) where 
+                    open o≤-Reasoning O
+                    z53 : {z : Ordinal } →  odef (UnionCF A f mf ay (ZChain.supf za) x) z →  odef (UnionCF A f mf ay (ZChain.supf zb) x) z
+                    z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 
+                    z53 {z} ⟪ as , ch-is-sup u u<x is-sup fc ⟫ =  ⟪ as , ch-is-sup u u<x z54 z55  ⟫ where
+                        ub=ua : supfb u ≡ supfa u
+                        ub=ua = sym ( prev u u<x (ordtrans u<x x≤xa ))
+                        order :  {s z1 : Ordinal} → ZChain.supf zb s o< ZChain.supf zb u → FClosure A f (ZChain.supf zb s) z1 →
+                            (z1 ≡ ZChain.supf zb u) ∨ (z1 << ZChain.supf zb u)
+                        order {s} {z1} lt fc = subst (λ k → z1 <= k) (sym ub=ua) 
+                             (ChainP.order is-sup (subst₂ ( λ j k → j o< k ) z56 ub=ua lt ) (subst (λ k → FClosure A f k z1 ) z56 fc )) where
+                             s<x : s o< x
+                             s<x = ordtrans (ZChain.supf-inject zb lt) u<x
+                             z56 : supfb s ≡ supfa s
+                             z56 = sym (prev s s<x (ordtrans s<x x≤xa))
+                        z54 : ChainP A f mf ay (ZChain.supf zb) u  
+                        z54 = record { fcy<sup = λ {w} fc → subst (λ k → w <= k ) (sym ub=ua) (ChainP.fcy<sup is-sup fc )
+                          ; order = order
+                          ; supu=u = trans ub=ua (ChainP.supu=u is-sup) } 
+                        z55 : FClosure A f (ZChain.supf zb u) z
+                        z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc
 
 UChain⊆ : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {z y : Ordinal} (ay : odef A y)  { supf supf1 : Ordinal → Ordinal }
@@ -1263,14 +1299,14 @@
 
      ... | no lim = zc5 where
 
-          pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
-          pzc z z<x = prev z z<x
+          pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
+          pzc {z} z<x = prev z z<x
 
           ysp =  MinSUP.sup (ysup f mf ay)
 
           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 = ZChain.supf (pzc  (ob<x lim a)) z
           ... | tri≈ ¬a b ¬c = ysp
           ... | tri> ¬a ¬b c = ysp
 
@@ -1288,23 +1324,53 @@
 
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z  
+          ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z  
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
           pchain1 : HOD
           pchain1 = UnionCF A f mf ay supf1 x
 
+          zeq : {xa xb z : Ordinal } 
+             → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 
+             → ZChain.supf (pzc  xa<x) z ≡  ZChain.supf (pzc  xb<x) z  
+          zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa =  spuf-unique A f mf ay xa≤xb  
+              (pzc xa<x)  (pzc xb<x)  z≤xa
+
+          sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc  (ob<x lim a)) z  
+          sf1=sf {z} z<x with trio< z x
+          ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
+          ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
+          ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x)
+
+          sf1=spu : {z : Ordinal } → (a : x o≤ z ) → supf1 z ≡ spu
+          sf1=spu {z} x≤z with trio< z x
+          ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a)
+          ... | tri≈ ¬a b ¬c = refl
+          ... | tri> ¬a ¬b c = refl
+
+          zc11 : {z : Ordinal } → (a : z o< x ) → odef pchain (ZChain.supf (pzc (ob<x lim a)) z)
+          zc11 {z} z<x = ⟪ ZChain.asupf (pzc (ob<x lim z<x)) , ch-is-sup (ZChain.supf (pzc (ob<x lim z<x)) z) 
+                  ? ? (init ? ?) ⟫           
+
           sfpx<=spu : {z : Ordinal } → supf1 z <= spu
-          sfpx<=spu {z} = ? -- MinSUP.x≤sup usup (case2 (init (ZChain.asupf zc {px}) refl ))
+          sfpx<=spu {z} with trio< z x
+          ... | tri< a ¬b ¬c = MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc  (ob<x lim a)) ) refl )
+          ... | tri≈ ¬a b ¬c = case1 refl
+          ... | tri> ¬a ¬b c = case1 refl
 
           sfpx≤spu : {z : Ordinal } → supf1 z o≤ spu
-          sfpx≤spu {z} = ? -- subst ( λ k → k o≤ spu) (sym (ZChain.supf-is-minsup zc o≤-refl ))  
-            -- ( MinSUP.minsup (ZChain.minsup zc o≤-refl) (MinSUP.asm supu)  
-            --  (λ {x} ux → MinSUP.x≤sup supu (case1 ux)) )
+          sfpx≤spu {z} with trio< z x
+          ... | tri< a ¬b ¬c = subst ( λ k → k o≤ spu) ?
+                    ( MinSUP.minsup (ZChain.minsup ? o≤-refl) ? (λ {x} ux → MinSUP.x≤sup ? ?) )
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ?
 
           supf-mono : {x y : Ordinal } → x o≤  y → supf1 x o≤ supf1 y
-          supf-mono {x} {y} x≤y = ?
+          supf-mono {x} {y} x≤y with trio< y x
+          ... | tri< a ¬b ¬c = ?
+          ... | tri≈ ¬a b ¬c = ?
+          ... | tri> ¬a ¬b c = ?
 
           zc5 : ZChain A f mf ay x
           zc5 with zc43 x spu