# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660719107 -32400
# Node ID 22676639125fe372a04d99a3091e9d8ef0dfd976
# Parent  d395f1827e6aa30d283fdce311e08e16da2e76ca
retreat

diff -r d395f1827e6a -r 22676639125f src/zorn.agda
--- a/src/zorn.agda	Wed Aug 17 15:40:17 2022 +0900
+++ b/src/zorn.agda	Wed Aug 17 15:51:47 2022 +0900
@@ -702,12 +702,12 @@
                ax : odef A x
                is-sup : IsSup A (UnionCF A f mf ay supf0 px) ax
 
-          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o≤ px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
-          UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-          UnionCF⊆ {z0} {z1} z0≤1 z0≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
+          UnionCF⊆ : {z0 z1 : Ordinal} → (z0≤1 : z0 o≤ z1 ) →  (z0≤px :  z0 o< px ) → UnionCF A f mf ay supf0 z0 ⊆' UnionCF A f mf ay supf1 z1 
+          UnionCF⊆ {z0} {z1} z0<1 z0≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+          UnionCF⊆ {z0} {z1} z0<1 z0≤px ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
               zc60 : {w : Ordinal } → FClosure A f (supf0 u1) w → odef (UnionCF A f mf ay supf1 z1 ) w
               zc60 (init asp refl) with trio< u1 px | inspect supf1 u1
-              ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
+              ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0<1 ) 
                 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 (ChainP.supu=u u1-is-sup)   } (init (subst (λ k → odef A k ) (sym eq1) asp) eq1 )  ⟫ where
                   fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
                   fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ( ChainP.fcy<sup u1-is-sup fc )
@@ -717,7 +717,7 @@
                   ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
                   ... | tri≈ ¬a b ¬c = ? -- subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 fc )
                   ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (ordtrans s<u1 a) ))  --  px o< s < u1 < px
-              ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
+              ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0<1 ) 
                 record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 ?   } ?  ⟫ where
                   fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u1) ∨ (z << supf1 u1 )
                   fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym eq1) ? -- ( ChainP.fcy<sup u1-is-sup fc )
@@ -727,9 +727,9 @@
                   ... | tri< a ¬b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
                   ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ? -- ( ChainP.order u1-is-sup s<u1 fc )
                   ... | tri> ¬a ¬b px<s = ⊥-elim ( o<¬≡ refl (ordtrans px<s (subst (λ k → s o< k) b s<u1 ) ))  --  px o< s < u1 = px
-              ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } with osuc-≡< (OrdTrans u1≤x z0≤px)
-              ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
-              ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
+              ... | tri> ¬a ¬b px<u1 | record { eq = eq1 } = ? -- with osuc-≡< (OrdTrans u1≤x z0≤px)
+              -- ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) px<u1 ) 
+              -- ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
               zc60 (fsuc w1 fc) with zc60 fc
               ... | ⟪ 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₁) ⟫ 
@@ -737,9 +737,9 @@
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
                ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = 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 
-                 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                 UnionCFR⊆ {z0} {z1} z0≤1 z0≤x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc 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 
+                 UnionCFR⊆ {z0} {z1} z0≤1 z0<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                 UnionCFR⊆ {z0} {z1} z0≤1 z0<x ⟪ au , ch-is-sup u1 {w} u1≤x u1-is-sup fc ⟫   = zc60 fc where
                       zc60 : {w : Ordinal } → FClosure A f (supf1 u1) w → odef (UnionCF A f mf ay supf0 z1 ) w
                       zc60 {w} (init asp refl) with trio< u1 px | inspect supf1 u1
                       ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ A∋fcs _ f mf fc  , ch-is-sup u1 (OrdTrans u1≤x z0≤1 ) 
@@ -771,9 +771,9 @@
                       ... | case2 lt = ⊥-elim ( o<> lt px<u1 )
                       zc60 (init asp refl) | tri> ¬a ¬b px<u1 | record { eq = eq2} | tri> ¬a' ¬b' px<z0 = ⊥-elim ( ¬sp=x zcsup ) where
                          zc30 : x ≡ z0
-                         zc30 with osuc-≡< z0≤x
-                         ... | case1 eq = sym (eq)
-                         ... | case2 z0<x = ⊥-elim (¬p<x<op ⟪ px<z0 , subst (λ k → z0 o< k ) (sym (Oprev.oprev=x op)) z0<x ⟫ )
+                         zc30 = ? -- with osuc-≡< z0≤x
+                         -- ... | case1 eq = sym (eq)
+                         -- ... | case2 z0<x = ⊥-elim (¬p<x<op ⟪ px<z0 , subst (λ k → z0 o< k ) (sym (Oprev.oprev=x op)) z0<x ⟫ )
                          zc31 : x ≡ u1 
                          zc31 with trio< x u1 
                          ... | tri≈ ¬a b ¬c = b
@@ -804,15 +804,15 @@
                       ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1)  , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ 
                  sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z<x with trio< z px
-                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl (ordtrans z<x <-osuc) ) ( ZChain.sup zc  a ) 
+                 ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ? ) ( ZChain.sup zc  a ) 
                  ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
                      zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
-                     zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) (o<→≤ z<x)  lt )
+                     zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) ?  lt )
                  ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
                     b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o<→≤ a) lt) } 
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl ? lt) } 
                  ... | tri≈ ¬a b ¬c = ? -- ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ o≤-refl (o≤-refl0 b) lt) } 
                  ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where
                      zc30 : x ≡ b
@@ -821,10 +821,10 @@
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
                      zcsup : xSUP
                      zcsup with zc30
-                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) o≤-refl lt) } } 
+                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF⊆ (pxo≤x op) ? lt) } } 
                  csupf : {b : Ordinal} → b o< x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b<x with trio< b px | inspect supf1 b
-                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) ( ZChain.csupf zc  a  )
+                 ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl a ( ZChain.csupf zc  a  )
                  ... | tri≈ ¬a b ¬c | _ = ? -- UnionCF⊆ o≤-refl o≤-refl ( ZChain.csupf zc ? )
                  ... | tri> ¬a ¬b px<b | record { eq = eq1 } =  
                     ⟪ SUP.as sup1  , ch-is-sup ?  ? ? (subst (λ k → FClosure A f k sp1) (sym eq1) (init (SUP.as sup1) refl))  ⟫