# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668933190 -32400
# Node ID f80d525e6a6b0a02becdcbed004386d22d787028
# Parent  7c39cae23803a6def6f3d0c72f027e2075fa1a74
Recursive record IChain

diff -r 7c39cae23803 -r f80d525e6a6b src/zorn.agda
--- a/src/zorn.agda	Sun Nov 20 16:07:25 2022 +0900
+++ b/src/zorn.agda	Sun Nov 20 17:33:10 2022 +0900
@@ -1304,22 +1304,36 @@
 
           ysp =  MinSUP.sup (ysup f mf ay)
 
-          supf0 : Ordinal → Ordinal
-          supf0 z with trio< z x
-          ... | tri< a ¬b ¬c = ZChain.supf (pzc  (ob<x lim a)) z
-          ... | tri≈ ¬a b ¬c = ysp
-          ... | tri> ¬a ¬b c = ysp
+          supfz : {z : Ordinal } → z o< x → Ordinal
+          supfz {z} z<x = ZChain.supf (pzc  (ob<x lim z<x)) z
+
+          record IChain (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
+              field
+                 i : Ordinal  
+                 i<x : i o< x
+                 fc : FClosure A f (supfz i<x) z 
+
+          pchainx : HOD
+          pchainx = record { od = record { def = λ z → IChain supfz z } ; odmax = & A ; <odmax = zc00 } where
+               zc00 : {z : Ordinal } → IChain supfz z → z o< & A
+               zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
 
-          pchain : HOD
-          pchain = UnionCF A f mf ay supf0 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
 
-          ptotal0 : IsTotalOrderSet pchain
-          ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
+          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 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb))
+               uz01 with trio< (IChain.i ia) (IChain.i ib)
+               ... | tri< a ¬b ¬c = ?
+               ... | tri≈ ¬a b ¬c = ?
+               ... | tri> ¬a ¬b c = ?
 
-          usup : MinSUP A pchain
-          usup = minsupP pchain (λ lt → proj1 lt) ptotal0
+          usup : MinSUP A pchainx
+          usup = minsupP pchainx (λ lt → ? ) ptotalx
           spu = MinSUP.sup usup
 
           supf1 : Ordinal → Ordinal
@@ -1328,14 +1342,15 @@
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
 
-          pchain1 : HOD
-          pchain1 = UnionCF A f mf ay supf1 x
+          pchain : HOD
+          pchain = UnionCF A f mf ay supf1 x
+
+          -- pchain ⊆ pchainx
 
-          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
+          ptotal : IsTotalOrderSet pchain
+          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))
 
           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
@@ -1349,9 +1364,9 @@
           ... | 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 ? ?) ⟫           
+          -- 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} with trio< z x