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

comparison filter.agda @ 365:7f919d6b045b

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 Sat, 18 Jul 2020 12:29:38 +0900
parents 67580311cc8e
children 1a8ca713bc32
comparison
equal deleted inserted replaced
364:67580311cc8e 365:7f919d6b045b
69 69
70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
71 q∩q⊆q = record { incl = λ lt → proj1 lt } 71 q∩q⊆q = record { incl = λ lt → proj1 lt }
72 72
73 open HOD 73 open HOD
74 _=h=_ : (x y : HOD) → Set n
75 x =h= y = od x == od y
76 74
77 ----- 75 -----
78 -- 76 --
79 -- ultra filter is prime 77 -- ultra filter is prime
80 -- 78 --
155 open OPair O 153 open OPair O
156 154
157 ODSuc : (y : HOD) → infinite ∋ y → HOD 155 ODSuc : (y : HOD) → infinite ∋ y → HOD
158 ODSuc y lt = Union (y , (y , y)) 156 ODSuc y lt = Union (y , (y , y))
159 157
160 nat→ω : Nat → HOD 158 postulate
161 nat→ω Zero = od∅
162 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
163
164 postulate -- we have proved in other module
165 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
166 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
167
168 postulate
169 ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 159 ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x))
160
170 161
171 data Hω2 : ( x : Ordinal ) → Set n where 162 data Hω2 : ( x : Ordinal ) → Set n where
172 hφ : Hω2 o∅ 163 hφ : Hω2 o∅
173 h0 : {x : Ordinal } → Hω2 x → 164 h0 : {x : Ordinal } → Hω2 x →
174 Hω2 (od→ord < nat→ω 0 , ord→od x >) 165 Hω2 (od→ord < nat→ω 0 , ord→od x >)
177 h2 : {x : Ordinal } → Hω2 x → 168 h2 : {x : Ordinal } → Hω2 x →
178 Hω2 (od→ord < nat→ω 2 , ord→od x >) 169 Hω2 (od→ord < nat→ω 2 , ord→od x >)
179 170
180 HODω2 : HOD 171 HODω2 : HOD
181 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where 172 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where
173 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
174 ω<next = ω<next-o∅ ho<
182 lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n → od→ord < ord→od n , ord→od y > o< next y 175 lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n → od→ord < ord→od n , ord→od y > o< next y
183 lemma0 {n} {y} hw2 inf = nexto=n {!!} 176 lemma0 {n} {y} hw2 inf = nexto=n {!!}
184 odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅ 177 odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅
185 odmax0 {o∅} hφ = x<nx 178 odmax0 {o∅} hφ = x<nx
186 odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {0} ))) 179 odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {0} )))
187 odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {1} ))) 180 odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {1} )))
188 odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {2} ))) 181 odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {2} )))
189 182
183 HODω2-Filter : Filter HODω2
184 HODω2-Filter = record {
185 filter = {!!}
186 ; f⊆PL = {!!}
187 ; filter1 = {!!}
188 ; filter2 = {!!}
189 } where
190 filter0 : HOD
191 filter0 = {!!}
192 f⊆PL1 : filter0 ⊆ Power HODω2
193 f⊆PL1 = {!!}
194 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q
195 filter11 = {!!}
196 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q)
197 filter12 = {!!}
198
190 -- the set of finite partial functions from ω to 2 199 -- the set of finite partial functions from ω to 2
191 200
192 data Two : Set n where 201 data Two : Set n where
193 i0 : Two 202 i0 : Two
194 i1 : Two 203 i1 : Two