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

comparison filter.agda @ 363:aad9249d1e8f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hω2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Jul 2020 10:36:32 +0900
parents 12071f79f3cf
children 67580311cc8e
comparison
equal deleted inserted replaced
362:8a430df110eb 363:aad9249d1e8f
4 4
5 open import zf 5 open import zf
6 open import logic 6 open import logic
7 import OD 7 import OD
8 8
9 open import Relation.Nullary 9 open import Relation.Nullary
10 open import Relation.Binary 10 open import Relation.Binary
11 open import Data.Empty 11 open import Data.Empty
12 open import Relation.Binary 12 open import Relation.Binary
13 open import Relation.Binary.Core 13 open import Relation.Binary.Core
14 open import Relation.Binary.PropositionalEquality 14 open import Relation.Binary.PropositionalEquality
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
16 import BAlgbra 16 import BAlgbra
17 17
18 open BAlgbra O 18 open BAlgbra O
19 19
20 open inOrdinal O 20 open inOrdinal O
21 open OD O 21 open OD O
129 incl : dense ⊆ P 129 incl : dense ⊆ P
130 dense-f : HOD → HOD 130 dense-f : HOD → HOD
131 dense-d : { p : HOD} → P ∋ p → dense ∋ dense-f p 131 dense-d : { p : HOD} → P ∋ p → dense ∋ dense-f p
132 dense-p : { p : HOD} → P ∋ p → p ⊆ (dense-f p) 132 dense-p : { p : HOD} → P ∋ p → p ⊆ (dense-f p)
133 133
134 -- the set of finite partial functions from ω to 2
135 --
136 -- ph2 : Nat → Set → 2
137 -- ph2 : Nat → Maybe 2
138 --
139 -- Hω2 : Filter (Power (Power infinite))
140
141 record Ideal ( L : HOD ) : Set (suc n) where 134 record Ideal ( L : HOD ) : Set (suc n) where
142 field 135 field
143 ideal : HOD 136 ideal : HOD
144 i⊆PL : ideal ⊆ Power L 137 i⊆PL : ideal ⊆ Power L
145 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q 138 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
151 proper-ideal {L} P {p} = ideal P ∋ od∅ 144 proper-ideal {L} P {p} = ideal P ∋ od∅
152 145
153 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n 146 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
154 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 )
155 148
149 -- the set of finite partial functions from ω to 2
150 --
151 -- ph2 : Nat → Set → 2
152 -- ph2 : Nat → Maybe 2
153 --
154 -- Hω2 : Filter (Power (Power infinite))
155
156 import OPair
157 open OPair O
158
159 ODSuc : (y : HOD) → infinite ∋ y → HOD
160 ODSuc y lt = Union (y , (y , y))
161
162 nat→ω : Nat → HOD
163 nat→ω Zero = od∅
164 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
165
166 data Hω2 : ( x : Ordinal ) → Set n where
167 hφ : Hω2 o∅
168 h0 : {x : Ordinal } → Hω2 x →
169 Hω2 (od→ord < nat→ω 0 , ord→od x >)
170 h1 : {x : Ordinal } → Hω2 x →
171 Hω2 (od→ord < nat→ω 1 , ord→od x >)
172 h2 : {x : Ordinal } → Hω2 x →
173 Hω2 (od→ord < nat→ω 2 , ord→od x >)
174
175 HODω2 : HOD
176 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = {!!} ; <odmax = {!!} }
177
178 -- the set of finite partial functions from ω to 2
179
180 data Two : Set n where
181 i0 : Two
182 i1 : Two
183
184 Hω2f : Set (suc n)
185 Hω2f = (Nat → Set n) → Two
186
187 Hω2f→Hω2 : Hω2f → HOD
188 Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
189
190