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

changeset 1115:97f4a14d88ce

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 17:02:54 +0900
parents ba3e053b85d4
children 6386019deef1
files src/Topology.agda
diffstat 1 files changed, 25 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sun Jan 01 15:51:08 2023 +0900
+++ b/src/Topology.agda	Sun Jan 01 17:02:54 2023 +0900
@@ -66,21 +66,18 @@
 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫
 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso  xy))
 
---  OS = { U ⊂ X | ∀ x ∈ U → ∃ b ∈ B →  x ∈ b ⊂ U }
+--  OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P →  x ∈ b ⊂ U }
 
-record aBase (P : HOD) {u x : Ordinal} (ux : odef (* u) x) : Set n where
+record Base (L P : HOD) (u x : Ordinal) : Set n where
    field
        b   : Ordinal 
+       u⊂L : * u ⊂ L
        sb  : Subbase P b
        b⊆u : * b ⊆ * u
        bx  : odef (* b) x
 
-record Base (P : HOD) (u : Ordinal) : Set n where
-   field
-       ab  : {x : Ordinal } → (ux : odef (* u) x ) → aBase P ux
-
-SO : (P : HOD) → HOD
-SO P = record { od = record { def = λ x → Base P x } ; odmax = ? ; <odmax = ? }
+SO : (L P : HOD) → HOD
+SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = ? ; <odmax = ? }
 
 record IsSubBase (L P : HOD) : Set (suc n) where
    field
@@ -90,8 +87,26 @@
        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 P ; OS⊆PL = ?
-         ; o∪ = ? ; o∩ = ? } 
+GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00
+         ; 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)
+    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
+        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)))
+        ul :  (p ∩ q) ⊂ L
+        ul = subst (λ k → k ⊂ L ) *iso ⟪ ? , (λ {z} pq →  IsSubBase.P⊆PL isb ? _ pq ) ⟫
+    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 = ? }
 
 -- covers