# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660871294 -32400
# Node ID 4822758b8bf8ab19591bc6de0ff6718b31372352
# Parent  802d70b7ea0147795ebe493c2fbe3fe6595b0f3b
...

diff -r 802d70b7ea01 -r 4822758b8bf8 src/zorn.agda
--- a/src/zorn.agda	Fri Aug 19 09:52:27 2022 +0900
+++ b/src/zorn.agda	Fri Aug 19 10:08:14 2022 +0900
@@ -327,7 +327,7 @@
                     zc07 = subst (λ k → k o≤ supf b) (sym su=ss) (supf-mono  (o<→≤ s<b)  )
                     zc08 :  u o≤ b 
                     zc08 with osuc-≡< zc07
-                    ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans ? su=sb ) ss<sb )
+                    ... | case1 su=sb = ⊥-elim ( o<¬≡ (trans (sym su=ss) su=sb ) ss<sb )
                     ... | case2 lt =  o<→≤ (supf-inject lt )
                 ... | case2 lt =  o<→≤ (ordtrans (supf-inject lt) s<b) 
       zc01  (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
@@ -393,7 +393,7 @@
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) with trio< ua ub
-     ... | tri< a₁ ¬b ¬c with ChainP.order supb  ? fca 
+     ... | tri< a₁ ¬b ¬c with ChainP.order supb  (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supa )) (sym (ChainP.supu=u supb )) a₁)  fca 
      ... | case1 eq with s≤fc (supf ub) f mf fcb 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -410,7 +410,7 @@
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x  supb fcb) | tri≈ ¬a  eq ¬c 
          = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (cong supf (sym eq)) fcb )
-     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa ? fcb 
+     ct-ind xa xb {a} {b} (ch-is-sup ua ua<x supa fca) (ch-is-sup ub ub<x supb fcb) | tri> ¬a ¬b c with ChainP.order supa (subst₂ (λ j k → j o< k ) (sym (ChainP.supu=u supb )) (sym (ChainP.supu=u supa )) c) fcb 
      ... | case1 eq with s≤fc (supf ua) f mf fca 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -758,7 +758,7 @@
               ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-init (fsuc _ fc₁)  ⟫ 
               ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
           no-extension : ¬ xSUP → ZChain A f mf ay x
-          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
+          no-extension ¬sp=x = record { supf = supf1 ;  sup = sup ; supf-mono = ?
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = ?
               ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
                  UnionCFR⊆ : {z0 z1 : Ordinal} → z0 o≤ z1 → z0 o< x → UnionCF A f mf ay supf1 z0 ⊆' UnionCF A f mf ay supf0 z1 
@@ -835,7 +835,7 @@
           ... | 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 ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; sup=u = {!!} 
+                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = ? ; sup=u = {!!} ; supf-mono = ?
                    ;  initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supx : SUP A (UnionCF A f mf ay supf0 x)
              supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
@@ -933,7 +933,7 @@
 
           no-extension : ¬ xSUP → ZChain A f mf ay x
           no-extension ¬sp=x  = record { initial = pinit ; chain∋init = pcy  ; supf = supf1  ; sup=u = sup=u
-               ; sup = sup ; supf-is-sup = sis
+               ; sup = sup ; supf-is-sup = sis ; supf-mono = ?
                ; csupf = ? ; chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
@@ -985,7 +985,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 = supf1  ; sup=u = {!!} 
-               ; sup = {!!} ; supf-is-sup = {!!}
+               ; sup = {!!} ; supf-is-sup = {!!} ; supf-mono = ?
                ;  chain⊆A = {!!} ;  f-next = {!!} ;  f-total = {!!} ; csupf = {!!}  } -- where -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  no-extension {!!} -- x is not f y' nor sup of former ZChain from y -- no extention