Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/Topology.agda @ 1115:97f4a14d88ce
....
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 01 Jan 2023 17:02:54 +0900 |
parents | ba3e053b85d4 |
children | 6386019deef1 |
comparison
equal
deleted
inserted
replaced
1114:ba3e053b85d4 | 1115:97f4a14d88ce |
---|---|
64 | 64 |
65 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y | 65 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y |
66 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫ | 66 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫ |
67 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) | 67 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) |
68 | 68 |
69 -- OS = { U ⊂ X | ∀ x ∈ U → ∃ b ∈ B → x ∈ b ⊂ U } | 69 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U } |
70 | 70 |
71 record aBase (P : HOD) {u x : Ordinal} (ux : odef (* u) x) : Set n where | 71 record Base (L P : HOD) (u x : Ordinal) : Set n where |
72 field | 72 field |
73 b : Ordinal | 73 b : Ordinal |
74 u⊂L : * u ⊂ L | |
74 sb : Subbase P b | 75 sb : Subbase P b |
75 b⊆u : * b ⊆ * u | 76 b⊆u : * b ⊆ * u |
76 bx : odef (* b) x | 77 bx : odef (* b) x |
77 | 78 |
78 record Base (P : HOD) (u : Ordinal) : Set n where | 79 SO : (L P : HOD) → HOD |
79 field | 80 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = ? ; <odmax = ? } |
80 ab : {x : Ordinal } → (ux : odef (* u) x ) → aBase P ux | |
81 | |
82 SO : (P : HOD) → HOD | |
83 SO P = record { od = record { def = λ x → Base P x } ; odmax = ? ; <odmax = ? } | |
84 | 81 |
85 record IsSubBase (L P : HOD) : Set (suc n) where | 82 record IsSubBase (L P : HOD) : Set (suc n) where |
86 field | 83 field |
87 P⊆PL : P ⊆ Power L | 84 P⊆PL : P ⊆ Power L |
88 p : {x : HOD} → L ∋ x → HOD | 85 p : {x : HOD} → L ∋ x → HOD |
89 Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx | 86 Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx |
90 px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x | 87 px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x |
91 | 88 |
92 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L | 89 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L |
93 GeneratedTopogy L P isb = record { OS = SO P ; OS⊆PL = ? | 90 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 |
94 ; o∪ = ? ; o∩ = ? } | 91 ; o∪ = tp02 ; o∩ = tp01 } where |
92 tp00 : SO L P ⊆ Power L | |
93 tp00 {u} ou x ux with ou ux | |
94 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = proj2 u⊂L (b⊆u bx) | |
95 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) | |
96 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊂ L) (sym *iso) ul | |
97 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = ? ; bx = ? } where | |
98 px : odef (* (& p)) x | |
99 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) | |
100 qx : odef (* (& q)) x | |
101 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) | |
102 b : Ordinal | |
103 b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) | |
104 ul : (p ∩ q) ⊂ L | |
105 ul = subst (λ k → k ⊂ L ) *iso ⟪ ? , (λ {z} pq → IsSubBase.P⊆PL isb ? _ pq ) ⟫ | |
106 tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q | |
107 tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux | |
108 ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | |
109 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = ? ; u⊂L = ? ; sb = ? ; b⊆u = ? ; bx = ? } | |
95 | 110 |
96 -- covers | 111 -- covers |
97 | 112 |
98 record _covers_ ( P q : HOD ) : Set (suc n) where | 113 record _covers_ ( P q : HOD ) : Set (suc n) where |
99 field | 114 field |