Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 191:9eb6a8691f02
choice function cannot jump between ordinal level
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Jul 2019 14:07:08 +0900 |
| parents | 6e778b0a7202 |
| children | 0b9645a65542 |
| rev | line source |
|---|---|
| 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 | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
13 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
|
14 |
| 190 | 15 |
| 16 record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where | |
| 17 field | |
| 18 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) | |
| 19 G : OD {suc n} | |
| 20 G∋1 : G ∋ max | |
| 21 Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ max | |
| 22 Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q | |
| 23 Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ ( | |
| 24 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r ))) | |
| 25 | |
| 26 dense : {n : Level} → Set (suc (suc n)) | |
| 27 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 )) | |
| 28 | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
29 record NatFilter {n : Level} ( P : Nat → Set n) : Set (suc n) where |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
30 field |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
31 GN : Nat → Set n |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
32 GN∋1 : GN 0 |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
33 GNmax : { p : Nat } → P p → 0 ≤ p |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
34 GNless : { p q : Nat } → GN p → P q → q ≤ p → GN q |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
35 Gr : ( p q : Nat ) → GN p → GN q → Nat |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
36 GNcompat : { p q : Nat } → (gp : GN p) → (gq : GN q ) → ( Gr p q gp gq ≤ p ) ∨ ( Gr p q gp gq ≤ q ) |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
37 |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
38 record NatDense {n : Level} ( P : Nat → Set n) : Set (suc n) where |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
39 field |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
40 Gmid : { p : Nat } → P p → Nat |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
41 GDense : { D : Nat → Set n } → {x p : Nat } → (pp : P p ) → D (Gmid {p} pp) → Gmid pp ≤ p |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
42 |
| 190 | 43 open OD.OD |
| 44 | |
| 45 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) | |
| 46 | |
| 47 Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n} | |
| 48 Pred {n} dom = record { | |
| 49 def = λ x → def dom x → Set n | |
| 50 } | |
| 51 | |
| 52 Hω2 : {n : Level} → OD {suc n} | |
| 53 Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) } | |
| 54 | |
| 55 Hω2Filter : {n : Level} → Filter {n} Hω2 od∅ | |
| 56 Hω2Filter {n} = record { | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
57 _⊇_ = _⊇_ |
| 190 | 58 ; G = {!!} |
| 59 ; G∋1 = {!!} | |
| 60 ; Gmax = {!!} | |
| 61 ; Gless = {!!} | |
| 62 ; Gcompat = {!!} | |
| 63 } where | |
| 64 P = Hω2 | |
| 65 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) | |
| 66 _⊇_ = {!!} | |
| 67 G : OD {suc n} | |
| 68 G = {!!} | |
| 69 G∋1 : G ∋ od∅ | |
| 70 G∋1 = {!!} | |
| 71 Gmax : { p : OD {suc n} } → P ∋ p → p ⊇ od∅ | |
| 72 Gmax = {!!} | |
| 73 Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q | |
| 74 Gless = {!!} | |
| 75 Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ ( | |
| 76 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r ))) | |
| 77 Gcompat = {!!} | |
| 78 |