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

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
2 open import Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
3 module filter {n : Level } (O : Ordinals {n}) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
4
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import zf
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
6 open import logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
7 import OD
193
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
8
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Empty
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Binary.Core
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 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
15 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
16
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
17 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
18 open OD O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
19 open OD.OD
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
21 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
22 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
23 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
24
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
25 record Filter ( P max : OD ) : Set (suc n) where
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 field
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
27 _⊇_ : OD → OD → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
28 G : OD
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 G∋1 : G ∋ max
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
30 Gmax : { p : OD } → P ∋ p → p ⊇ max
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
31 Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
32 Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ (
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
33 ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r )))
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
35 dense : Set (suc n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
36 dense = { D P p : OD } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q ))
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
38 record NatFilter ( P : Nat → Set n) : Set (suc n) where
191
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 GN : Nat → Set n
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
41 GN∋1 : GN 0
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
42 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
43 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
44 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
45 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
46
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
47 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
48 field
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
49 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
50 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
51
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 open OD.OD
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
56 Pred : ( Dom : OD ) → OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
57 Pred dom = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
58 def = λ x → def dom x → {!!}
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 }
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
61 Hω2 : OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
62 Hω2 = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) }
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
64 Hω2Filter : Filter Hω2 od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
65 Hω2Filter = record {
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
66 _⊇_ = _⊇_
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 ; G = {!!}
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 ; G∋1 = {!!}
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 ; Gmax = {!!}
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 ; Gless = {!!}
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ; Gcompat = {!!}
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 } where
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 P = Hω2
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
74 _⊇_ : OD → OD → Set n
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 _⊇_ = {!!}
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
76 G : OD
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 G = {!!}
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 G∋1 : G ∋ od∅
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 G∋1 = {!!}
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
80 Gmax : { p : OD } → P ∋ p → p ⊇ od∅
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 Gmax = {!!}
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
82 Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 Gless = {!!}
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
84 Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ (
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
85 ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r )))
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 Gcompat = {!!}
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87