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

comparison filter.agda @ 190:6e778b0a7202

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jul 2019 21:08:06 +0900
parents
children 9eb6a8691f02
comparison
equal deleted inserted replaced
189:540b845ea2de 190:6e778b0a7202
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