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

changeset 1145:f8c3537e68a6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 16 Jan 2023 02:22:03 +0900
parents 73b256c5474b
children 1966127fc14f
files src/Topology.agda
diffstat 1 files changed, 13 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sun Jan 15 23:02:36 2023 +0900
+++ b/src/Topology.agda	Mon Jan 16 02:22:03 2023 +0900
@@ -206,8 +206,8 @@
 record _covers_ ( P q : HOD  ) : Set n where
    field
        cover   : {x : Ordinal } → odef q x → Ordinal
-       P∋cover : {x : Ordinal } → {lt : odef q  x} → odef P (cover lt)
-       isCover : {x : Ordinal } → {lt : odef q  x} → odef (* (cover lt))  x
+       P∋cover : {x : Ordinal } → (lt : odef q  x) → odef P (cover lt)
+       isCover : {x : Ordinal } → (lt : odef q  x) → odef (* (cover lt))  x
 
 open _covers_
 
@@ -280,7 +280,7 @@
    cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
    cex {X} ox oc = & ( ODC.minimal O Cex  fip00)  where
       fip00 : ¬ ( Cex  =h= od∅ ) 
-      fip00 cex=0 = fip03 (FIP.is-limit fip (CCX ox) fip02 fip07 ) fip09 where 
+      fip00 cex=0 = ⊥-elim (fip09 fip25 fip20) where 
           fip03 : {x z : Ordinal } → odef (* x) z →  (¬ odef (* x) z) → ⊥
           fip03 {x} {z} xz nxz = nxz xz
           fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
@@ -290,30 +290,16 @@
           ... | tri≈ ¬a b ¬c  = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = C ; sy = subst (λ k → Subbase (* C) k) b sc } )) where
               fip10 : * C ⊆  CS top
               fip10 {w} cw = CCX ox ( C<CX cw )
-          fip01 : Ordinal
-          fip01 = FIP.limit fip (CCX ox) fip02
-          fip11 :  {w : Ordinal } → {Lw : odef L  w} → ¬ ( odef (* (cover oc Lw)) w )
-          fip11 {w} {Lw} pw = ? where
-                fip15 : odef (* X) (cover oc Lw)
-                fip15 = P∋cover oc {w} {Lw}
-                fip13 : HOD
-                fip13 = L ＼ * w
-                fip14 : odef (* (CX ox)) (& ( L ＼ * w ))
-                fip14 = ?
-                fip12 : odef ( L ＼ * w ) fip01
-                fip12 = subst (λ k → odef k fip01 ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip14 )
-          fip10 : odef ? fip01
-          fip10 = FIP.is-limit fip (CCX ox) fip02 ?
-          fip08 : odef L fip01
-          fip08 = FIP.L∋limit fip (CCX ox) fip02 ?
-          fip05 : odef (CS top) fip01 
-          fip05 = ?
-          fip07 : odef (* (CX ox)) ( cover oc fip08  )
-          fip07 = ?
-          fip09 : ¬ odef (* (cover oc fip08)) (FIP.limit fip (CCX ox) fip02)
-          fip09 = ?
-          fip04 : Ordinal
-          fip04 = cover oc (cs⊆L top (subst₂ (λ j k → odef j k ) refl (sym &iso) fip05) (FIP.is-limit fip (CCX ox) ? ?) )
+          fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
+          fip25 = FIP.L∋limit fip (CCX ox) fip02 ?
+          fip20 : {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 ))
+          fip20 {y} Xy yl = proj2 fip21 yl where
+              fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
+              fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } 
+              fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
+              fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
+          fip09 : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z )) 
+          fip09 {z} Lz nc  =  nc ( P∋cover oc Lz  ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
    ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ 
    ¬CXfip {X} ox oc = {!!} where
       fip04 : odef Cex (cex ox oc)