Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/ODUtil.agda @ 1489:0dbbae768c90 default tip
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jul 2024 23:04:17 +0900 |
| parents | 5dacb669f13b |
| children |
| rev | line source |
|---|---|
| 1463 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 431 | 2 open import Level |
| 3 open import Ordinals | |
| 1463 | 4 import HODBase |
| 5 import OD | |
| 6 module ODUtil {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) where | |
| 431 | 7 |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 431 | 9 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
10 open import Data.Nat.Properties |
| 431 | 11 open import Data.Empty |
| 1463 | 12 open import Data.Unit |
| 431 | 13 open import Relation.Nullary |
| 1463 | 14 open import Relation.Binary hiding (_⇔_) |
| 15 open import Relation.Binary.Core hiding (_⇔_) | |
| 1464 | 16 import Relation.Binary.Reasoning.Setoid as EqR |
| 431 | 17 |
| 18 open import logic | |
| 1463 | 19 import OrdUtil |
| 431 | 20 open import nat |
| 21 | |
| 22 open Ordinals.Ordinals O | |
| 23 open Ordinals.IsOrdinals isOrdinal | |
| 1300 | 24 -- open Ordinals.IsNext isNext |
| 431 | 25 open OrdUtil O |
| 26 | |
| 1463 | 27 -- Ordinal Definable Set |
| 28 | |
| 29 open HODBase.HOD | |
| 30 open HODBase.OD | |
| 31 | |
| 32 open _∧_ | |
| 33 open _∨_ | |
| 34 open Bool | |
| 35 | |
| 36 open HODBase._==_ | |
| 37 | |
| 38 open HODBase.ODAxiom HODAxiom | |
| 39 open OD O HODAxiom | |
| 431 | 40 |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
41 _⊂_ : ( A B : HOD) → Set n |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
42 _⊂_ A B = ( & A o< & B) ∧ ( A ⊆ B ) |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
43 |
| 1116 | 44 ⊆∩-dist : {a b c : HOD} → a ⊆ b → a ⊆ c → a ⊆ ( b ∩ c ) |
| 45 ⊆∩-dist {a} {b} {c} a<b a<c {z} az = ⟪ a<b az , a<c az ⟫ | |
| 46 | |
| 47 ⊆∩-incl-1 : {a b c : HOD} → a ⊆ c → ( a ∩ b ) ⊆ c | |
| 48 ⊆∩-incl-1 {a} {b} {c} a<c {z} ab = a<c (proj1 ab) | |
| 49 | |
| 50 ⊆∩-incl-2 : {a b c : HOD} → a ⊆ c → ( b ∩ a ) ⊆ c | |
| 51 ⊆∩-incl-2 {a} {b} {c} a<c {z} ab = a<c (proj2 ab) | |
| 52 | |
| 1483 | 53 *iso∩ : {p q : HOD} → (p ∩ q) =h= (* (& p) ∩ * (& q)) |
| 54 eq→ (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq← *iso px , eq← *iso qx ⟫ | |
| 55 eq← (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq→ *iso px , eq→ *iso qx ⟫ | |
| 56 | |
| 1485 | 57 ∩-cong : {A B C D : HOD} → A =h= B → C =h= D → (A ∩ C) =h= (B ∩ D) |
| 58 eq→ (∩-cong eq1 eq2) {x} lt = ⟪ eq→ eq1 (proj1 lt) , eq→ eq2 (proj2 lt) ⟫ | |
| 59 eq← (∩-cong eq1 eq2) {x} lt = ⟪ eq← eq1 (proj1 lt) , eq← eq2 (proj2 lt) ⟫ | |
| 60 | |
| 1467 | 61 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A |
| 62 power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where | |
| 63 t1 : {x : HOD } → t ∋ x → A ∋ x | |
| 64 t1 = power→ A t PA∋t | |
| 65 | |
| 66 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y ) | |
| 67 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where | |
| 68 p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z | |
| 69 p01 {z} xyz = power→ A x ax (proj1 xyz ) | |
| 70 | |
|
1475
6752e2ff4dc6
ordinal (countable Ordinal) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1467
diff
changeset
|
71 odef-not : {S : HOD} {x : Ordinal } → ¬ ( odef S x ) → odef S x → ⊥ |
|
6752e2ff4dc6
ordinal (countable Ordinal) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1467
diff
changeset
|
72 odef-not neg sx = ⊥-elim ( neg sx ) |
| 1467 | 73 |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
74 cseq : HOD → HOD |
| 431 | 75 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where |
| 76 lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x) | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
77 lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) |
| 431 | 78 |
| 1463 | 79 ∩-comm : { A B : HOD } → (A ∩ B) =h= (B ∩ A) |
| 80 ∩-comm {A} {B} = record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ } | |
| 1150 | 81 |
| 82 _∪_ : ( A B : HOD ) → HOD | |
| 83 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ; | |
| 84 odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where | |
| 85 lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B) | |
| 86 lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _) | |
| 87 lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _) | |
| 88 | |
| 1485 | 89 ∪-cong : {A B C D : HOD} → A =h= B → C =h= D → (A ∪ C) =h= (B ∪ D) |
| 90 eq→ (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case1 lt) = case1 (eq→ eq1 lt) | |
| 91 eq→ (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case2 lt) = case2 (eq→ eq2 lt) | |
| 92 eq← (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case1 lt) = case1 (eq← eq1 lt) | |
| 93 eq← (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case2 lt) = case2 (eq← eq2 lt) | |
| 94 | |
| 1463 | 95 x∪x≡x : { A : HOD } → (A ∪ A) =h= A |
| 96 x∪x≡x {A} = record { eq← = λ {x} lt → case1 lt ; eq→ = lem00 } where | |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
97 lem00 : {x : Ordinal} → odef A x ∨ odef A x → odef A x |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
98 lem00 {x} (case1 ax) = ax |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
99 lem00 {x} (case2 ax) = ax |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
100 |
| 1150 | 101 _＼_ : ( A B : HOD ) → HOD |
| 102 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) } | |
| 103 | |
| 104 ¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x ) | |
| 105 ¬∅∋ {x} = ¬x<0 | |
| 106 | |
| 431 | 107 |
| 108 pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) ) | |
| 109 pair-xx<xy {x} {y} = ⊆→o≤ lemma where | |
| 110 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z | |
| 111 lemma {z} (case1 refl) = case1 refl | |
| 112 lemma {z} (case2 refl) = case1 refl | |
| 113 | |
| 114 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
115 trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab) |
| 431 | 116 |
| 1126 | 117 trans-⊂ : { A B C : HOD} → A ⊂ B → B ⊂ C → A ⊂ C |
| 118 trans-⊂ ⟪ A<B , A⊆B ⟫ ⟪ B<C , B⊆C ⟫ = ⟪ ordtrans A<B B<C , (λ ab → B⊆C (A⊆B ab)) ⟫ | |
| 119 | |
| 431 | 120 refl-⊆ : {A : HOD} → A ⊆ A |
| 1096 | 121 refl-⊆ x = x |
| 431 | 122 |
| 123 od⊆→o≤ : {x y : HOD } → x ⊆ y → & x o< osuc (& y) | |
| 1096 | 124 od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) &iso (lt (d→∋ x x>z))) |
| 431 | 125 |
| 480 | 126 ⊆→= : {F U : HOD} → F ⊆ U → U ⊆ F → F =h= U |
| 1096 | 127 ⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (FU (subst (λ k → odef F k) (sym &iso) lt) ) |
| 128 ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (UF (subst (λ k → odef U k) (sym &iso) lt) ) } | |
| 480 | 129 |
| 519 | 130 ¬A∋x→A≡od∅ : (A : HOD) → {x : HOD} → A ∋ x → ¬ ( & A ≡ o∅ ) |
| 131 ¬A∋x→A≡od∅ A {x} ax a=0 = ¬x<0 ( subst (λ k → & x o< k) a=0 (c<→o< ax )) | |
| 132 | |
| 431 | 133 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A ) |
| 134 subset-lemma {A} {x} = record { | |
| 1096 | 135 proj1 = λ lt x∋z → subst (λ k → odef A k ) &iso ( proj1 (lt (subst (λ k → odef x k) (sym &iso) x∋z ) )) |
| 136 ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫ | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
137 } |
| 431 | 138 |
| 139 nat→ω : Nat → HOD | |
| 140 nat→ω Zero = od∅ | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
141 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) |
| 431 | 142 |
| 1300 | 143 ω→nato : {y : Ordinal} → Omega-d y → Nat |
| 431 | 144 ω→nato iφ = Zero |
| 145 ω→nato (isuc lt) = Suc (ω→nato lt) | |
| 146 | |
| 1463 | 147 ω→nat : (n : HOD) → Omega ho< ∋ n → Nat |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
148 ω→nat n = ω→nato |
| 431 | 149 |
| 1463 | 150 ω∋nat→ω : {n : Nat} → def (od (Omega ho<)) (& (nat→ω n)) |
| 151 ω∋nat→ω {Zero} = subst (λ k → def (od (Omega ho<)) k) (sym ord-od∅) iφ | |
| 152 ω∋nat→ω {Suc n} = subst (λ k → Omega-d k) (sym (==→o≡ nat01)) nat00 where | |
| 153 nat00 : Omega-d (& (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n)))))) | |
| 154 nat00 = isuc ( ω∋nat→ω {n}) | |
| 155 nat01 : Union (nat→ω n , ( nat→ω n , nat→ω n)) =h= Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n)))) | |
| 156 nat01 = ==-sym Omega-iso | |
| 431 | 157 |
| 158 pair1 : { x y : HOD } → (x , y ) ∋ x | |
| 159 pair1 = case1 refl | |
| 160 | |
| 161 pair2 : { x y : HOD } → (x , y ) ∋ y | |
| 162 pair2 = case2 refl | |
| 163 | |
| 1463 | 164 single : {x y : HOD } → (x , x ) ∋ y → x =h= y |
| 165 single (case1 eq) = ord→== (sym eq) | |
| 166 single (case2 eq) = ord→== (sym eq) | |
| 431 | 167 |
| 1096 | 168 single& : {x y : Ordinal } → odef (* x , * x ) y → x ≡ y |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
169 single& (case1 eq) = sym (trans eq &iso) |
| 1096 | 170 single& (case2 eq) = sym (trans eq &iso) |
| 171 | |
| 172 pair=∨ : {a b c : Ordinal } → odef (* a , * b) c → ( a ≡ c ) ∨ ( b ≡ c ) | |
| 173 pair=∨ {a} {b} {c} (case1 c=a) = case1 ( sym (trans c=a &iso)) | |
| 174 pair=∨ {a} {b} {c} (case2 c=b) = case2 ( sym (trans c=b &iso)) | |
| 175 | |
| 431 | 176 ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y) |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
177 ω-prev-eq1 {x} {y} eq x<y with eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl |
| 1467 | 178 ; ox = eq→ (==-sym *iso) (case1 refl) } -- (* x , (* x , * x)) ∋ * y |
| 1096 | 179 ... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u |
| 180 ... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
181 osuc y ≡⟨ sym (cong osuc &iso) ⟩ |
| 1096 | 182 osuc (& (* y)) ≤⟨ osucc (c<→o< {* y} {* u} uy) ⟩ -- * x ≡ * u ∋ * y |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
183 & (* u) ≡⟨ &iso ⟩ |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
184 u ≡⟨ u=x ⟩ |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
185 & (* x) ≡⟨ &iso ⟩ |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
186 x ∎ ))) where open o≤-Reasoning O |
| 1096 | 187 ... | case2 u=xx = ⊥-elim (o<¬≡ ( begin |
| 1467 | 188 x ≡⟨ single& ( eq← (==-sym *iso) (subst₂ (λ j k → odef j k ) (cong (*) u=xx ) &iso uy)) ⟩ |
| 1096 | 189 y ∎ ) x<y) where open ≡-Reasoning |
| 431 | 190 |
| 1464 | 191 Omega-inject : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → y ≡ x |
| 192 Omega-inject {x} {y} eq with trio< x y | |
| 193 Omega-inject {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a) | |
| 194 Omega-inject {x} {y} eq | tri≈ ¬a b ¬c = (sym b) | |
| 195 Omega-inject {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) | |
| 431 | 196 |
| 1463 | 197 ω-inject : {x y : HOD} → Union ( y , ( y , y)) =h= Union ( x , ( x , x)) → y =h= x |
| 1464 | 198 ω-inject {x} {y} eq = ord→== ( Omega-inject (==→o≡ (==-trans Omega-iso (==-trans eq (==-sym Omega-iso))))) |
| 1301 | 199 |
| 431 | 200 ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x |
| 1467 | 201 ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = eq→ (==-sym *iso) (case2 refl) } |
| 431 | 202 |
| 1464 | 203 ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) =h= od∅ ) |
| 204 ωs≠0 x = ∅< {Union ( x , ( x , x))} (ω-∈s _) | |
| 205 | |
| 206 ω→nato-cong : {n m : Ordinal} → (x : odef (Omega ho< ) n) (y : odef (Omega ho< ) m) → n ≡ m → ω→nato x ≡ ω→nato y | |
| 207 ω→nato-cong OD.iφ OD.iφ eq = refl | |
| 208 ω→nato-cong OD.iφ (OD.isuc {x} y) eq = ⊥-elim ( ∅< {Union (* x , (* x , * x))} {* x} (ω-∈s _) (≡o∅→=od∅ (sym eq) ) ) | |
| 209 ω→nato-cong (OD.isuc {x} y) OD.iφ eq = ⊥-elim ( ∅< {Union (* x , (* x , * x))} {* x} (ω-∈s _) (≡o∅→=od∅ eq ) ) | |
| 210 ω→nato-cong (OD.isuc x) (OD.isuc y) eq = cong Suc ( ω→nato-cong x y (Omega-inject eq) ) | |
| 431 | 211 |
| 1301 | 212 ωs0 : o∅ ≡ & (nat→ω 0) |
| 213 ωs0 = trans (sym ord-od∅) (cong (&) refl ) | |
| 214 | |
| 1464 | 215 Omega-subst : (x y : HOD) → x =h= y → Union ( x , (x , x)) =h= Union ( y , (y , y)) |
| 216 Omega-subst x y x=y = begin | |
| 217 Union (x , (x , x)) ≈⟨ ==-sym Omega-iso ⟩ | |
| 218 Union (* (& x) , (* (& x) , * (& x))) ≈⟨ ord→== (cong (λ k → & (Union (* k , (* k , * k )))) (==→o≡ x=y) ) ⟩ | |
| 219 Union (* (& y) , (* (& y) , * (& y))) ≈⟨ Omega-iso ⟩ | |
| 220 Union (y , (y , y)) ∎ where open EqR ==-Setoid | |
| 221 | |
| 1463 | 222 nat→ω-iso : {i : HOD} → (lt : Omega ho< ∋ i ) → nat→ω ( ω→nat i lt ) =h= i |
| 1467 | 223 nat→ω-iso {i} lt = ==-trans (nat→ω-iso-ord _ lt) *iso where |
| 1464 | 224 nat→ω-iso-ord : (x : Ordinal) → (lt : odef (Omega ho< ) x) → nat→ω ( ω→nato lt ) =h= (* x) |
| 225 nat→ω-iso-ord _ OD.iφ = ==-sym o∅==od∅ | |
| 1467 | 226 nat→ω-iso-ord x (OD.isuc OD.iφ) = ==-trans (Omega-subst _ _ (==-sym o∅==od∅)) (==-sym *iso) |
| 1464 | 227 nat→ω-iso-ord x (OD.isuc (OD.isuc {y} lt)) = ==-trans (Omega-subst _ _ |
| 1467 | 228 (==-trans (Omega-subst _ _ lem02 ) (==-sym *iso))) (==-sym *iso) where |
| 1464 | 229 lem02 : nat→ω ( ω→nato lt ) =h= (* y) |
| 230 lem02 = nat→ω-iso-ord y lt | |
| 431 | 231 |
| 1464 | 232 ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : Omega-d ox) → * ox =h= nat→ω x → ω→nato ltd ≡ x |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
233 ω→nat-iso0 Zero iφ eq = refl |
| 1464 | 234 ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (begin |
| 235 Union (nat→ω x , (nat→ω x , nat→ω x)) ≈⟨ ==-sym eq ⟩ | |
| 236 * o∅ ≈⟨ o∅==od∅ ⟩ | |
| 237 od∅ ∎ )) where open EqR ==-Setoid | |
| 1467 | 238 ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (==-trans (==-sym *iso) eq) ) |
| 1100 | 239 ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where |
| 1464 | 240 lemma1 : * (& (Union (* x , (* x , * x)))) =h= Union (nat→ω i , (nat→ω i , nat→ω i)) → * x =h= nat→ω i |
| 241 lemma1 eq = begin | |
| 242 * x ≈⟨ (o≡→== ( Omega-inject (==→o≡ (begin | |
| 1467 | 243 Union (* x , (* x , * x)) ≈⟨ ==-sym *iso ⟩ |
| 1464 | 244 * (& ( Union (* x , (* x , * x)))) ≈⟨ eq ⟩ |
| 245 Union ((nat→ω i) , (nat→ω i , nat→ω i)) ≈⟨ ==-sym Omega-iso ⟩ | |
| 246 Union (* (& (nat→ω i)) , (* (& (nat→ω i)) , * (& (nat→ω i)))) ∎ )) )) ⟩ | |
| 1467 | 247 * (& ( nat→ω i)) ≈⟨ *iso ⟩ |
| 1464 | 248 nat→ω i ∎ where open EqR ==-Setoid |
| 1100 | 249 |
| 431 | 250 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i |
| 1467 | 251 ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso |
| 431 | 252 |
| 1464 | 253 nat→ω-inject : {i j : Nat} → nat→ω i =h= nat→ω j → i ≡ j |
| 1301 | 254 nat→ω-inject {Zero} {Zero} eq = refl |
| 1464 | 255 nat→ω-inject {Zero} {Suc j} eq = ⊥-elim ( ∅< {Union (nat→ω j , (nat→ω j , nat→ω j))} (ω-∈s _) (==-sym eq) ) |
| 256 nat→ω-inject {Suc i} {Zero} eq = ⊥-elim ( ∅< {Union (nat→ω i , (nat→ω i , nat→ω i))} (ω-∈s _) eq ) | |
| 257 nat→ω-inject {Suc i} {Suc j} eq = cong Suc (nat→ω-inject {i} {j} ( ω-inject eq )) | |
| 1301 | 258 |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
259 Repl⊆ : {A B : HOD} (A⊆B : A ⊆ B) → { ψa : ( x : HOD) → A ∋ x → HOD } { ψb : ( x : HOD) → B ∋ x → HOD } |
| 1285 | 260 → {Ca : HOD} → {rca : RXCod A Ca ψa } |
| 261 → {Cb : HOD} → {rcb : RXCod B Cb ψb } | |
| 1106 | 262 → ( {z : Ordinal } → (az : odef A z ) → (ψa (* z) (subst (odef A) (sym &iso) az) ≡ ψb (* z) (subst (odef B) (sym &iso) (A⊆B az)))) |
| 1285 | 263 → Replace' A ψa rca ⊆ Replace' B ψb rcb |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
264 Repl⊆ {A} {B} A⊆B {ψa} {ψb} eq record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = A⊆B az |
| 1106 | 265 ; x=ψz = trans x=ψz (cong (&) (eq az) ) } |
| 266 | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
267 PPP : {P : HOD} → Power P ∋ P |
| 1467 | 268 PPP {P} z pz = eq← (==-sym *iso) pz |
| 1106 | 269 |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
270 UPower⊆Q : {P Q : HOD} → P ⊆ Q → Union (Power P) ⊆ Q |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
271 UPower⊆Q {P} {Q} P⊆Q {z} record { owner = y ; ao = ppy ; ox = yz } = P⊆Q (ppy _ yz) |
| 1106 | 272 |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
273 UPower∩ : {P : HOD} → ({ p q : HOD } → P ∋ p → P ∋ q → P ∋ (p ∩ q)) |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
274 → { p q : HOD } → Union (Power P) ∋ p → Union (Power P) ∋ q → Union (Power P) ∋ (p ∩ q) |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
275 UPower∩ {P} each {p} {q} record { owner = x ; ao = ppx ; ox = xz } record { owner = y ; ao = ppy ; ox = yz } |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
276 = record { owner = & P ; ao = PPP ; ox = lem03 } where |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1106
diff
changeset
|
277 lem03 : odef (* (& P)) (& (p ∩ q)) |
| 1467 | 278 lem03 = eq→ (==-sym *iso) ( each (ppx _ xz) (ppy _ yz) ) |
| 1150 | 279 |