annotate filter.agda @ 268:7b4a66710cdd

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Sep 2019 21:22:07 +0900
parents e469de3ae7cc
children 30e419a2be24
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
2 open import Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
3 module filter {n : Level } (O : Ordinals {n}) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
4
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import zf
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
6 open import logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
7 import OD
193
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
8
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Empty
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Binary.Core
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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⊔_ )
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
16
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
17 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
18 open OD O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
19 open OD.OD
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
21 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
22 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
23 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
24
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
25 _∩_ : ( A B : OD ) → OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
26 A ∩ B = record { def = λ x → def A x ∧ def B x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
28 _∪_ : ( A B : OD ) → OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
29 A ∪ B = Union (A , B)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
30
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
31 record Filter ( L : OD ) : 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
32 field
268
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
33 F1 : { p q : OD } → L ∋ p → ({ x : OD} → _⊆_ q p {x} ) → L ∋ q
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
34 F2 : { p q : OD } → L ∋ p → L ∋ q → L ∋ (p ∩ q)
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
35
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
36 open Filter
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
37
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
38 proper-filter : {L : OD} → Filter L → Set n
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
39 proper-filter {L} P = ¬ ( L ∋ od∅ )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
41 prime-filter : {L : OD} → Filter L → {p q : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
42 prime-filter {L} P {p} {q} = L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
44 ultra-filter : {L : OD} → Filter L → {p : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
45 ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
47 postulate
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
48 dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r )
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
49
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
50 filter-lemma1 : {L : OD} → (P : Filter L) → {p q : OD } → ( (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
51 filter-lemma1 {L} P {p} {q} u lt with u p | u q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
52 filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
53 filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
54 filter-lemma1 {L} P {p} {q} u lt | case2 x | case1 y = case2 y
268
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
55 filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim (lemma (record { proj1 = x ; proj2 = y })) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
56 lemma : ¬ ( ¬ ( L ∋ p ) ) ∧ ( ¬ ( L ∋ q ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
57 lemma = {!!}
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
58
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
59 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
60 generated-filter {L} P p = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
61 F1 = {!!} ; F2 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
62 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
63
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
64 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
66 infinite = ZF.infinite OD→ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
67
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
68 Hω2 : Filter (Power (Power infinite))
268
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
69 Hω2 = record { F1 = {!!} ; F2 = {!!} }
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
70