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

annotate filter.agda @ 271:2169d948159b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix incl
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Dec 2019 23:45:59 +0900
parents fc3d4bc1dc5e
children 985a1af11bce
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
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
25 _∩_ : ( A B : OD ) → OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
26 A ∩ B = record { def = λ x → def A x ∧ def B x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
28 _∪_ : ( A B : OD ) → OD
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
29 A ∪ B = record { def = λ x → def A x ∨ def B x }
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
30
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
31 _＼_ : ( A B : OD ) → OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
32 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
33
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
34 ∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
35 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
36 lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
37 lemma1 {x} lt = lemma3 lt where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
38 lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
39 lemma4 {y} z with proj1 z
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
40 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
41 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
42 lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
43 lemma3 not = double-neg-eilm (FExists _ lemma4 not) -- choice
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
44 lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
45 lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
46 (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
47 lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
48 (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x}))
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
49
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
50 ∩-Select : { A B : OD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
51 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
52 lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
53 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) }
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
54 lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
55 lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
56 record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } }
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
57
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
58 dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
59 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
60 lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
61 lemma1 {x} lt with proj2 lt
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
62 lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
63 lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
64 lemma2 : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
65 lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) }
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
66 lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) }
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
67
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
68 dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r )
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
69 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
70 lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
71 lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
72 lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) }
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
73 lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
74 lemma2 {x} lt with proj1 lt | proj2 lt
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
75 lemma2 {x} lt | case1 cp | _ = case1 cp
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
76 lemma2 {x} lt | _ | case1 cp = case1 cp
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
77 lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } )
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
78
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
79 record IsBooleanAlgebra ( L : Set n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
80 ( b1 : L )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
81 ( b0 : L )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
82 ( -_ : L → L )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
83 ( _+_ : L → L → L )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
84 ( _*_ : L → L → L ) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
85 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
86 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
87 *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
88 +-sym : {a b : L } → a + b ≡ b + a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
89 -sym : {a b : L } → a * b ≡ b * a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
90 -aab : {a b : L } → a + ( a * b ) ≡ a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
91 *-aab : {a b : L } → a * ( a + b ) ≡ a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
92 -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
93 *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
94 a+0 : {a : L } → a + b0 ≡ a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
95 a*1 : {a : L } → a * b1 ≡ a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
96 a+-a1 : {a : L } → a + ( - a ) ≡ b1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
97 a*-a0 : {a : L } → a * ( - a ) ≡ b0
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
98
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
99 record BooleanAlgebra ( L : Set n) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
100 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
101 b1 : L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
102 b0 : L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
103 -_ : L → L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
104 _++_ : L → L → L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
105 _**_ : L → L → L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
106 isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
107
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
108
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
109 record Filter ( L : OD ) : 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
110 field
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
111 filter : OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
112 proper : ¬ ( filter ∋ od∅ )
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
113 inL : filter ⊆ L
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
114 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
115 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
116
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
117 open Filter
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
118
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
119 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
120 L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!}
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
122 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
123 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
125 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
126 ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
128
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
129 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
130 filter-lemma1 {L} P {p} {q} u lt = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
131
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
132 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
133 filter-lemma2 {L} P prime p with prime {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
134 ... | t = {!!}
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
135
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
136 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
137 generated-filter {L} P p = record {
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
138 proper = {!!} ;
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
139 filter = {!!} ; inL = {!!} ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
140 filter1 = {!!} ; filter2 = {!!}
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
141 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
142
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
143 record Dense (P : OD ) : Set (suc n) where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
144 field
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
145 dense : OD
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
146 incl : dense ⊆ P
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
147 dense-f : OD → OD
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
148 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p)
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
149
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
150 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
151
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
152 infinite = ZF.infinite OD→ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
153
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
154 module in-countable-ordinal {n : Level} where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
155
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
156 import ordinal
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
157
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
158 open ordinal.C-Ordinal-with-choice
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
159
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
160 Hω2 : Filter (Power (Power infinite))
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
161 Hω2 = {!!}
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
162