Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 382:c3a0fb13e267
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 Jul 2020 21:32:58 +0900 |
| parents | d2cb5278e46d |
| children | 5994f10d9bfd |
| rev | line source |
|---|---|
| 190 | 1 open import Level |
| 236 | 2 open import Ordinals |
| 3 module filter {n : Level } (O : Ordinals {n}) where | |
| 4 | |
| 190 | 5 open import zf |
| 236 | 6 open import logic |
| 7 import OD | |
| 193 | 8 |
| 363 | 9 open import Relation.Nullary |
| 10 open import Relation.Binary | |
| 11 open import Data.Empty | |
| 190 | 12 open import Relation.Binary |
| 13 open import Relation.Binary.Core | |
| 363 | 14 open import Relation.Binary.PropositionalEquality |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 363 | 16 import BAlgbra |
| 293 | 17 |
| 18 open BAlgbra O | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
19 |
| 236 | 20 open inOrdinal O |
| 21 open OD O | |
| 22 open OD.OD | |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
23 open ODAxiom odAxiom |
| 190 | 24 |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
25 import ODC |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
26 |
| 236 | 27 open _∧_ |
| 28 open _∨_ | |
| 29 open Bool | |
| 30 | |
| 295 | 31 -- Kunen p.76 and p.53, we use ⊆ |
| 329 | 32 record Filter ( L : HOD ) : Set (suc n) where |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
33 field |
| 329 | 34 filter : HOD |
| 290 | 35 f⊆PL : filter ⊆ Power L |
| 329 | 36 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q |
| 37 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
38 |
| 292 | 39 open Filter |
| 40 | |
| 329 | 41 record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
| 295 | 42 field |
| 43 proper : ¬ (filter P ∋ od∅) | |
| 329 | 44 prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
| 292 | 45 |
| 329 | 46 record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
| 295 | 47 field |
| 48 proper : ¬ (filter P ∋ od∅) | |
| 329 | 49 ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
50 |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
51 open _⊆_ |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
52 |
| 329 | 53 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
54 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
55 |
| 374 | 56 refl-⊆ : {A : HOD} → A ⊆ A |
| 57 refl-⊆ {A} = record { incl = λ x → x } | |
| 58 | |
| 329 | 59 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A |
| 331 | 60 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where |
| 329 | 61 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
62 t1 = zf.IsZF.power→ isZF A t PA∋t |
| 292 | 63 |
| 329 | 64 ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
65 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt ) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
66 |
| 329 | 67 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
68 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
69 |
| 329 | 70 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
71 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
72 |
| 329 | 73 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
74 q∩q⊆q = record { incl = λ lt → proj1 lt } |
| 265 | 75 |
| 331 | 76 open HOD |
| 77 | |
| 295 | 78 ----- |
| 79 -- | |
| 80 -- ultra filter is prime | |
| 81 -- | |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
82 |
| 329 | 83 filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P |
| 295 | 84 filter-lemma1 {L} P u = record { |
| 85 proper = ultra-filter.proper u | |
| 86 ; prime = lemma3 | |
| 87 } where | |
| 329 | 88 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
| 295 | 89 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) |
| 90 ... | case1 p∈P = case1 p∈P | |
| 91 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where | |
| 331 | 92 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
93 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
94 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
95 } where |
| 331 | 96 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x |
|
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
97 lemma4 x lt with proj1 lt |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
98 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
99 lemma4 x lt | case2 qx = qx |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
100 lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p)) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
101 lemma6 = filter2 P lt ¬p∈P |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
102 lemma7 : filter P ∋ (q ∩ (L ＼ p)) |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
103 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6 |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
104 lemma8 : (q ∩ (L ＼ p)) ⊆ q |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
105 lemma8 = q∩q⊆q |
|
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
106 |
| 295 | 107 ----- |
| 108 -- | |
| 109 -- if Filter contains L, prime filter is ultra | |
| 110 -- | |
| 111 | |
| 329 | 112 filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
113 filter-lemma2 {L} P f∋L prime = record { |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
114 proper = prime-filter.proper prime |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
115 ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
116 } where |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
117 open _==_ |
| 331 | 118 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) |
| 119 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) | |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
120 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x |
|
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
121 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) |
| 331 | 122 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x )) |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
123 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p |
| 329 | 124 lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p)) |
|
296
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
125 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L |
| 293 | 126 |
| 329 | 127 record Dense (P : HOD ) : Set (suc n) where |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
128 field |
| 329 | 129 dense : HOD |
| 379 | 130 d⊆P : dense ⊆ Power P |
| 329 | 131 dense-f : HOD → HOD |
| 368 | 132 dense-d : { p : HOD} → p ⊆ P → dense ∋ dense-f p |
| 133 dense-p : { p : HOD} → p ⊆ P → p ⊆ (dense-f p) | |
| 266 | 134 |
| 329 | 135 record Ideal ( L : HOD ) : Set (suc n) where |
| 293 | 136 field |
| 329 | 137 ideal : HOD |
| 293 | 138 i⊆PL : ideal ⊆ Power L |
| 329 | 139 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q |
| 140 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) | |
| 293 | 141 |
| 142 open Ideal | |
| 143 | |
| 329 | 144 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n |
| 293 | 145 proper-ideal {L} P {p} = ideal P ∋ od∅ |
| 146 | |
| 329 | 147 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n |
| 293 | 148 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) |
| 149 | |
| 374 | 150 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where |
| 370 | 151 field |
| 374 | 152 filter : L → Set n |
| 371 | 153 f⊆P : PL filter |
| 374 | 154 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q |
| 371 | 155 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q) |
| 156 | |
| 374 | 157 Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ |
| 158 Filter-is-F {L} f = record { | |
| 159 filter = λ x → Lift (suc n) ((filter f) ∋ x) | |
| 160 ; f⊆P = λ x f∋x → power→⊆ _ _ (incl ( f⊆PL f ) (lower f∋x )) | |
| 161 ; filter1 = λ {p} {q} q⊆L f∋p p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q) | |
| 162 ; filter2 = λ {p} {q} f∋p f∋q → lift ( filter2 f (lower f∋p) (lower f∋q)) | |
| 163 } | |
| 164 | |
| 379 | 165 record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where |
| 166 field | |
| 167 dense : L → Set n | |
| 168 d⊆P : PL dense | |
| 169 dense-f : L → L | |
| 170 dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p ) | |
| 171 dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) | |
| 172 | |
| 173 Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ | |
| 174 Dense-is-F {L} f = record { | |
| 175 dense = λ x → Lift (suc n) ((dense f) ∋ x) | |
| 176 ; d⊆P = λ x f∋x → power→⊆ _ _ (incl ( d⊆P f ) (lower f∋x )) | |
| 177 ; dense-f = λ x → dense-f f x | |
| 178 ; dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) ) | |
| 179 ; dense-p = λ {p} d → dense-p f (d p refl-⊆) | |
| 180 } where open Dense | |
| 181 | |
| 182 ------- | |
| 183 -- the set of finite partial functions from ω to 2 | |
| 184 -- | |
| 185 -- | |
| 186 | |
| 381 | 187 data Two : Set where |
| 379 | 188 i0 : Two |
| 189 i1 : Two | |
| 190 | |
| 381 | 191 data Three : Set where |
| 379 | 192 j0 : Three |
| 193 j1 : Three | |
| 194 j2 : Three | |
| 195 | |
| 196 open import Data.List hiding (map) | |
| 197 | |
| 198 import OPair | |
| 199 open OPair O | |
| 200 | |
| 381 | 201 record PFunc {n : Level} : Set (suc n) where |
| 379 | 202 field |
| 203 dom : Nat → Set n | |
| 204 map : (x : Nat ) → dom x → Two | |
| 205 meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q | |
| 206 | |
| 207 open PFunc | |
| 208 | |
| 381 | 209 data Findp : List Three → (x : Nat) → Set where |
| 379 | 210 v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero |
| 211 v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero | |
| 212 vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x) | |
| 213 | |
| 381 | 214 findp : List Three → (x : Nat) → Set |
| 215 findp n x = Findp n x | |
| 216 | |
| 217 find : (n : List Three ) → (x : Nat) → Findp n x → Two | |
| 218 find (j0 ∷ _) 0 v0 = i0 | |
| 219 find (j1 ∷ _) 0 v1 = i1 | |
| 220 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p | |
| 221 | |
| 222 Findp=n : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p) | |
| 223 Findp=n j0 n {x} {p} = refl | |
| 224 Findp=n j1 n {x} {p} = refl | |
| 225 Findp=n j2 n {x} {p} = refl | |
| 226 | |
| 227 findpeq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q | |
| 228 findpeq n {0} {v0} {v0} = refl | |
| 229 findpeq n {0} {v1} {v1} = refl | |
| 230 findpeq [] {Suc x} {()} | |
| 231 findpeq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (Findp=n h n) (Findp=n h n) (findpeq n {x} {p} {q}) | |
| 232 | |
| 233 3List→PFunc : List Three → PFunc | |
| 234 3List→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → findpeq fp } | |
| 235 | |
| 236 _3⊆b_ : (f g : List Three) → Bool | |
| 237 [] 3⊆b [] = true | |
| 238 [] 3⊆b (j2 ∷ g) = [] 3⊆b g | |
| 239 [] 3⊆b (_ ∷ g) = true | |
| 240 (j2 ∷ f) 3⊆b [] = f 3⊆b [] | |
| 241 (j2 ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g | |
| 242 (j0 ∷ f) 3⊆b (j0 ∷ g) = f 3⊆b g | |
| 243 (j1 ∷ f) 3⊆b (j1 ∷ g) = f 3⊆b g | |
| 244 _ 3⊆b _ = false | |
| 245 | |
| 246 _3⊆_ : (f g : List Three) → Set | |
| 247 f 3⊆ g = (f 3⊆b g) ≡ true | |
| 248 | |
| 249 _3∩_ : (f g : List Three) → List Three | |
| 250 [] 3∩ (j2 ∷ g) = j2 ∷ ([] 3∩ g) | |
| 251 [] 3∩ g = [] | |
| 252 (j2 ∷ f) 3∩ [] = j2 ∷ f 3∩ [] | |
| 253 f 3∩ [] = [] | |
| 254 (j0 ∷ f) 3∩ (j0 ∷ g) = j0 ∷ ( f 3∩ g ) | |
| 255 (j1 ∷ f) 3∩ (j1 ∷ g) = j1 ∷ ( f 3∩ g ) | |
| 256 (_ ∷ f) 3∩ (_ ∷ g) = j2 ∷ ( f 3∩ g ) | |
| 257 | |
| 258 3∩⊆f : { f g : List Three } → (f 3∩ g ) 3⊆ f | |
| 259 3∩⊆f {[]} {[]} = refl | |
| 260 3∩⊆f {[]} {j0 ∷ g} = refl | |
| 261 3∩⊆f {[]} {j1 ∷ g} = refl | |
| 262 3∩⊆f {[]} {j2 ∷ g} = 3∩⊆f {[]} {g} | |
| 263 3∩⊆f {j0 ∷ f} {[]} = refl | |
| 264 3∩⊆f {j1 ∷ f} {[]} = refl | |
| 265 3∩⊆f {j2 ∷ f} {[]} = 3∩⊆f {f} {[]} | |
| 266 3∩⊆f {j0 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} | |
| 267 3∩⊆f {j1 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} | |
| 268 3∩⊆f {j0 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} | |
| 269 3∩⊆f {j1 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} | |
| 270 3∩⊆f {j2 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g} | |
| 271 3∩⊆f {j2 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g} | |
| 272 3∩⊆f {j0 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} | |
| 273 3∩⊆f {j1 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} | |
| 274 3∩⊆f {j2 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g} | |
| 275 | |
| 276 3∩sym : { f g : List Three } → (f 3∩ g ) ≡ (g 3∩ f ) | |
| 277 3∩sym {[]} {[]} = refl | |
| 278 3∩sym {[]} {j0 ∷ g} = refl | |
| 279 3∩sym {[]} {j1 ∷ g} = refl | |
| 280 3∩sym {[]} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {[]} {g}) | |
| 281 3∩sym {j0 ∷ f} {[]} = refl | |
| 282 3∩sym {j1 ∷ f} {[]} = refl | |
| 283 3∩sym {j2 ∷ f} {[]} = cong (λ k → j2 ∷ k) (3∩sym {f} {[]}) | |
| 284 3∩sym {j0 ∷ f} {j0 ∷ g} = cong (λ k → j0 ∷ k) (3∩sym {f} {g}) | |
| 285 3∩sym {j0 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
| 286 3∩sym {j0 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
| 287 3∩sym {j1 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
| 288 3∩sym {j1 ∷ f} {j1 ∷ g} = cong (λ k → j1 ∷ k) (3∩sym {f} {g}) | |
| 289 3∩sym {j1 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
| 290 3∩sym {j2 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
| 291 3∩sym {j2 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
| 292 3∩sym {j2 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g}) | |
| 293 | |
| 294 3⊆-[] : { h : List Three } → [] 3⊆ h | |
| 295 3⊆-[] {[]} = refl | |
| 296 3⊆-[] {j0 ∷ h} = refl | |
| 297 3⊆-[] {j1 ∷ h} = refl | |
| 298 3⊆-[] {j2 ∷ h} = 3⊆-[] {h} | |
| 299 | |
| 300 3⊆trans : { f g h : List Three } → f 3⊆ g → g 3⊆ h → f 3⊆ h | |
| 301 3⊆trans {[]} {[]} {[]} f<g g<h = refl | |
| 302 3⊆trans {[]} {[]} {j0 ∷ h} f<g g<h = refl | |
| 303 3⊆trans {[]} {[]} {j1 ∷ h} f<g g<h = refl | |
| 304 3⊆trans {[]} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h | |
| 305 3⊆trans {[]} {j2 ∷ g} {[]} f<g g<h = refl | |
| 306 3⊆trans {[]} {j0 ∷ g} {j0 ∷ h} f<g g<h = refl | |
| 307 3⊆trans {[]} {j1 ∷ g} {j1 ∷ h} f<g g<h = refl | |
| 308 3⊆trans {[]} {j2 ∷ g} {j0 ∷ h} f<g g<h = refl | |
| 309 3⊆trans {[]} {j2 ∷ g} {j1 ∷ h} f<g g<h = refl | |
| 310 3⊆trans {[]} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h | |
| 311 3⊆trans {j2 ∷ f} {[]} {[]} f<g g<h = f<g | |
| 312 3⊆trans {j2 ∷ f} {[]} {j0 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) | |
| 313 3⊆trans {j2 ∷ f} {[]} {j1 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h}) | |
| 314 3⊆trans {j2 ∷ f} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h | |
| 315 3⊆trans {j0 ∷ f} {j0 ∷ g} {[]} f<g () | |
| 316 3⊆trans {j0 ∷ f} {j1 ∷ g} {[]} f<g () | |
| 317 3⊆trans {j0 ∷ f} {j2 ∷ g} {[]} () g<h | |
| 318 3⊆trans {j1 ∷ f} {j0 ∷ g} {[]} f<g () | |
| 319 3⊆trans {j1 ∷ f} {j1 ∷ g} {[]} f<g () | |
| 320 3⊆trans {j1 ∷ f} {j2 ∷ g} {[]} () g<h | |
| 321 3⊆trans {j2 ∷ f} {j2 ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h | |
| 322 3⊆trans {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 323 3⊆trans {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 324 3⊆trans {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 325 3⊆trans {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 326 3⊆trans {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 327 3⊆trans {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 328 3⊆trans {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h | |
| 379 | 329 |
| 381 | 330 3⊆∩f : { f g h : List Three } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h ) |
| 331 3⊆∩f {[]} {[]} {[]} f<g f<h = refl | |
| 332 3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)} | |
| 333 3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h} | |
| 334 3⊆∩f {j2 ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h | |
| 335 3⊆∩f {j2 ∷ f} {[]} {j0 ∷ h} f<g f<h = f<g | |
| 336 3⊆∩f {j2 ∷ f} {[]} {j1 ∷ h} f<g f<h = f<g | |
| 337 3⊆∩f {j2 ∷ f} {[]} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h | |
| 338 3⊆∩f {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 339 3⊆∩f {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 340 3⊆∩f {j2 ∷ f} {j0 ∷ g} {[]} f<g f<h = f<h | |
| 341 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 342 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 343 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 344 3⊆∩f {j2 ∷ f} {j1 ∷ g} {[]} f<g f<h = f<h | |
| 345 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 346 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 347 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 348 3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h | |
| 349 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 350 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 351 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h | |
| 352 | |
| 353 ↑app :(Nat → Two) → Nat → List Three → List Three | |
| 354 ↑app f Zero y = y | |
| 355 ↑app f (Suc x) y with f x | |
| 356 ... | i0 = ↑app f x (j0 ∷ y ) | |
| 357 ... | i1 = ↑app f x (j1 ∷ y ) | |
| 358 | |
| 359 _3↑_ : (Nat → Two) → Nat → List Three | |
| 360 f 3↑ x = ↑app f x [] | |
| 361 | |
| 382 | 362 3↑22 : (f : Nat → Two) (i j : Nat) → List Three |
| 363 3↑22 f Zero j = [] | |
| 364 3↑22 f (Suc i) j with f i | |
| 365 3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j) | |
| 366 3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j) | |
| 367 | |
| 368 3↑2 : (Nat → Two) → Nat → List Three | |
| 369 3↑2 f i = 3↑22 f i 0 | |
| 381 | 370 |
| 382 | 371 lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t)) |
| 372 lemma10 s t eq = eq | |
| 373 lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t)) | |
| 374 lemma11 s t eq = eq | |
| 375 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t)) | |
| 376 lemma12 s t eq = eq | |
| 377 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t)) | |
| 378 lemma13 s t eq = eq | |
| 379 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t)) | |
| 380 lemma14 s t eq = eq | |
| 381 | 381 |
| 382 | 382 3↑<2 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x) 3⊆ (3↑2 f y) |
| 383 3↑<2 {f} {x} {y} x<y = lemma x 0 y x<y (3↑22 f x 0) (3↑22 f y 0) where | |
| 384 lemma : (i j y : Nat) → i ≤ y → (s t : List Three) → s 3⊆ t | |
| 385 lemma Zero j y z≤n [] [] = refl | |
| 386 lemma Zero j y z≤n [] (x ∷ t) = 3⊆-[] {x ∷ t} | |
| 387 lemma Zero j y z≤n (x ∷ s) [] = {!!} | |
| 388 lemma Zero j y z≤n (j0 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t | |
| 389 lemma Zero j y z≤n (j0 ∷ s) (j1 ∷ t) = {!!} | |
| 390 lemma Zero j y z≤n (j0 ∷ s) (j2 ∷ t) = {!!} | |
| 391 lemma Zero j y z≤n (j1 ∷ s) (j0 ∷ t) = {!!} | |
| 392 lemma Zero j y z≤n (j1 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t | |
| 393 lemma Zero j y z≤n (j1 ∷ s) (j2 ∷ t) = {!!} | |
| 394 lemma Zero j y z≤n (j2 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t | |
| 395 lemma Zero j y z≤n (j2 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t | |
| 396 lemma Zero j y z≤n (j2 ∷ s) (j2 ∷ t) = lemma Zero j y z≤n s t | |
| 397 lemma (Suc i) j (Suc y) (s≤s i<y) [] t = 3⊆-[] {t} | |
| 398 lemma (Suc i) j (Suc y) (s≤s i<y) (x ∷ s) [] = {!!} | |
| 399 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j0 ∷ t) = {!!} | |
| 400 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j1 ∷ t) = {!!} | |
| 401 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j2 ∷ t) = {!!} | |
| 402 lemma (Suc i) j (Suc y) (s≤s i<y) (j1 ∷ s) (x1 ∷ t) = {!!} | |
| 403 lemma (Suc i) j (Suc y) (s≤s i<y) (j2 ∷ s) (x1 ∷ t) = {!!} | |
| 404 -- with lemma i j y i<y s t | |
| 381 | 405 |
| 406 | |
| 407 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y) | |
| 408 3↑< {f} {x} {y} x<y = {!!} where | |
| 409 lemma0 : (i : Nat) → (y : List Three ) → ( ↑app f (Suc i) y ≡ ↑app f i (j0 ∷ y)) ∨ ( ↑app f (Suc i) y ≡ ↑app f i (j1 ∷ y)) | |
| 410 lemma0 i y with f i | |
| 411 lemma0 i y | i0 = case1 refl | |
| 412 lemma0 i y | i1 = case2 refl | |
| 413 lemma : (i : Nat) → (f 3↑ i) 3⊆ (f 3↑ Suc i) | |
| 414 lemma i with f i | |
| 415 lemma i | i0 = {!!} | |
| 416 lemma i | i1 = {!!} | |
| 417 | |
| 418 record Finite3 (p : List Three ) : Set where | |
| 419 field | |
| 420 3-max : Nat | |
| 421 3-func : Nat → Two | |
| 422 3-p⊆f : p 3⊆ (3-func 3↑ 3-max) | |
| 423 3-f⊆p : (3-func 3↑ 3-max) 3⊆ p | |
| 424 | |
| 425 Finite3b : (p : List Three ) → Bool | |
| 426 Finite3b [] = true | |
| 427 Finite3b (j0 ∷ f) = Finite3b f | |
| 428 Finite3b (j1 ∷ f) = Finite3b f | |
| 429 Finite3b (j2 ∷ f) = false | |
| 430 | |
| 431 finite3cov : (p : List Three ) → List Three | |
| 432 finite3cov [] = [] | |
| 433 finite3cov (j0 ∷ x) = j0 ∷ finite3cov x | |
| 434 finite3cov (j1 ∷ x) = j1 ∷ finite3cov x | |
| 435 finite3cov (j2 ∷ x) = j0 ∷ finite3cov x | |
| 436 | |
| 437 Dense-3 : F-Dense (List Three) (λ x → One) _3⊆_ _3∩_ | |
| 438 Dense-3 = record { | |
| 439 dense = λ x → Finite3b x ≡ true | |
| 440 ; d⊆P = OneObj | |
| 441 ; dense-f = λ x → finite3cov x | |
| 442 ; dense-d = λ {p} d → lemma1 p | |
| 443 ; dense-p = λ {p} d → lemma2 p | |
| 444 } where | |
| 445 lemma1 : (p : List Three ) → Finite3b (finite3cov p) ≡ true | |
| 446 lemma1 [] = refl | |
| 447 lemma1 (j0 ∷ p) = lemma1 p | |
| 448 lemma1 (j1 ∷ p) = lemma1 p | |
| 449 lemma1 (j2 ∷ p) = lemma1 p | |
| 450 lemma2 : (p : List Three) → p 3⊆ finite3cov p | |
| 451 lemma2 [] = refl | |
| 452 lemma2 (j0 ∷ p) = lemma2 p | |
| 453 lemma2 (j1 ∷ p) = lemma2 p | |
| 454 lemma2 (j2 ∷ p) = lemma2 p | |
| 455 | |
| 456 record 3Gf (f : Nat → Two) (p : List Three ) : Set where | |
| 457 field | |
| 458 3gn : Nat | |
| 459 3f<n : (f 3↑ 3gn) 3⊆ p | |
| 460 | |
| 461 open 3Gf | |
| 462 | |
| 463 min = Data.Nat._⊓_ | |
| 464 -- m≤m⊔n = Data.Nat._⊔_ | |
| 465 open import Data.Nat.Properties | |
| 466 | |
| 467 3GF : {n : Level } → (Nat → Two ) → F-Filter (List Three) (λ x → One) _3⊆_ _3∩_ | |
| 468 3GF {n} f = record { | |
| 469 filter = λ p → 3Gf f p | |
| 470 ; f⊆P = OneObj | |
| 471 ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q | |
| 472 ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq } | |
| 473 } where | |
| 474 lemma1 : (p q : List Three ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q | |
| 475 lemma1 p q fp p⊆q = record { 3gn = 3gn fp ; 3f<n = 3⊆trans {f 3↑ 3gn fp } {p} {q} (3f<n fp) p⊆q } | |
| 476 lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (f 3↑ min (3gn fp) (3gn fq)) 3⊆ (p 3∩ q) | |
| 477 lemma2 p q fp fq = 3⊆∩f {f 3↑ min (3gn fp) (3gn fq) } {p} {q} (3⊆trans {bb} {f 3↑ (3gn fp)} {p} (3↑< {_} {bm} (m⊓n≤m _ _ )) (3f<n fp)) | |
| 478 (3⊆trans {bb} {f 3↑ (3gn fq)} {q} (3↑< {_} {bm} (m⊓n≤n _ _ )) (3f<n fq)) where | |
| 479 bb = f 3↑ min (3gn fp) (3gn fq) | |
| 480 bm = min (3gn fp) (3gn fq) | |
| 481 | |
| 482 record _f⊆_ {n : Level } (f g : PFunc {n} ) : Set (suc n) where | |
| 379 | 483 field |
| 484 extend : {x : Nat} → (fr : dom f x ) → dom g x | |
| 485 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr) | |
| 486 | |
| 487 open _f⊆_ | |
| 488 | |
| 381 | 489 _f∩_ : {n : Level} → (f g : PFunc {n} ) → PFunc {n} |
| 379 | 490 f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr) |
| 491 ; map = λ x p → map f x (proj1 p) ; meq = meq f } | |
|
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
492 |
| 381 | 493 _↑_ : {n : Level} → (Nat → Two) → Nat → PFunc {n} |
| 494 _↑_ {n} f i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl } | |
|
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
495 |
| 381 | 496 record Gf {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where |
|
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
497 field |
|
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
498 gn : Nat |
|
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
499 f<n : (f ↑ gn) f⊆ p |
|
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
500 |
| 381 | 501 record FiniteF {n : Level} (p : PFunc {n} ) : Set (suc n) where |
| 379 | 502 field |
| 503 f-max : Nat | |
| 504 f-func : Nat → Two | |
| 505 f-p⊆f : p f⊆ (f-func ↑ f-max) | |
| 506 f-f⊆p : (f-func ↑ f-max) f⊆ p | |
| 507 | |
| 508 open FiniteF | |
| 509 | |
| 381 | 510 -- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_ |
| 511 -- Dense-Gf = record { | |
| 512 -- dense = λ x → FiniteF x | |
| 513 -- ; d⊆P = lift OneObj | |
| 514 -- ; dense-f = λ x → record { dom = {!!} ; map = {!!} } | |
| 515 -- ; dense-d = λ {p} d → {!!} | |
| 516 -- ; dense-p = λ {p} d → {!!} | |
| 517 -- } | |
| 379 | 518 |
|
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
519 open Gf |
|
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
520 |
| 381 | 521 GF : {n : Level } → (Nat → Two ) → F-Filter (PFunc {n}) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_ |
| 522 GF {n} f = record { | |
| 372 | 523 filter = λ p → Gf f p |
| 374 | 524 ; f⊆P = lift OneObj |
| 525 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } | |
| 526 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } | |
| 372 | 527 } where |
| 381 | 528 f1 : {p q : PFunc {n} } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q |
| 379 | 529 f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q (extend (f<n fp ) x<g) ; feq = λ {x} {fr} → lemma {x} {fr} } where |
| 530 lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr)) | |
| 531 lemma {x} {fr} = begin | |
| 532 map (f ↑ gn fp) x fr | |
| 533 ≡⟨ feq (f<n fp ) ⟩ | |
| 534 map p x (extend (f<n fp) fr) | |
| 535 ≡⟨ feq p⊆q ⟩ | |
| 536 map q x (extend p⊆q (extend (f<n fp) fr)) | |
| 537 ∎ where open ≡-Reasoning | |
| 381 | 538 f2 : {p q : PFunc {n} } → (fp : Gf {n} f p ) → (fq : Gf {n} f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) |
| 379 | 539 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where |
| 381 | 540 fmin : PFunc {n} |
| 379 | 541 fmin = f ↑ (min (gn fp) (gn fq)) |
| 542 lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr | |
| 543 lemma1 {x} x<g fr gr = begin | |
| 544 map p x fr | |
| 545 ≡⟨ meq p ⟩ | |
| 546 map p x (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))) | |
| 547 ≡⟨ sym (feq (f<n fp)) ⟩ | |
| 548 map (f ↑ (min (gn fp) (gn fq))) x x<g | |
| 549 ≡⟨ feq (f<n fq) ⟩ | |
| 550 map q x (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))) | |
| 551 ≡⟨ meq q ⟩ | |
| 552 map q x gr | |
| 553 ∎ where open ≡-Reasoning | |
| 554 lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) x | |
| 555 lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ; | |
| 556 proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }} | |
| 557 f∩→⊆ : (p q : PFunc ) → (p f∩ q ) f⊆ q | |
| 558 f∩→⊆ p q = record { | |
| 559 extend = λ {x} pq → proj1 (proj2 pq) | |
| 560 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) | |
| 561 } | |
| 562 lemma3 : {x : Nat} → ( fr : Lift n (x ≤ min (gn fp) (gn fq))) → map (f ↑ min (gn fp) (gn fq)) x fr ≡ map (p f∩ q) x (lemma2 fr) | |
| 563 lemma3 {x} fr = | |
| 564 map (f ↑ min (gn fp) (gn fq)) x fr | |
| 565 ≡⟨ feq (f<n fq) ⟩ | |
| 566 map q x (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) )) | |
| 567 ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩ | |
| 568 map (p f∩ q) x (lemma2 fr) | |
| 569 ∎ where open ≡-Reasoning | |
| 570 | |
| 370 | 571 |
| 363 | 572 ODSuc : (y : HOD) → infinite ∋ y → HOD |
| 573 ODSuc y lt = Union (y , (y , y)) | |
| 574 | |
| 366 | 575 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where |
| 576 hφ : Hω2 0 o∅ | |
| 577 h0 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 578 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) | |
| 579 h1 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 580 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) | |
| 581 he : {i : Nat} {x : Ordinal } → Hω2 i x → | |
| 582 Hω2 (Suc i) x | |
| 583 | |
| 584 record Hω2r (x : Ordinal) : Set n where | |
| 585 field | |
| 586 count : Nat | |
| 587 hω2 : Hω2 count x | |
| 588 | |
| 589 open Hω2r | |
| 363 | 590 |
| 591 HODω2 : HOD | |
| 366 | 592 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where |
| 365 | 593 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ |
| 594 ω<next = ω<next-o∅ ho< | |
| 366 | 595 lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x |
| 596 lemma = {!!} | |
| 597 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ | |
| 598 odmax0 {y} r with hω2 r | |
| 599 ... | hφ = x<nx | |
| 600 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x}) | |
| 601 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x}) | |
| 602 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx | |
| 363 | 603 |
| 370 | 604 ω→2 : HOD |
| 379 | 605 ω→2 = Replace (Power infinite) (λ p → Replace infinite (λ x → < x , repl p x > )) where |
| 370 | 606 repl : HOD → HOD → HOD |
| 607 repl p x with ODC.∋-p O p x | |
| 608 ... | yes _ = nat→ω 1 | |
| 609 ... | no _ = nat→ω 0 | |
| 368 | 610 |
| 370 | 611 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where |
| 612 -- field | |
| 613 -- n : HOD | |
| 614 -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n | |
| 615 | |
| 372 | 616 -- Gf : {f : HOD} → ω→2 ∋ f → HOD |
| 617 -- Gf {f} lt = Select HODω2 (λ x H∋x → {!!} ) | |
| 368 | 618 |
| 619 G : (Nat → Two) → Filter HODω2 | |
| 620 G f = record { | |
| 365 | 621 filter = {!!} |
| 622 ; f⊆PL = {!!} | |
| 623 ; filter1 = {!!} | |
| 624 ; filter2 = {!!} | |
| 625 } where | |
| 626 filter0 : HOD | |
| 627 filter0 = {!!} | |
| 628 f⊆PL1 : filter0 ⊆ Power HODω2 | |
| 629 f⊆PL1 = {!!} | |
| 630 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q | |
| 631 filter11 = {!!} | |
| 632 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) | |
| 633 filter12 = {!!} | |
| 634 | |
| 363 | 635 -- the set of finite partial functions from ω to 2 |
| 636 | |
| 637 Hω2f : Set (suc n) | |
| 638 Hω2f = (Nat → Set n) → Two | |
| 639 | |
| 640 Hω2f→Hω2 : Hω2f → HOD | |
| 381 | 641 Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } |
| 363 | 642 |
| 643 |