|
190
|
1 open import Level
|
|
|
2 module filter where
|
|
|
3
|
|
|
4 open import zf
|
|
|
5 open import ordinal
|
|
|
6 open import OD
|
|
|
7 open import Relation.Nullary
|
|
|
8 open import Relation.Binary
|
|
|
9 open import Data.Empty
|
|
|
10 open import Relation.Binary
|
|
|
11 open import Relation.Binary.Core
|
|
|
12 open import Relation.Binary.PropositionalEquality
|
|
|
13
|
|
|
14 record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where
|
|
|
15 field
|
|
|
16 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
|
|
|
17 G : OD {suc n}
|
|
|
18 G∋1 : G ∋ max
|
|
|
19 Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ max
|
|
|
20 Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q
|
|
|
21 Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
|
|
|
22 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r )))
|
|
|
23
|
|
|
24 dense : {n : Level} → Set (suc (suc n))
|
|
|
25 dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q ))
|
|
|
26
|
|
|
27 open OD.OD
|
|
|
28
|
|
|
29 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
|
|
|
30
|
|
|
31 Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n}
|
|
|
32 Pred {n} dom = record {
|
|
|
33 def = λ x → def dom x → Set n
|
|
|
34 }
|
|
|
35
|
|
|
36 Hω2 : {n : Level} → OD {suc n}
|
|
|
37 Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
|
|
|
38
|
|
|
39 _⊆_ : {n : Level} → ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n)
|
|
|
40 _⊆_ A B {x} = A ∋ x → B ∋ x
|
|
|
41
|
|
|
42 Hω2Filter : {n : Level} → Filter {n} Hω2 od∅
|
|
|
43 Hω2Filter {n} = record {
|
|
|
44 _⊇_ = {!!}
|
|
|
45 ; G = {!!}
|
|
|
46 ; G∋1 = {!!}
|
|
|
47 ; Gmax = {!!}
|
|
|
48 ; Gless = {!!}
|
|
|
49 ; Gcompat = {!!}
|
|
|
50 } where
|
|
|
51 P = Hω2
|
|
|
52 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
|
|
|
53 _⊇_ = {!!}
|
|
|
54 G : OD {suc n}
|
|
|
55 G = {!!}
|
|
|
56 G∋1 : G ∋ od∅
|
|
|
57 G∋1 = {!!}
|
|
|
58 Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ od∅
|
|
|
59 Gmax = {!!}
|
|
|
60 Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q
|
|
|
61 Gless = {!!}
|
|
|
62 Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
|
|
|
63 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r )))
|
|
|
64 Gcompat = {!!}
|
|
|
65
|
