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

changeset 1117:53ca3c609f0e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generated topology from subbase done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 01 Jan 2023 20:07:04 +0900
parents 6386019deef1
children 441ad880a45d
files src/Topology.agda
diffstat 1 files changed, 8 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sun Jan 01 20:03:29 2023 +0900
+++ b/src/Topology.agda	Sun Jan 01 20:07:04 2023 +0900
@@ -71,7 +71,7 @@
 record Base (L P : HOD) (u x : Ordinal) : Set n where
    field
        b   : Ordinal 
-       u⊂L : * u ⊂ L
+       u⊂L : * u ⊆ L
        sb  : Subbase P b
        b⊆u : * b ⊆ * u
        bx  : odef (* b) x
@@ -93,9 +93,9 @@
          ; o∪ = tp02 ; o∩ = tp01 } where
     tp00 : SO L P ⊆ Power L
     tp00 {u} ou x ux  with ou ux
-    ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = proj2 u⊂L (b⊆u bx)
+    ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx)
     tp01 :  {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q)
-    tp01 {p} {q} op oq {x} ux =  record { b = b ; u⊂L = subst (λ k → k ⊂ L) (sym *iso) ul  
+    tp01 {p} {q} op oq {x} ux =  record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul  
       ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx))   ; b⊆u = tp08 ; bx = tp14 } where
         px : odef (* (& p)) x
         px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) )
@@ -115,23 +115,21 @@
              tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12)
         tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x
         tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫
-        ul :  (p ∩ q) ⊂ L
-        ul = subst (λ k → k ⊂ L ) *iso ⟪ tp02 , (λ {z} pq →  proj2 (Base.u⊂L (op px)) (pz pq) ) ⟫ where
+        ul :  (p ∩ q) ⊆ L
+        ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq →  (Base.u⊂L (op px)) (pz pq) )  where
             pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z
             pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) )
-            tp02 : & (* (& (p ∩ q))) o< & L
-            tp02 = subst ( λ k → k o< & L) (sym &iso) ?
     tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q
     tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux
     ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx
-    ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊂L = subst (λ k → k ⊂ L) (sym *iso) tp04 
+    ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) tp04 
            ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06  ; bx = bx } where
         tp05 :  Union q ⊆ L
         tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx
         ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } 
            = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx ))
-        tp04 :  Union q ⊂ L
-        tp04 = ⟪ ? , tp05 ⟫
+        tp04 :  Union q ⊆ L
+        tp04 = tp05 
         tp06 : * b ⊆ Union q
         tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz  }