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

changeset 1116:6386019deef1

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 Sun, 01 Jan 2023 20:03:29 +0900
parents 97f4a14d88ce
children 53ca3c609f0e
files src/ODUtil.agda src/Topology.agda
diffstat 2 files changed, 42 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODUtil.agda	Sun Jan 01 17:02:54 2023 +0900
+++ b/src/ODUtil.agda	Sun Jan 01 20:03:29 2023 +0900
@@ -32,6 +32,15 @@
 _⊂_ : ( A B : HOD) → Set n
 _⊂_ A B = ( & A o< & B) ∧ ( A ⊆ B )
 
+⊆∩-dist : {a b c : HOD} → a ⊆ b → a ⊆ c  →  a ⊆ ( b ∩ c )
+⊆∩-dist {a} {b} {c} a<b a<c {z} az = ⟪ a<b az , a<c az ⟫
+
+⊆∩-incl-1 : {a b c : HOD} → a ⊆ c → ( a ∩ b ) ⊆ c
+⊆∩-incl-1 {a} {b} {c} a<c {z} ab = a<c (proj1 ab)
+
+⊆∩-incl-2 : {a b c : HOD} → a ⊆ c → ( b ∩ a ) ⊆ c
+⊆∩-incl-2 {a} {b} {c} a<c {z} ab = a<c (proj2 ab)
+
 cseq :  HOD  →  HOD
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
--- a/src/Topology.agda	Sun Jan 01 17:02:54 2023 +0900
+++ b/src/Topology.agda	Sun Jan 01 20:03:29 2023 +0900
@@ -82,9 +82,11 @@
 record IsSubBase (L P : HOD) : Set (suc n) where
    field
        P⊆PL  : P ⊆ Power L
-       p    : {x : HOD} → L ∋ x → HOD
-       Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
-       px   : {x : HOD} → {lx : L ∋ x } → p lx ∋ x
+
+--  we may need these if OS ∋ L is necessary
+--     p    : {x : HOD} → L ∋ x → HOD
+--     Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
+--     px   : {x : HOD} → {lx : L ∋ x } → p lx ∋ x
 
 GeneratedTopogy : (L P : HOD) → IsSubBase L P  → Topology L
 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00
@@ -94,19 +96,44 @@
     ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = proj2 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  
-      ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx))   ; b⊆u = ? ; bx = ? } where
+      ; 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 ) )
         qx : odef (* (& q)) x
         qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) )
         b : Ordinal
         b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx)))
+        tp08 :  * b ⊆ * (& (p ∩ q) )
+        tp08 =  subst₂ (λ j k → j ⊆ k ) (sym *iso)  (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where 
+             tp11 : * (Base.b (op px))  ⊆ * (& p )
+             tp11 = Base.b⊆u (op px)
+             tp12 : * (Base.b (oq qx))  ⊆ * (& q )
+             tp12 = Base.b⊆u (oq qx)
+             tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p 
+             tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11)
+             tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q 
+             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 ⟪ ? , (λ {z} pq →  IsSubBase.P⊆PL isb ? _ pq ) ⟫
+        ul = subst (λ k → k ⊂ L ) *iso ⟪ tp02 , (λ {z} pq →  proj2 (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 = ? ; u⊂L = ? ; sb = ? ; b⊆u = ? ; bx = ? }
+    ... | 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 ⟫
+        tp06 : * b ⊆ Union q
+        tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz  } 
 
 -- covers