# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659392981 -32400
# Node ID 1db222b676d8ef928193536c5720ed0b15af0cc9
# Parent  7472e3dc002bf52a44cf321de711a0652703fc36
...

diff -r 7472e3dc002b -r 1db222b676d8 src/zorn.agda
--- a/src/zorn.agda	Mon Aug 01 18:51:27 2022 +0900
+++ b/src/zorn.agda	Tue Aug 02 07:29:41 2022 +0900
@@ -312,16 +312,16 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
-      sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x)
-      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
+      sup : {x : Ordinal } → x o< z  → SUP A (UnionCF A f mf ay supf x)
+      supf-is-sup : {x : Ordinal } → (x<z : x o< z) → supf x ≡ & (SUP.sup (sup x<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 
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
       supf-mono : {x y : Ordinal } → x o< y → supf x o≤ supf y
    fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
-   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
+   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup u<z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
-   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) ))
+   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
    order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z sf<sb fc = zc04 where
         zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
@@ -342,12 +342,12 @@
             zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (zc01 fc  )
             ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 
             ... | ⟪ as , ch-is-sup u is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc) ⟫ 
-        zc00 : ( * z1  ≡  SUP.sup (sup (o<→≤ b<z ))) ∨ ( * z1  < SUP.sup ( sup (o<→≤ b<z )) )
-        zc00 = SUP.x<sup (sup (o<→≤ b<z)) (zc01 fc )
+        zc00 : ( * z1  ≡  SUP.sup (sup b<z )) ∨ ( * z1  < SUP.sup ( sup b<z ) )
+        zc00 = SUP.x<sup (sup b<z) (zc01 fc )
         zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
         zc04 with zc00
-        ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup (o<→≤ b<z )) ) (cong (&) eq) )
-        ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup (o<→≤ b<z )) )))  lt )
+        ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (supf-is-sup  b<z ) ) (cong (&) eq) )
+        ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (supf-is-sup b<z ) )))  lt )
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
@@ -665,8 +665,8 @@
      ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
      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 
-      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) } where
+     inititalChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = sup ; supf-is-sup =  λ b<0 → ⊥-elim (¬x<0 b<0)
+      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ⊥-elim (¬x<0 b<0) ; supf-mono = mono ; csupf = csupf } where
           spi =  & (SUP.sup (ysup f mf ay))
           isupf : Ordinal → Ordinal
           isupf z = spi
@@ -676,6 +676,8 @@
           cy = ⟪ ay , ch-init (init ay refl)  ⟫
           y<sup : * y ≤ SUP.sup (ysup f mf ay)
           y<sup = SUP.x<sup  (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay refl))
+          sup : {x : Ordinal} → x o< o∅ → SUP A (UnionCF A f mf ay isupf x)
+          sup {x} lt = ⊥-elim ( ¬x<0 lt )
           isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
           isy {z} ⟪ az , uz ⟫ with uz 
           ... | ch-init fc = s≤fc y f mf fc 
@@ -688,9 +690,10 @@
           itotal {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 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 refl) ⟫ where
+          mono : {x : Ordinal} {z : Ordinal} → x o< z → isupf x o≤ isupf z 
+          mono {x} {z} x<z = o≤-refl
+          csupf : {z : Ordinal} → z o≤ o∅ → odef (UnionCF A f mf ay isupf z ) (isupf z)
+          csupf {z} z≤0 = ⟪ asi , ch-is-sup spi uz02 (init asi refl) ⟫ 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
@@ -748,8 +751,8 @@
           -- if previous chain satisfies maximality, we caan reuse it
           --
           no-extension : ZChain A f mf ay x
-          no-extension = record { supf = supf0
-               ; initial = pinit ; chain∋init = pcy  ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} 
+          no-extension = record { supf = supf0 ; supf-mono = ZChain.supf-mono zc ; sup = ?
+               ; initial = pinit ; chain∋init = pcy  ; sup=u = {!!} ; supf-is-sup = ? ; csupf = ? 
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
 
           zc4 : ZChain A f mf ay x 
@@ -760,8 +763,8 @@
           ... | case1 pr = no-extension -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; order = {!!} ; fcy<sup = {!!} 
-                   ; supf-mono = {!!} ; initial = {!!} ; chain∋init  = {!!} }  where
+                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} 
+                   ; supf-mono = {!!} ; initial = {!!} ; chain∋init  = {!!} ; sup = ? ; supf-is-sup = ? ; supf-mono = ? }  where
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf zc z
@@ -816,8 +819,10 @@
           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)
+                zc13 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) z (ZChain.supf ozc z)
+                zc13  = ZChain.csupf ozc (ordtrans o≤-refl <-osuc )
                 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 ?
+                zc12  = ?
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
                 zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
                       az : odef A ( ZChain.supf ozc z )