Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 827:685f7ae1b821

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... remove ChainP.sup=u
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Aug 2022 09:30:32 +0900
parents da99e787cb7a
children 802d70b7ea01
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Aug 18 18:20:54 2022 +0900
+++ b/src/zorn.agda	Fri Aug 19 09:30:32 2022 +0900
@@ -252,7 +252,6 @@
    field
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 
       order    : {s z1 : Ordinal} → (lt : s o< u ) → FClosure A f (supf s ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
-      supu=u   : supf u ≡ u
 
 data UChain  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y )
        (supf : Ordinal → Ordinal) (x : Ordinal) : (z : Ordinal) → Set n where 
@@ -307,6 +306,7 @@
    ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u<z ) ) ))
    ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u<z ))) ) lt )
 
+   -- supf s o< b
    order : {b s z1 : Ordinal} → b o< z → s o< b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    order {b} {s} {z1} b<z s<b fc = zc04 where
       zc01 : {z1 : Ordinal } → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1
@@ -320,7 +320,7 @@
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
             ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where
                 zc06 : supf u ≡ u
-                zc06 = ChainP.supu=u is-sup
+                zc06 = sup=u ? ? ?
                 zc09 : u o≤ supf s  → ( u o≤ b ) ∨ ( supf u ≡ supf b )
                 zc09 u<s with osuc-≡< (subst (λ k → k o≤ supf s) (sym zc06) u<s)
                 ... | case1 su=ss = zc08 where
@@ -334,7 +334,9 @@
                 zc10 :  odef (UnionCF A f mf ay supf b)  (supf s)
                 zc10 with zc09 u≤x
                 ... | case1 lt = ⟪ as , ch-is-sup u lt is-sup fc ⟫ 
-                ... | case2 eq = ⟪ as , ch-is-sup u ?  is-sup ?  ⟫ 
+                ... | case2 eq = ⟪ as , ch-is-sup b ? record { fcy<sup = ? ; order = ? } (init ? ? )  ⟫  where
+                    zc11 : supf (supf s) ≡  supf s
+                    zc11 = ?
             zc03 : odef (UnionCF A f mf ay supf b)  (supf s)
             zc03 with csupf (o<→≤ s<z) 
             ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
@@ -552,8 +554,7 @@
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m09 {s} {z} s<b fcz = ZChain.order zc b<A s<b fcz    
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A )
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } }  
+              m06 = record {  fcy<sup = m08  ; order = m09 }
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -575,8 +576,7 @@
               m05 = sym (ZChain.sup=u zc ab (o<→≤  m09)
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} )   -- ZChain on x
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab (o<→≤  m09)
-                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} } 
+              m06 = record { fcy<sup = m07 ;  order = m08 }
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -741,7 +741,7 @@
               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 ) 
-                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
+                record { fcy<sup = fcy<sup ; order = order  } (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 )
                   order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
@@ -751,7 +751,7 @@
                   ... | tri≈ ¬a b ¬c = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym eq1) ( ChainP.order u1-is-sup s<u1 ? )
                   ... | 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 ) 
-                record { fcy<sup = fcy<sup ; order = order ; supu=u = trans eq1 ?   } (init (subst (λ k → odef A k ) (sym eq1) ? ) ? )  ⟫ where
+                record { fcy<sup = fcy<sup ; order = order } (init (subst (λ k → odef A k ) (sym 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 )
                   order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf1 s) z2 →
@@ -776,7 +776,7 @@
                       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 ) 
-                        record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym eq1) (ChainP.supu=u u1-is-sup)   } (init asp refl )  ⟫ where
+                        record { fcy<sup = fcy<sup ; order = order } (init asp refl )  ⟫ where
                           fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
                           fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) eq1 ( ChainP.fcy<sup u1-is-sup fc )
                           order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →
@@ -786,7 +786,7 @@
                           ... | tri≈ ¬a b ¬c | record { eq = eq2 } = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) eq1 ( ChainP.order u1-is-sup s<u1 (subst (λ k → FClosure A f k z2) (sym eq2) ? ))
                           ... | tri> ¬a ¬b px<s | record { eq = eq2 } = ⊥-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 ) 
-                        record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym ? ) (ChainP.supu=u u1-is-sup)   } (init ? ? )  ⟫ where
+                        record { fcy<sup = fcy<sup ; order = order } (init ? ? )  ⟫ where
                           fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u1) ∨ (z << supf0 u1 )
                           fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) ? ( ChainP.fcy<sup u1-is-sup fc )
                           order : {s : Ordinal} {z2 : Ordinal} → s o< u1 → FClosure A f (supf0 s) z2 →