# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1664516287 -32400
# Node ID d4839adf694dcb9a9090b5edad7d89b1bf3f1137
# Parent  6222efcf3b043fed48f53f40c129d8dd33fa3220
...

diff -r 6222efcf3b04 -r d4839adf694d src/zorn.agda
--- a/src/zorn.agda	Fri Sep 30 10:55:23 2022 +0900
+++ b/src/zorn.agda	Fri Sep 30 14:38:07 2022 +0900
@@ -372,32 +372,43 @@
 z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
 z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
 
--- M→S  : {A B : HOD} → MinSUP A B → SUP A B
--- M→S {A} {B} ms = record { sup = MinSUP.sup ms ; as = MinSUP.asm ms ; x<sup = MinSUP.x<sup ms } 
+M→S  : { A : HOD } { f : Ordinal → Ordinal } {mf : ≤-monotonic-f A f} {y : Ordinal} {ay : odef A y}  { x : Ordinal }
+      →  (supf : Ordinal → Ordinal )
+      →  MinSUP A (UnionCF A f mf ay supf x)  
+      → SUP A (UnionCF A f mf ay supf x) 
+M→S {A} {f} {mf} {y} {ay} {x} supf ms = record { sup = * (MinSUP.sup ms) 
+        ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm ms) ; x<sup = ms00 } where
+   msup = MinSUP.sup ms
+   ms00 : {z : HOD} → UnionCF A f mf ay supf x ∋ z → (z ≡ * msup) ∨ (z < * msup)
+   ms00 {z} uz with MinSUP.x<sup ms uz 
+   ... | case1 eq = case1 (subst (λ k → k ≡ _) *iso ( cong (*) eq))
+   ... | case2 lt = case2 (subst₂ (λ j k →  j < k ) *iso refl lt )
+
 
 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
    field
       supf :  Ordinal → Ordinal 
+      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
+           → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
+
       asupf :  {x : Ordinal } → odef A (supf x)
+      supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
+      supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
+      x≤supfx : z o≤ supf z
+
+      minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
+      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (M→S supf (minsup x≤z) ))
+      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
+
    chain : HOD
    chain = UnionCF A f mf ay supf z
    chain⊆A : chain ⊆' A
    chain⊆A = λ lt → proj1 lt
-   field
-      supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      supf-< : {x y : Ordinal } → supf x o< supf  y → supf x << supf y
-      minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f mf ay supf x) 
    sup : {x : Ordinal } → x o≤ z  → SUP A (UnionCF A f mf ay supf x) 
-   sup {x} x≤z = ? -- M→S  (minsup x≤z )
-   field
-      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  
-           → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
-      supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
-      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain
-
-      -- supf-max : {x : Ordinal } → z o< x → supf x ≡ supf z -- supf z may different from spuf pz
-      x≤supfx : z o≤ supf z
+   sup {x} x≤z = M→S supf (minsup x≤z) 
+   supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
+   supf-is-minsup {x} x≤z = trans (supf-is-sup x≤z) &iso
 
    chain∋init : odef chain y
    chain∋init = ⟪ ay , ch-init (init ay refl)    ⟫
@@ -869,11 +880,11 @@
                       lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
                  ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp px f mf a b)
 
-                 sup1 : SUP A pchainpx 
-                 sup1 = supP pchainpx zc01 ptotal
+                 sup1 : MinSUP A pchainpx 
+                 sup1 = minsupP pchainpx zc01 ptotal
 
                  sp1 : Ordinal
-                 sp1 = & (SUP.sup sup1 )
+                 sp1 = MinSUP.sup sup1 
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
@@ -1145,9 +1156,9 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb)) 
   
-          usup : SUP A pchain
-          usup = supP pchain (λ lt → proj1 lt) ptotal0
-          spu = & (SUP.sup usup)
+          usup : MinSUP A pchain
+          usup = minsupP pchain (λ lt → proj1 lt) ptotal0
+          spu = MinSUP.sup usup
 
           supf1 : Ordinal → Ordinal
           supf1 z with trio< z x