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