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

comparison filter.agda @ 370:1425104bb5d8

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, 19 Jul 2020 12:26:17 +0900
parents 30de2d9b93c1
children e75402b1f7d4
comparison
equal deleted inserted replaced
369:17adeeee0c2a 370:1425104bb5d8
150 -- 150 --
151 151
152 import OPair 152 import OPair
153 open OPair O 153 open OPair O
154 154
155 data Two : Set n where
156 i0 : Two
157 i1 : Two
158
159 record PFunc : Set (suc n) where
160 field
161 restrict : Nat → Set n
162 map : (x : Nat ) → restrict x → Two
163
164 open PFunc
165
166 record _f⊆_ (f g : PFunc) : Set (suc n) where
167 field
168 feq : (x : Nat) → (fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr
169
170 full-func : Set n
171 full-func = Nat → Two
172
173 full→PF : (Nat → Two) → PFunc
174 full→PF f = record { restrict = λ x → One ; map = λ x _ → f x }
175
176 _↑_ : (Nat → Two) → Nat → PFunc
177 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
178
179 record F-Filter (PL : Set n) (L : PL ) ( _⊆_ : PL → PL → Set n) ( _∋_ : PL → PL → Set n) : Set (suc n) where
180 field
181 filter : PL
182 f⊆PL : filter ⊆ L
183 filter1 : { p q : PL } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
184 filter2 : { p q : PL } → filter ∋ p → filter ∋ q → (filter ∋ p) ∧ (filter ∋ q)
185
155 ODSuc : (y : HOD) → infinite ∋ y → HOD 186 ODSuc : (y : HOD) → infinite ∋ y → HOD
156 ODSuc y lt = Union (y , (y , y)) 187 ODSuc y lt = Union (y , (y , y))
157 188
158 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where 189 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where
159 hφ : Hω2 0 o∅ 190 hφ : Hω2 0 o∅
182 ... | hφ = x<nx 213 ... | hφ = x<nx
183 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x}) 214 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
184 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x}) 215 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
185 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx 216 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
186 217
187 data Two : Set n where
188 i0 : Two
189 i1 : Two
190
191 record ω2r : Set n where
192 field
193 func2 : Nat → Two
194 ω2 : {!!}
195
196 ω→2 : HOD 218 ω→2 : HOD
197 ω→2 = Replace infinite (λ x → < x , {!!} > ) 219 ω→2 = Replace (Power infinite) (λ p p⊆i → Replace infinite (λ x i∋x → < x , repl p x > )) where
220 repl : HOD → HOD → HOD
221 repl p x with ODC.∋-p O p x
222 ... | yes _ = nat→ω 1
223 ... | no _ = nat→ω 0
224
225 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
226 -- field
227 -- n : HOD
228 -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
229
230 Gf : {f : HOD} → ω→2 ∋ f → HOD
231 Gf {f} lt = Select HODω2 (λ x H∋x → {!!} )
198 232
199 G : (Nat → Two) → Filter HODω2 233 G : (Nat → Two) → Filter HODω2
200 G f = record { 234 G f = record {
201 filter = {!!} 235 filter = {!!}
202 ; f⊆PL = {!!} 236 ; f⊆PL = {!!}