# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658761751 -32400
# Node ID 798d8b8c36b161c6e70a6152b15208b2d3085f06
# Parent  34678c0ad2788dee4a58c9788223a7d3368ffd03
...

diff -r 34678c0ad278 -r 798d8b8c36b1 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 25 23:38:38 2022 +0900
+++ b/src/zorn.agda	Tue Jul 26 00:09:11 2022 +0900
@@ -73,6 +73,10 @@
 ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
 ≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 
+<=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y 
+<=to≤ (case1 eq) = case1 (cong (*) eq)
+<=to≤ (case2 lt) = case2 lt
+
 <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
 <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
@@ -503,28 +507,7 @@
                     m03 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a -- if a ∈ chain of px, is-max of px can be used
                     m03 with proj2 ua
                     ... | ch-init fc = ⟪ proj1 ua ,  ch-init fc ⟫
-                    ... | ch-is-sup u is-sup-a fc with trio< u px
-                    ... | tri< a ¬b ¬c    = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫ -- u o< osuc x
-                    ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫
-                    ... | tri> ¬a ¬b c = m08 where
-                         --  a and b is a sup of chain, order forces minimulity of sup
-                         su=u : ZChain.supf zc u ≡ u
-                         su=u = ChainP.supfu=u is-sup-a 
-                         u<A : u o< & A
-                         u<A = z09 (subst (λ k → odef A k ) su=u (proj1 (ZChain.csupf zc )))
-                         u≤a : (* u ≡ * a) ∨ (u << a)
-                         u≤a = s≤fc u f mf (subst (λ k → FClosure A f k a) su=u fc ) 
-                         m07 : osuc b o≤ x
-                         m07 = osucc (ordtrans b<px px<x )
-                         fcb : FClosure A f (ZChain.supf zc b) b
-                         fcb = subst (λ k → FClosure A f k b ) (sym (ZChain.sup=u zc ab (z09 ab) 
-                            (record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x m07 o≤-refl lt)  } ) )) ( init ab )
-                         m08 :  odef (UnionCF A f mf ay (ZChain.supf zc) px) a 
-                         m08 with osuc-≡<  (ZChain.supf-mono zc (ordtrans b<px c))
-                         ... | case1 eq = ?
-                         ... | case2 lt  with subst (λ k → b <= k ) su=u ( ZChain.order zc u<A lt fcb )
-                         ... | case2 b<u = ⊥-elim (<-irr u≤a (ptrans a<b b<u ) ) 
-                         ... | case1 eq = ⊥-elim ( <-irr (s≤fc u f mf (subst (λ k → FClosure A f k a ) su=u fc )) (subst (λ k → * a < * k) eq a<b ))
+                    ... | ch-is-sup u is-sup-a fc = ⟪ proj1 ua , ch-is-sup u  is-sup-a fc ⟫
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
@@ -538,7 +521,7 @@
                     m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
                     m09 : {sup1 z1 : Ordinal} → (ZChain.supf zc sup1) o< (ZChain.supf zc b) 
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
-                    m09 {sup1} {z} s<b fcz = ZChain.order zc b<A ? fcz
+                    m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
                     m06 : ChainP A f mf ay (ZChain.supf zc) b b
                     m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) ; supfu=u = sym m05 
                       ; fcy<sup = m08  ; order = m09 } 
@@ -719,7 +702,7 @@
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u is-sup fc = ≤-ftrans ? (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= (ZChain.supf zc) u 
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
@@ -736,7 +719,7 @@
           --
           no-extension : ZChain A f mf ay x
           no-extension = record { supf = supf0
-               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?
+               ; initial = pinit ; chain∋init = pcy  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ? ; supf-mono = ZChain.supf-mono zc
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } 
 
           zc4 : ZChain A f mf ay x 
@@ -747,8 +730,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 = ?
-                     ; initial = ? ; chain∋init  = ? }  where
+                record {  supf = psupf1 ; chain⊆A = ? ; f-next = ? ; f-total = ? ; csupf = ? ; sup=u = ? ; order = ? ; fcy<sup = ? 
+                   ; supf-mono = ? ; initial = ? ; chain∋init  = ? }  where
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf zc z
@@ -836,7 +819,7 @@
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with  ua
           ... | ch-init fc = s≤fc y f mf fc
-          ... | ch-is-sup u is-sup fc = ≤-ftrans ? (s≤fc _ f mf fc)  where
+          ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= psupf _
                zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
@@ -858,8 +841,7 @@
 
           no-extension : ZChain A f mf ay x
           no-extension  = record { initial = pinit ; chain∋init = pcy  ; supf = psupf  ; csupf = csupf ; sup=u = ? ; order = ? ; fcy<sup = ?
-              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
-
+              ; supf-mono = ? ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = no-extension -- ¬ A ∋ p, just skip
@@ -868,7 +850,7 @@
           ... | case1 pr = no-extension  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = record { initial = {!!} ; chain∋init = {!!}  ; supf = psupf1  ; csupf = ? ; sup=u = ? ; order = ? ; fcy<sup = ?
-              ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
+              ; supf-mono = ? ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = ? } where -- x is a sup of (zc ?) 
              psupf1 : Ordinal → Ordinal
              psupf1 z with trio< z x 
              ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z