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

changeset 1114:ba3e053b85d4

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 15:51:08 +0900
parents 384ba5a3c019
children 97f4a14d88ce
files src/Topology.agda
diffstat 1 files changed, 18 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sun Jan 01 13:46:38 2023 +0900
+++ b/src/Topology.agda	Sun Jan 01 15:51:08 2023 +0900
@@ -58,9 +58,6 @@
    gi : {x : Ordinal } → odef P x → Subbase P x
    g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y))
 
-SI : (P : HOD) → HOD
-SI P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? }
-
 sbp :  (P : HOD) {x : Ordinal } → Subbase P x → Ordinal
 sbp P {x} (gi {y} px) = x
 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb
@@ -69,6 +66,22 @@
 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 }
+
+record aBase (P : HOD) {u x : Ordinal} (ux : odef (* u) x) : Set n where
+   field
+       b   : Ordinal 
+       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 = ? }
+
 record IsSubBase (L P : HOD) : Set (suc n) where
    field
        P⊆PL  : P ⊆ Power L
@@ -77,16 +90,8 @@
        px   : {x : HOD} → {lx : L ∋ x } → p lx ∋ x
 
 GeneratedTopogy : (L P : HOD) → IsSubBase L P  → Topology L
-GeneratedTopogy L P isb = record { OS = Union (Power (SI P)) ; OS⊆PL = UPower⊆Q {SI P} {Power L} OS⊆PL0
-         ; o∪ = tp01 ; o∩ = UPower∩ tp04 } where
-       OS⊆PL0 :  SI P ⊆ Power L
-       OS⊆PL0 (gi px) z xz = IsSubBase.P⊆PL isb px _ xz
-       OS⊆PL0 (g∩ {x} {y} px py) z xz = IsSubBase.P⊆PL isb (proj1 (is-sbp P px (proj1 (subst (λ k → odef k z) *iso xz )) )) _
-            (proj2 (is-sbp P px (proj1 (subst (λ k → odef k z) *iso xz )) ))
-       tp04 : {p q : HOD} → SI P ∋ p → SI P ∋ q → SI P ∋ (p ∩ q)
-       tp04 {p} {q} pp pq = subst (λ k → odef (SI P) k ) (cong₂ (λ j k → & ( j  ∩ k )) *iso *iso )  ( g∩ pp pq )
-       tp01 : {q : HOD} → q ⊂ Union (Power (SI P)) → Union (Power (SI P)) ∋ Union q
-       tp01 {q} ⟪ q<ups , qp ⟫ = record { owner = ? ; ao = ? ; ox = ? }
+GeneratedTopogy L P isb = record { OS = SO P ; OS⊆PL = ?
+         ; o∪ = ? ; o∩ = ? } 
 
 -- covers