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

comparison filter.agda @ 381:d2cb5278e46d

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 Tue, 21 Jul 2020 14:34:27 +0900
parents 0a116938a564
children c3a0fb13e267
comparison
equal deleted inserted replaced
380:0a116938a564 381:d2cb5278e46d
182 ------- 182 -------
183 -- the set of finite partial functions from ω to 2 183 -- the set of finite partial functions from ω to 2
184 -- 184 --
185 -- 185 --
186 186
187 data Two : Set n where 187 data Two : Set where
188 i0 : Two 188 i0 : Two
189 i1 : Two 189 i1 : Two
190 190
191 data Three : Set n where 191 data Three : Set where
192 j0 : Three 192 j0 : Three
193 j1 : Three 193 j1 : Three
194 j2 : Three 194 j2 : Three
195 195
196 open import Data.List hiding (map) 196 open import Data.List hiding (map)
197 197
198 import OPair 198 import OPair
199 open OPair O 199 open OPair O
200 200
201 record PFunc : Set (suc n) where 201 record PFunc {n : Level} : Set (suc n) where
202 field 202 field
203 dom : Nat → Set n 203 dom : Nat → Set n
204 map : (x : Nat ) → dom x → Two 204 map : (x : Nat ) → dom x → Two
205 meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q 205 meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q
206 206
207 open PFunc 207 open PFunc
208 208
209 data Findp : List Three → (x : Nat) → Set n where 209 data Findp : List Three → (x : Nat) → Set where
210 v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero 210 v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero
211 v1 : {n : List Three} → Findp ( j1 ∷ 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) 212 vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x)
213 213
214 FPFunc→PFunc : List Three → PFunc 214 findp : List Three → (x : Nat) → Set
215 FPFunc→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → feq fp } where 215 findp n x = Findp n x
216 findp : List Three → (x : Nat) → Set n 216
217 findp n x = Findp n x 217 find : (n : List Three ) → (x : Nat) → Findp n x → Two
218 find : (n : List Three ) → (x : Nat) → Findp n x → Two 218 find (j0 ∷ _) 0 v0 = i0
219 find (j0 ∷ _) 0 v0 = i0 219 find (j1 ∷ _) 0 v1 = i1
220 find (j1 ∷ _) 0 v1 = i1 220 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p
221 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p 221
222 lemma : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p) 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 lemma j0 n {x} {p} = refl 223 Findp=n j0 n {x} {p} = refl
224 lemma j1 n {x} {p} = refl 224 Findp=n j1 n {x} {p} = refl
225 lemma j2 n {x} {p} = refl 225 Findp=n j2 n {x} {p} = refl
226 feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q 226
227 feq n {0} {v0} {v0} = refl 227 findpeq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q
228 feq n {0} {v1} {v1} = refl 228 findpeq n {0} {v0} {v0} = refl
229 feq [] {Suc x} {()} 229 findpeq n {0} {v1} {v1} = refl
230 feq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (lemma h n) (lemma h n) (feq n {x} {p} {q}) 230 findpeq [] {Suc x} {()}
231 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 record _f⊆_ (f g : PFunc) : Set (suc n) where 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
329
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
362 listn : Nat → List Nat
363 listn 0 = []
364 listn (Suc n) = n ∷ listn n
365
366 rev : {A : Set} → List A → List A
367 rev {A} x = rev1 x [] where
368 rev1 : List A → List A → List A
369 rev1 [] y = y
370 rev1 (h ∷ x) y = rev1 x (h ∷ y)
371
372 Lmap : {A B : Set} → (A → B ) → List A → List B
373 Lmap f [] = []
374 Lmap f (h ∷ t) = f h ∷ Lmap f t
375
376 3↑1 : (Nat → Two) → Nat → List Three
377 3↑1 f i with f i
378 ... | i0 = Lmap (λ x → j0) (rev ( listn i ))
379 ... | i1 = Lmap (λ x → j1) (rev ( listn i ))
380
381 3↑<1 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑1 f x) 3⊆ (3↑1 f y)
382 3↑<1 {f} {x} {y} x<y = lemma (rev ( listn x )) where
383 lemma : (z : List Nat ) → {!!}
384 lemma = {!!}
385
386
387 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y)
388 3↑< {f} {x} {y} x<y = {!!} where
389 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))
390 lemma0 i y with f i
391 lemma0 i y | i0 = case1 refl
392 lemma0 i y | i1 = case2 refl
393 lemma : (i : Nat) → (f 3↑ i) 3⊆ (f 3↑ Suc i)
394 lemma i with f i
395 lemma i | i0 = {!!}
396 lemma i | i1 = {!!}
397
398 record Finite3 (p : List Three ) : Set where
399 field
400 3-max : Nat
401 3-func : Nat → Two
402 3-p⊆f : p 3⊆ (3-func 3↑ 3-max)
403 3-f⊆p : (3-func 3↑ 3-max) 3⊆ p
404
405 Finite3b : (p : List Three ) → Bool
406 Finite3b [] = true
407 Finite3b (j0 ∷ f) = Finite3b f
408 Finite3b (j1 ∷ f) = Finite3b f
409 Finite3b (j2 ∷ f) = false
410
411 finite3cov : (p : List Three ) → List Three
412 finite3cov [] = []
413 finite3cov (j0 ∷ x) = j0 ∷ finite3cov x
414 finite3cov (j1 ∷ x) = j1 ∷ finite3cov x
415 finite3cov (j2 ∷ x) = j0 ∷ finite3cov x
416
417 Dense-3 : F-Dense (List Three) (λ x → One) _3⊆_ _3∩_
418 Dense-3 = record {
419 dense = λ x → Finite3b x ≡ true
420 ; d⊆P = OneObj
421 ; dense-f = λ x → finite3cov x
422 ; dense-d = λ {p} d → lemma1 p
423 ; dense-p = λ {p} d → lemma2 p
424 } where
425 lemma1 : (p : List Three ) → Finite3b (finite3cov p) ≡ true
426 lemma1 [] = refl
427 lemma1 (j0 ∷ p) = lemma1 p
428 lemma1 (j1 ∷ p) = lemma1 p
429 lemma1 (j2 ∷ p) = lemma1 p
430 lemma2 : (p : List Three) → p 3⊆ finite3cov p
431 lemma2 [] = refl
432 lemma2 (j0 ∷ p) = lemma2 p
433 lemma2 (j1 ∷ p) = lemma2 p
434 lemma2 (j2 ∷ p) = lemma2 p
435
436 record 3Gf (f : Nat → Two) (p : List Three ) : Set where
437 field
438 3gn : Nat
439 3f<n : (f 3↑ 3gn) 3⊆ p
440
441 open 3Gf
442
443 min = Data.Nat._⊓_
444 -- m≤m⊔n = Data.Nat._⊔_
445 open import Data.Nat.Properties
446
447 3GF : {n : Level } → (Nat → Two ) → F-Filter (List Three) (λ x → One) _3⊆_ _3∩_
448 3GF {n} f = record {
449 filter = λ p → 3Gf f p
450 ; f⊆P = OneObj
451 ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q
452 ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
453 } where
454 lemma1 : (p q : List Three ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q
455 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 }
456 lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (f 3↑ min (3gn fp) (3gn fq)) 3⊆ (p 3∩ q)
457 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))
458 (3⊆trans {bb} {f 3↑ (3gn fq)} {q} (3↑< {_} {bm} (m⊓n≤n _ _ )) (3f<n fq)) where
459 bb = f 3↑ min (3gn fp) (3gn fq)
460 bm = min (3gn fp) (3gn fq)
461
462 record _f⊆_ {n : Level } (f g : PFunc {n} ) : Set (suc n) where
233 field 463 field
234 extend : {x : Nat} → (fr : dom f x ) → dom g x 464 extend : {x : Nat} → (fr : dom f x ) → dom g x
235 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr) 465 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr)
236 466
237 open _f⊆_ 467 open _f⊆_
238 468
239 min = Data.Nat._⊓_ 469 _f∩_ : {n : Level} → (f g : PFunc {n} ) → PFunc {n}
240 -- m≤m⊔n = Data.Nat._⊔_
241 open import Data.Nat.Properties
242
243 _f∩_ : (f g : PFunc) → PFunc
244 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) 470 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)
245 ; map = λ x p → map f x (proj1 p) ; meq = meq f } 471 ; map = λ x p → map f x (proj1 p) ; meq = meq f }
246 472
247 _↑_ : (Nat → Two) → Nat → PFunc 473 _↑_ : {n : Level} → (Nat → Two) → Nat → PFunc {n}
248 f ↑ i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl } 474 _↑_ {n} f i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl }
249 475
250 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where 476 record Gf {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where
251 field 477 field
252 gn : Nat 478 gn : Nat
253 f<n : (f ↑ gn) f⊆ p 479 f<n : (f ↑ gn) f⊆ p
254 480
255 record FiniteF (p : PFunc ) : Set (suc n) where 481 record FiniteF {n : Level} (p : PFunc {n} ) : Set (suc n) where
256 field 482 field
257 f-max : Nat 483 f-max : Nat
258 f-func : Nat → Two 484 f-func : Nat → Two
259 f-p⊆f : p f⊆ (f-func ↑ f-max) 485 f-p⊆f : p f⊆ (f-func ↑ f-max)
260 f-f⊆p : (f-func ↑ f-max) f⊆ p 486 f-f⊆p : (f-func ↑ f-max) f⊆ p
261 487
262 open FiniteF 488 open FiniteF
263 489
264 Dense-Gf : F-Dense PFunc (λ x → Lift (suc n) One) _f⊆_ _f∩_ 490 -- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_
265 Dense-Gf = record { 491 -- Dense-Gf = record {
266 dense = λ x → FiniteF x 492 -- dense = λ x → FiniteF x
267 ; d⊆P = lift OneObj 493 -- ; d⊆P = lift OneObj
268 ; dense-f = λ x → record { dom = {!!} ; map = {!!} } 494 -- ; dense-f = λ x → record { dom = {!!} ; map = {!!} }
269 ; dense-d = λ {p} d → {!!} 495 -- ; dense-d = λ {p} d → {!!}
270 ; dense-p = λ {p} d → {!!} 496 -- ; dense-p = λ {p} d → {!!}
271 } 497 -- }
272 498
273 open Gf 499 open Gf
274 500
275 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_ 501 GF : {n : Level } → (Nat → Two ) → F-Filter (PFunc {n}) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_
276 GF f = record { 502 GF {n} f = record {
277 filter = λ p → Gf f p 503 filter = λ p → Gf f p
278 ; f⊆P = lift OneObj 504 ; f⊆P = lift OneObj
279 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } 505 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
280 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } 506 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq }
281 } where 507 } where
282 f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q 508 f1 : {p q : PFunc {n} } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q
283 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 509 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
284 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)) 510 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))
285 lemma {x} {fr} = begin 511 lemma {x} {fr} = begin
286 map (f ↑ gn fp) x fr 512 map (f ↑ gn fp) x fr
287 ≡⟨ feq (f<n fp ) ⟩ 513 ≡⟨ feq (f<n fp ) ⟩
288 map p x (extend (f<n fp) fr) 514 map p x (extend (f<n fp) fr)
289 ≡⟨ feq p⊆q ⟩ 515 ≡⟨ feq p⊆q ⟩
290 map q x (extend p⊆q (extend (f<n fp) fr)) 516 map q x (extend p⊆q (extend (f<n fp) fr))
291 ∎ where open ≡-Reasoning 517 ∎ where open ≡-Reasoning
292 f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) 518 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)
293 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where 519 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
520 fmin : PFunc {n}
294 fmin = f ↑ (min (gn fp) (gn fq)) 521 fmin = f ↑ (min (gn fp) (gn fq))
295 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 522 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
296 lemma1 {x} x<g fr gr = begin 523 lemma1 {x} x<g fr gr = begin
297 map p x fr 524 map p x fr
298 ≡⟨ meq p ⟩ 525 ≡⟨ meq p ⟩
389 616
390 Hω2f : Set (suc n) 617 Hω2f : Set (suc n)
391 Hω2f = (Nat → Set n) → Two 618 Hω2f = (Nat → Set n) → Two
392 619
393 Hω2f→Hω2 : Hω2f → HOD 620 Hω2f→Hω2 : Hω2f → HOD
394 Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } 621 Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
395 622
396 623