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

comparison filter.agda @ 364:67580311cc8e

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 11:38:33 +0900
parents aad9249d1e8f
children 7f919d6b045b
comparison
equal deleted inserted replaced
363:aad9249d1e8f 364:67580311cc8e
144 proper-ideal {L} P {p} = ideal P ∋ od∅ 144 proper-ideal {L} P {p} = ideal P ∋ od∅
145 145
146 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n 146 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
147 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) 147 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
148 148
149 -------
149 -- the set of finite partial functions from ω to 2 150 -- the set of finite partial functions from ω to 2
150 -- 151 --
151 -- ph2 : Nat → Set → 2 152 --
152 -- ph2 : Nat → Maybe 2
153 --
154 -- Hω2 : Filter (Power (Power infinite))
155 153
156 import OPair 154 import OPair
157 open OPair O 155 open OPair O
158 156
159 ODSuc : (y : HOD) → infinite ∋ y → HOD 157 ODSuc : (y : HOD) → infinite ∋ y → HOD
160 ODSuc y lt = Union (y , (y , y)) 158 ODSuc y lt = Union (y , (y , y))
161 159
162 nat→ω : Nat → HOD 160 nat→ω : Nat → HOD
163 nat→ω Zero = od∅ 161 nat→ω Zero = od∅
164 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 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))
165 170
166 data Hω2 : ( x : Ordinal ) → Set n where 171 data Hω2 : ( x : Ordinal ) → Set n where
167 hφ : Hω2 o∅ 172 hφ : Hω2 o∅
168 h0 : {x : Ordinal } → Hω2 x → 173 h0 : {x : Ordinal } → Hω2 x →
169 Hω2 (od→ord < nat→ω 0 , ord→od x >) 174 Hω2 (od→ord < nat→ω 0 , ord→od x >)
171 Hω2 (od→ord < nat→ω 1 , ord→od x >) 176 Hω2 (od→ord < nat→ω 1 , ord→od x >)
172 h2 : {x : Ordinal } → Hω2 x → 177 h2 : {x : Ordinal } → Hω2 x →
173 Hω2 (od→ord < nat→ω 2 , ord→od x >) 178 Hω2 (od→ord < nat→ω 2 , ord→od x >)
174 179
175 HODω2 : HOD 180 HODω2 : HOD
176 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = {!!} ; <odmax = {!!} } 181 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where
182 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 {!!}
184 odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅
185 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} )))
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} )))
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} )))
177 189
178 -- the set of finite partial functions from ω to 2 190 -- the set of finite partial functions from ω to 2
179 191
180 data Two : Set n where 192 data Two : Set n where
181 i0 : Two 193 i0 : Two