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

comparison filter.agda @ 372:8c3b59f583f2

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 19:14:12 +0900
parents e75402b1f7d4
children b4a247f9d940
comparison
equal deleted inserted replaced
371:e75402b1f7d4 372:8c3b59f583f2
166 record _f⊆_ (f g : PFunc) : Set (suc n) where 166 record _f⊆_ (f g : PFunc) : Set (suc n) where
167 field 167 field
168 extend : (x : Nat) → (fr : restrict f x ) → restrict g x 168 extend : (x : Nat) → (fr : restrict f x ) → restrict g x
169 feq : (x : Nat) → (fr : restrict f x ) → map f x fr ≡ map g x (extend x fr) 169 feq : (x : Nat) → (fr : restrict f x ) → map f x fr ≡ map g x (extend x fr)
170 170
171 record _f∩_ (f g : PFunc) : Set (suc n) where 171 open _f⊆_
172 field 172
173 pf : PFunc 173 _f∩_ : (f g : PFunc) → PFunc
174 f< : f f⊆ pf 174 f f∩ g = record { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
175 g< : g f⊆ pf 175 ; map = λ x p → map f x (proj1 p) }
176
177 full-func : Set n
178 full-func = Nat → Two
179
180 full→PF : (Nat → Two) → PFunc
181 full→PF f = record { restrict = λ x → One ; map = λ x _ → f x }
182 176
183 _↑_ : (Nat → Two) → Nat → PFunc 177 _↑_ : (Nat → Two) → Nat → PFunc
184 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x } 178 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
185 179
186 record gf-filter (f : Nat → Two) (p : PFunc ) : Set (suc n) where 180 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
187 field 181 field
188 gn : Nat 182 gn : Nat
189 f<n : p f⊆ (f ↑ gn) 183 f<n : p f⊆ (f ↑ gn)
184
185 open Gf
190 186
191 record F-Filter (L : Set (suc n)) (PL : (L → Set (suc n)) → Set n) ( _⊆_ : L → L → Set (suc n)) (_∩_ : L → L → L ) : Set (suc (suc n)) where 187 record F-Filter (L : Set (suc n)) (PL : (L → Set (suc n)) → Set n) ( _⊆_ : L → L → Set (suc n)) (_∩_ : L → L → L ) : Set (suc (suc n)) where
192 field 188 field
193 filter : L → Set (suc n) 189 filter : L → Set (suc n)
194 f⊆P : PL filter 190 f⊆P : PL filter
195 filter1 : { p q : L } → filter p → p ⊆ q → filter q 191 filter1 : { p q : L } → filter p → p ⊆ q → filter q
196 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q) 192 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q)
197 193
198 GF : (Nat → Two ) → F-Filter PFunc (λ x → One) _f⊆_ {!!} 194 GF : (Nat → Two ) → F-Filter PFunc (λ x → One) _f⊆_ _f∩_
199 GF f = record { 195 GF f = record {
200 filter = λ p → gf-filter f p 196 filter = λ p → Gf f p
201 ; f⊆P = OneObj 197 ; f⊆P = OneObj
202 ; filter1 = λ {p} {q} fp p⊆q → record { gn = {!!} ; f<n = {!!} } 198 ; filter1 = λ {p} {q} fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
203 ; filter2 = λ {p} {q} fp fq → record { gn = {!!} ; f<n = {!!} } 199 ; filter2 = λ {p} {q} fp fq → record { gn = {!!} ; f<n = {!!} }
204 } 200 } where
201 f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → q f⊆ (f ↑ gn fp)
202 f1 {p} {q} fp p⊆q = record { extend = λ x fr → extend (f<n fp) x {!!} ; feq = λ x fr → {!!} } where
203 f2 : (x : Nat) → x ≤ gn fp
204 f2 x = ? -- extend (f<n fp) x ?
205 205
206 ODSuc : (y : HOD) → infinite ∋ y → HOD 206 ODSuc : (y : HOD) → infinite ∋ y → HOD
207 ODSuc y lt = Union (y , (y , y)) 207 ODSuc y lt = Union (y , (y , y))
208 208
209 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where 209 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where
245 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where 245 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
246 -- field 246 -- field
247 -- n : HOD 247 -- n : HOD
248 -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n 248 -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
249 249
250 Gf : {f : HOD} → ω→2 ∋ f → HOD 250 -- Gf : {f : HOD} → ω→2 ∋ f → HOD
251 Gf {f} lt = Select HODω2 (λ x H∋x → {!!} ) 251 -- Gf {f} lt = Select HODω2 (λ x H∋x → {!!} )
252 252
253 G : (Nat → Two) → Filter HODω2 253 G : (Nat → Two) → Filter HODω2
254 G f = record { 254 G f = record {
255 filter = {!!} 255 filter = {!!}
256 ; f⊆PL = {!!} 256 ; f⊆PL = {!!}