# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1670838931 -32400
# Node ID 77740070e0088414d3a04005e5ffd96c13fbaae3
# Parent  091e7a80bfe3acb795aeb6c727891e7f3759f5c3
...

diff -r 091e7a80bfe3 -r 77740070e008 src/zorn.agda
--- a/src/zorn.agda	Mon Dec 12 07:24:45 2022 +0900
+++ b/src/zorn.agda	Mon Dec 12 18:55:31 2022 +0900
@@ -1284,12 +1284,6 @@
           pic<x {z} (ic-init fc) = ob<x lim 0<x   -- 0<x ∧ lim x → osuc o∅ o< x
           pic<x {z} (ic-isup ia ia<x sa<x fca) = ob<x lim ia<x 
 
-          ifc≤ : {za zb : Ordinal } ( ia : IChain ay supfz za ) ( ib : IChain ay supfz zb ) → (ia≤ib : IChain-i ia o≤ IChain-i ib )
-              → FClosure A f (ZChain.supf (pzc (ob<x lim (pic<x ib))) (IChain-i ia)) za
-          ifc≤ {za} {zb} (ic-isup ia ia<x sa<x fca) (ic-isup ib ib<x sb<x fcb)  ia≤ib 
-              = subst (λ k → FClosure A f k _ ) (zeq _ _ ? (o<→≤ <-osuc) ) fca
-          ifc≤ {za} {zb} ia ib ia≤ib = ?
-
           pchainx⊆chain : {z : Ordinal } → (pz : odef pchainx z) → odef (ZChain.chain (pzc (pic<x (proj2 pz)))) z
           pchainx⊆chain {z} ⟪ aw , ic-init fc ⟫ = ⟪ aw , ch-init fc ⟫
           pchainx⊆chain {z} ⟪ aw , (ic-isup ia ia<x sa<x fca) ⟫ = ZChain.cfcs (pzc (ob<x lim ia<x) ) <-osuc o≤-refl uz03 fca where
@@ -1300,27 +1294,50 @@
 
           chain⊆pchainx : {z w : Ordinal } → (oz<x : osuc z o< x) → odef (ZChain.chain (pzc oz<x)) w → odef pchainx w 
           chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
-          chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = ⟪ aw , ic-isup u ? ? (subst (λ  k → FClosure A f k w ) ? fc )  ⟫ where
-                 z<x : z o< x
-                 z<x = ordtrans <-osuc oz<x
+          chain⊆pchainx {z} {w} oz<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫ 
+             = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ  k → FClosure A f k w ) su=su fc) ⟫ where
+                 u<x : u o< x
+                 u<x = ordtrans u<oz oz<x
+                 su=su : ZChain.supf (pzc oz<x) u ≡ supfz u<x
+                 su=su = sym ( zeq _ _  (osucc u<oz) (o<→≤ <-osuc) )
+                 su≡u :  supfz u<x ≡ u
+                 su≡u = begin 
+                    ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩
+                    ZChain.supf (pzc oz<x) u  ≡⟨ su=u ⟩
+                    u ∎ where open ≡-Reasoning 
+
+          ichain-inject : {a b : Ordinal } {ia : IChain ay supfz a } {ib : IChain ay supfz b }
+            → ZChain.supf (pzc (pic<x ia)) (IChain-i ia) o< ZChain.supf (pzc (pic<x ib)) (IChain-i ib)
+            → IChain-i ia o< IChain-i ib
+          ichain-inject {a} {b} {ia} {ib} sa<sb = osucprev ( begin
+                    osuc (IChain-i ia)  ≤⟨ osucc ( ZChain.supf-inject (pzc (pic<x ib)) (osucprev ( begin 
+                        osuc (ZChain.supf (pzc (pic<x ib)) (IChain-i ia))  ≡⟨ cong osuc ( zeq _ _ ? ?)  ⟩ 
+                        osuc (ZChain.supf (pzc (pic<x ia)) (IChain-i ia))  ≤⟨ osucc sa<sb ⟩ 
+                        ZChain.supf (pzc (pic<x ib)) (IChain-i ib)  ∎ ))) ⟩
+                    IChain-i ib ∎ ) where open o≤-Reasoning O
 
           ptotalx : IsTotalOrderSet pchainx
-          ptotalx {a} {b} ⟪ _ , ia ⟫ ⟪ _ , ib ⟫ = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 with trio< (supfz (pic<x ia))  (supfz (pic<x ib))
-               ... | tri< ia<ib ¬b ¬c with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (pic<x ib))) ? ? (ifc≤ ia ib (o<→≤ ?))) (s≤fc _ f mf ?)
-               ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-                   ct00 : * (& a) ≡ * (& b)
-                   ct00 = cong (*) eq1
-               ... | case2 lt = tri< lt  (λ eq → <-irr (case1 (sym eq)) lt) (λ lt1 → <-irr (case2 lt) lt1)
-               uz01 | tri≈ ¬a ia=ib ¬c = fcn-cmp _ f mf ? (subst (λ k → FClosure A f k (& b)) (sym ia=ib) ?)
-               uz01 | tri> ¬a ¬b ib<ia  with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (pic<x ia))) ? ? (ifc≤ ib ia (o<→≤ ?))) (s≤fc _ f mf ?)
-               ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
-                   ct00 : * (& a) ≡ * (& b)
-                   ct00 = sym (cong (*) eq1)
-               ... | case2 lt = tri> (λ lt1 → <-irr (case2 lt) lt1) (λ eq → <-irr (case1 eq) lt) lt
+          ptotalx {a} {b} ia ib with trio< (ZChain.supf (pzc (pic<x (proj2 ia))) (IChain-i (proj2 ia)))  
+                                           (ZChain.supf (pzc (pic<x (proj2 ib))) (IChain-i (proj2 ib)))
+          ... | tri< ia<ib ¬b ¬c = uz01 where
+              uz01 : Tri (a < b) (a ≡ b) (b < a )
+              uz01 with pchainx⊆chain ia
+              ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib)))  ⟪ ai , ch-init fc ⟫ (pchainx⊆chain ib) 
+              ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u uz02 uz03 uz04 ⟫ (pchainx⊆chain ib) where
+                 uz05 : IChain-i (proj2 ia) o< IChain-i (proj2 ib)
+                 uz05 = ichain-inject {_} {_} {proj2 ia} {proj2 ib} ia<ib
+                 uz02 : u o< osuc (IChain-i (proj2 ib))
+                 uz02 = ordtrans<-≤ u<x ?
+                 uz03 : ZChain.supf (pzc (pic<x (proj2 ib))) u ≡ u
+                 uz03 = trans ( zeq _ _ ? ? ) su=u
+                 uz04 : FClosure A f (ZChain.supf (pzc (pic<x (proj2 ib))) u) (& a)
+                 uz04 = subst (λ k → FClosure A f k (& a)) ? fc
+          ... | tri≈ ¬a ia=ib ¬c = uz01 where
+              uz01 : Tri (a < b) (a ≡ b) (b < a )
+              uz01 with pchainx⊆chain ia
+              ... | ⟪ ai , ch-init fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib)))  ⟪ ai , ch-init fc ⟫  (pchainx⊆chain ib) 
+              ... | ⟪ ai , ch-is-sup u u<x su=u fc ⟫ = ZChain.f-total (pzc (pic<x (proj2 ib))) ⟪ ai , ch-is-sup u ? ? ? ⟫ (pchainx⊆chain ib) 
+          ... | tri> ¬a ¬b ib<ia = ?
 
           usup : MinSUP A pchainx
           usup = minsupP pchainx (λ ic → ? ) ptotalx