# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662893929 -32400
# Node ID 8a49ab1dcbd0481274215b06279a1c008fa7a46e
# Parent  b095c84310dfc95d8291b8895ea15c3f5bbaaa58
...

diff -r b095c84310df -r 8a49ab1dcbd0 src/zorn.agda
--- a/src/zorn.agda	Sat Sep 10 18:20:24 2022 +0900
+++ b/src/zorn.agda	Sun Sep 11 19:58:49 2022 +0900
@@ -351,13 +351,69 @@
 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
-record Zsupf ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
+zsupf0 : ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)  
+        → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
+        → { z : Ordinal } → (odef A z) → SUP A (UnionCF A f mf ay (λ _ → z) z)
+zsupf0 A f mf ay supP {z} az =  supP chain (λ lt → proj1 lt ) f-total where
+    chain = UnionCF A f mf ay (λ _ → z) z
+    f-total : IsTotalOrderSet chain
+    f-total {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 (λ _ → z) ( (proj2 ca)) ( (proj2 cb))
+
+record ZSupf ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
-      s : Ordinal
-      s=z : odef A z → s ≡ z
-      as : odef A s
-      sup : SUP A (UnionCF A f mf ay (λ _ → s) z)
+      supf : Ordinal → Ordinal
+      sup : (x : Ordinal ) → SUP A (UnionCF A f mf ay (λ _ → z) x)
+      supf-is-sup : {x : Ordinal } → supf x ≡ & (SUP.sup (sup x) )
+      supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
+
+
+zsupf : (A : HOD) ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) 
+    → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
+    →  (x : Ordinal)   → ZSupf A f mf ay x
+zsupf A f mf {y} ay supP x = TransFinite { λ x →  ZSupf A f mf ay x } zc1 x where
+
+    zc1 :  (x : Ordinal) →  ((y₁ : Ordinal) → y₁ o< x → ZSupf A f mf ay y₁) → ZSupf A f mf ay x
+    zc1 x prev with Oprev-p x
+    ... | yes op = record { supf = ? ; sup = ? ; spuf-is-sup = ? ; supf-mono = ? }  where
+       px = Oprev.oprev op
+       zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
+       zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+       supf : Ordinal → Ordinal
+       supf z with trio< z px
+       ... | tri< a ¬b ¬c = ZSupf.spuf (prev (ordtrans a (pxo<x op))) z
+       ... | tri≈ ¬a b ¬c = ZSupf.spuf (prev (subst (λ k → k o< x ) b (pxo<x op))) z
+       ... | tri> ¬a ¬b px<x with ODC.∋-p O A (* x)
+       ... | no noax = ZSupf.spuf (prev o≤-refl ) px
+       ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) z f )   
+       ... | case1 pr = ZSupf.spuf (prev o≤-refl ) px
+       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
+       ... | case2 ¬x=sup = ZSupf.spuf (prev o≤-refl ) px
+       ... | case1 is-sup = ?
+
+    ... | no lim = ?  where
+
+       --  Range of supf is total order set, so it has SUP
+       supfmax :  Ordinal
+       supfmax = ?
+
+       supfx :  Ordinal
+       supfx with ODC.∋-p O A (* x)
+       ... | no noax = supfmax
+       ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) z f )   
+       ... | case1 pr = supfmax
+       ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
+       ... | case2 ¬x=sup = supfmax
+       ... | case1 is-sup = ?
+
+       supf : Ordinal → Ordinal
+       supf z with trio< z x
+       ... | tri< a ¬b ¬c = ZSupf.spuf a z
+       ... | tri≈ ¬a b ¬c = supfx
+       ... | tri> ¬a ¬b px<x = supfx
+
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where