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

diff -r 88731edfa691 -r 091e7a80bfe3 src/zorn.agda
--- a/src/zorn.agda	Sun Dec 11 20:38:22 2022 +0900
+++ b/src/zorn.agda	Mon Dec 12 07:24:45 2022 +0900
@@ -283,16 +283,14 @@
 
 -- Union of chain lower than x
 
-record IChain  {A : HOD}  { f : Ordinal → Ordinal } {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
-  field
-     i : Ordinal
-     i<x : i o< x
-     s<x : supfz i<x o≤ i 
-     fc : FClosure A f (supfz i<x) z
+data IChain  {A : HOD}  { f : Ordinal → Ordinal } {y : Ordinal } (ay : odef A y ) 
+               {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) : (z : Ordinal ) → Set n where
+    ic-init : {z : Ordinal } (fc : FClosure A f y z) → IChain ay supfz z
+    ic-isup : {z : Ordinal} (i : Ordinal) (i<x : i o< x) (s<x : supfz i<x o≤ i ) (fc : FClosure A f (supfz i<x) z) → IChain ay supfz z
 
-UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) { x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal)  → HOD
-UnionIC A f supfz 
-   = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} supfz z } ;
+UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) { x : Ordinal } {y : Ordinal } (ay : odef A y ) (supfz : {z : Ordinal } → z o< x → Ordinal)  → HOD
+UnionIC A f ay supfz 
+   = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} ay supfz z } ;
        odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y )
@@ -1267,7 +1265,7 @@
           supfz {z} z<x = ZChain.supf (pzc  (ob<x lim z<x)) z
 
           pchainx : HOD
-          pchainx = UnionIC A f supfz 
+          pchainx = UnionIC A f ay supfz 
 
           zeq : {xa xb z : Ordinal }
              → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
@@ -1278,45 +1276,54 @@
           iceq : {ix iy : Ordinal } → ix ≡ iy → {i<x : ix o< x } {i<y : iy o< x } → supfz i<x ≡ supfz i<y
           iceq refl = cong supfz  o<-irr
 
-          ifc≤ : {za zb : Ordinal } ( ia : IChain supfz za ) ( ib : IChain supfz zb ) → (ia≤ib : IChain.i ia o≤ IChain.i ib )
-              → FClosure A f (ZChain.supf (pzc (ob<x lim (IChain.i<x ib))) (IChain.i ia)) za
-          ifc≤ {za} {zb} ia ib ia≤ib = subst (λ k → FClosure A f k _ ) (zeq _ _ (osucc ia≤ib) (o<→≤ <-osuc) )   (IChain.fc ia)
+          IChain-i : {z : Ordinal } → IChain ay supfz z → Ordinal
+          IChain-i (ic-init fc) = o∅
+          IChain-i (ic-isup ia ia<x sa<x fca) = ia
 
-          pic<x : {z : Ordinal } → (ic : IChain supfz z ) → osuc (IChain.i ic) o< x
-          pic<x {z} ic = ob<x lim (IChain.i<x ic)
+          pic<x : {z : Ordinal } → (ic : IChain ay supfz z ) → osuc (IChain-i ic) o< x
+          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 ⟫ = ZChain.cfcs (pzc (pic<x  ic) ) <-osuc o≤-refl uz03 (IChain.fc ic) where
-               uz02 : FClosure A f (ZChain.supf (pzc (pic<x ic )) (IChain.i ic)) z
-               uz02 = IChain.fc ic
-               uz03 : ZChain.supf (pzc (pic<x ic)) (IChain.i ic) o≤ IChain.i ic
-               uz03 = IChain.s<x ic
+          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
+               uz02 : FClosure A f (ZChain.supf (pzc (ob<x lim ia<x)) ia ) z
+               uz02 = fca
+               uz03 : ZChain.supf (pzc (ob<x lim ia<x)) ia o≤ ia
+               uz03 = sa<x
 
-          chain⊆pchainx : {z : Ordinal } → (z<x : z o< x) → odef (ZChain.chain (pzc (ob<x lim z<x))) z → odef pchainx z 
-          chain⊆pchainx {z} z<x ⟪ ua , ch-init fc ⟫ = ⟪ ua , record { i = o∅ ; i<x = ? ; s<x = ? ; fc = ?  }  ⟫
-          chain⊆pchainx {z} z<x ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , record {  i = ? ; i<x = ? ; s<x = ? 
-             ; fc = subst (λ  k → FClosure A f k z ) ? fc }  ⟫
+          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
 
           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 (IChain.i<x ia))  (supfz (IChain.i<x ib))
+               uz01 with trio< (supfz (pic<x ia))  (supfz (pic<x ib))
                ... | tri< ia<ib ¬b ¬c with
-                    ≤-ftrans (ZChain.order (pzc (ob<x lim (IChain.i<x ib))) ? ? (ifc≤ ia ib (o<→≤ ?))) (s≤fc _ f mf (IChain.fc ib))
+                    ≤-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 (IChain.fc ia) (subst (λ k → FClosure A f k (& b)) (sym ia=ib) (IChain.fc ib))
+               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 (IChain.i<x ia))) ? ? (ifc≤ ib ia (o<→≤ ?))) (s≤fc _ f mf (IChain.fc ia))
+                    ≤-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
 
           usup : MinSUP A pchainx
-          usup = minsupP pchainx (λ ic → A∋fc _ f mf (IChain.fc (proj2 ic) ) ) ptotalx
+          usup = minsupP pchainx (λ ic → ? ) ptotalx
           spu = MinSUP.sup usup
 
           supf1 : Ordinal → Ordinal