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