# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658797662 -32400
# Node ID 068cba4ee934744687dc0e19c061d0096e569d3c
# Parent  7679fef530738bab457a40d2a6a08e8089578b62
...

diff -r 7679fef53073 -r 068cba4ee934 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 26 03:37:25 2022 +0900
+++ b/src/zorn.agda	Tue Jul 26 10:07:42 2022 +0900
@@ -301,7 +301,7 @@
       f-total : IsTotalOrderSet chain
 
       supf-mono : { a b : Ordinal } → a o< b → supf a o≤ supf b
-      csupf : {z : Ordinal } → odef chain (supf z) 
+      csupf : (z : Ordinal ) → odef chain (supf z) 
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
       order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
@@ -630,7 +630,7 @@
 
      inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
      inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy 
-      ; csupf = λ {z} → csupf {z} ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 ) ; supf-mono = λ _ → o≤-refl
+      ; csupf = λ z → csupf z ; fcy<sup = λ u<0 → ⊥-elim ( ¬x<0 u<0 ) ; supf-mono = λ _ → o≤-refl
       ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; order = λ b<0 → ⊥-elim (¬x<0 b<0) } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
@@ -654,8 +654,8 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)  
 
-          csupf : {z : Ordinal} → odef (UnionCF A f mf ay isupf o∅) (isupf z)
-          csupf {z} = ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where
+          csupf : (z : Ordinal) → odef (UnionCF A f mf ay isupf o∅) (isupf z)
+          csupf z = ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where
                uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi)
                uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc )
                ... | case1 eq = case1 ( begin
@@ -710,8 +710,8 @@
 
           supf0 = ZChain.supf zc
 
-          csupf : {z : Ordinal} → odef (UnionCF A f mf ay supf0 x) (supf0 z)
-          csupf {z} with ZChain.csupf zc {z}
+          csupf : (z : Ordinal) → odef (UnionCF A f mf ay supf0 x) (supf0 z)
+          csupf z with ZChain.csupf zc z
           ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
           ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , ch-is-sup u is-sup fc ⟫ 
 
@@ -783,34 +783,44 @@
               ... | tri≈ ¬a b ¬c | record { eq = eq1 } = subst (λ k → spu ≡ psupf k) b (sym eq1)
               ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬b z=x)
 
-          csupf :{z : Ordinal} → odef (UnionCF A f mf ay psupf x) (psupf z)
-          csupf {z} with trio< z x | inspect psupf z
+          csupf : (z : Ordinal) → odef (UnionCF A f mf ay psupf x) (psupf z)
+          csupf z with trio< z x | inspect psupf z
           ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
                 ozc = pzc (osuc z) (ob<x lim z<x)
-                zc12 : odef A (ZChain.supf ozc z) 
-                    ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
-                zc12  = ZChain.csupf ozc {z}
+                oz<x : osuc z o< x
+                oz<x = ?
+                zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
+                zc12  = ZChain.csupf ozc z
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-                zc11 with zc12
-                ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                ... | ⟪ az , ch-is-sup u is-sup fc ⟫ = ⟪ az , z13 fc is-sup ⟫ where
-                   z13 : FClosure A f (ZChain.supf ozc u ) (ZChain.supf ozc z ) →  ChainP A f mf ay (ZChain.supf ozc) u (ZChain.supf ozc z )
-                       →  UChain A f mf ay psupf x (ZChain.supf ozc z )
-                   z13 fc is-sup = ?
-
-                -- ch-is-sup z 
-                --     zc14 (subst (λ k → FClosure A f k (ZChain.supf ozc z)) (sym eq1) (init az))  ⟫  where
-                --      zc14 :  ChainP A f mf ay psupf z (ZChain.supf ozc z)
-                --      zc14 = record { csupz = ? ; supfu=u = ? ; fcy<sup = ? ; order = ? } where
-                --          csupz : FClosure A f (psupf z) (ZChain.supf ozc z)
-                --          csupz = ?
-
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc15 
-                  (subst (λ k → FClosure A f k spu) zc17  (init (SUP.A∋maximal usup)))  ⟫ where
-                zc15 : ChainP A f mf ay psupf x spu
-                zc15 = ?
+                zc11 with ZChain.csupf ozc z | inspect (ZChain.csupf ozc) z
+                ... | ⟪ az , ch-init fc ⟫ | _ = ⟪ az , ch-init fc ⟫ 
+                ... | ⟪ az , ch-is-sup u is-sup fc ⟫ | record { eq = eq2 } 
+                   = ⟪ az , ch-is-sup u zc18 (subst (λ k → FClosure A f k _) zc16 fc)  ⟫  where
+                      zc14 : ZChain.csupf ozc z ≡ ⟪ az , ch-is-sup u is-sup fc ⟫
+                      zc14 = eq2
+                      zc13 : odef A (ZChain.supf ozc u) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc u)
+                      zc13  = ZChain.csupf ozc u
+                      zc15 : FClosure A f (ZChain.supf ozc u) (ZChain.supf ozc z) 
+                      zc15 = fc
+                      zc17 : u ≡ psupf z
+                      zc17 = ?
+                      zc19 : u o< x
+                      zc19 = ?
+                      zc16 : ZChain.supf ozc u ≡ psupf u 
+                      zc16 = ?
+                      zc18 : ChainP A f mf ay psupf u (ZChain.supf ozc z)
+                      zc18 = record { csupz = subst (λ k → FClosure A f k _) zc16 fc
+                         ; supfu=u = ? ; fcy<sup = ? ; order = ? }
+          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup spu zc15 
+                  (subst (λ k → FClosure A f k spu) zc18 (init sa))  ⟫ where
+                sa = SUP.A∋maximal usup
+                zc18 : spu ≡ psupf spu
+                zc18 = ?
                 zc17 : spu ≡ psupf x 
                 zc17 = subst (λ k → spu ≡ psupf k  ) b (sym eq1) 
+                zc15 : ChainP A f mf ay psupf spu spu
+                zc15 = record { csupz = subst (λ k → FClosure A f k spu) zc18 (init sa)
+                         ; supfu=u = sym zc18 ; fcy<sup = ? ; order = ? }
           ... | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc16
                   (subst (λ k → FClosure A f k spu) psupf=x (init (SUP.A∋maximal usup)))  ⟫ where
                 zc16 : ChainP A f mf ay psupf x spu