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

comparison filter.agda @ 236:650bdad56729

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 Fri, 16 Aug 2019 15:53:29 +0900
parents 0b9645a65542
children 9bf100ae50ac
comparison
equal deleted inserted replaced
235:846e0926bb89 236:650bdad56729
1 open import Level 1 open import Level
2 open import OD 2 open import Ordinals
3 module filter {n : Level } (O : Ordinals {n}) where
4
3 open import zf 5 open import zf
4 open import ordinal 6 open import logic
5 module filter ( n : Level ) where 7 import OD
6 8
7 open import Relation.Nullary 9 open import Relation.Nullary
8 open import Relation.Binary 10 open import Relation.Binary
9 open import Data.Empty 11 open import Data.Empty
10 open import Relation.Binary 12 open import Relation.Binary
11 open import Relation.Binary.Core 13 open import Relation.Binary.Core
12 open import Relation.Binary.PropositionalEquality 14 open import Relation.Binary.PropositionalEquality
13 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
14 16
15 od = OD→ZF {n} 17 open inOrdinal O
18 open OD O
19 open OD.OD
16 20
21 open _∧_
22 open _∨_
23 open Bool
17 24
18 record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where 25 record Filter ( P max : OD ) : Set (suc n) where
19 field 26 field
20 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) 27 _⊇_ : OD → OD → Set n
21 G : OD {suc n} 28 G : OD
22 G∋1 : G ∋ max 29 G∋1 : G ∋ max
23 Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ max 30 Gmax : { p : OD } → P ∋ p → p ⊇ max
24 Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q 31 Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q
25 Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ ( 32 Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ (
26 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r ))) 33 ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r )))
27 34
28 dense : {n : Level} → Set (suc (suc n)) 35 dense : Set (suc n)
29 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 )) 36 dense = { D P p : OD } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q ))
30 37
31 record NatFilter {n : Level} ( P : Nat → Set n) : Set (suc n) where 38 record NatFilter ( P : Nat → Set n) : Set (suc n) where
32 field 39 field
33 GN : Nat → Set n 40 GN : Nat → Set n
34 GN∋1 : GN 0 41 GN∋1 : GN 0
35 GNmax : { p : Nat } → P p → 0 ≤ p 42 GNmax : { p : Nat } → P p → 0 ≤ p
36 GNless : { p q : Nat } → GN p → P q → q ≤ p → GN q 43 GNless : { p q : Nat } → GN p → P q → q ≤ p → GN q
44 51
45 open OD.OD 52 open OD.OD
46 53
47 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) 54 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
48 55
49 Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n} 56 Pred : ( Dom : OD ) → OD
50 Pred {n} dom = record { 57 Pred dom = record {
51 def = λ x → def dom x → Set n 58 def = λ x → def dom x → {!!}
52 } 59 }
53 60
54 Hω2 : {n : Level} → OD {suc n} 61 Hω2 : OD
55 Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) } 62 Hω2 = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) }
56 63
57 Hω2Filter : {n : Level} → Filter {n} Hω2 od∅ 64 Hω2Filter : Filter Hω2 od∅
58 Hω2Filter {n} = record { 65 Hω2Filter = record {
59 _⊇_ = _⊇_ 66 _⊇_ = _⊇_
60 ; G = {!!} 67 ; G = {!!}
61 ; G∋1 = {!!} 68 ; G∋1 = {!!}
62 ; Gmax = {!!} 69 ; Gmax = {!!}
63 ; Gless = {!!} 70 ; Gless = {!!}
64 ; Gcompat = {!!} 71 ; Gcompat = {!!}
65 } where 72 } where
66 P = Hω2 73 P = Hω2
67 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) 74 _⊇_ : OD → OD → Set n
68 _⊇_ = {!!} 75 _⊇_ = {!!}
69 G : OD {suc n} 76 G : OD
70 G = {!!} 77 G = {!!}
71 G∋1 : G ∋ od∅ 78 G∋1 : G ∋ od∅
72 G∋1 = {!!} 79 G∋1 = {!!}
73 Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ od∅ 80 Gmax : { p : OD } → P ∋ p → p ⊇ od∅
74 Gmax = {!!} 81 Gmax = {!!}
75 Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q 82 Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q
76 Gless = {!!} 83 Gless = {!!}
77 Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ ( 84 Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ (
78 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r ))) 85 ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r )))
79 Gcompat = {!!} 86 Gcompat = {!!}
80 87