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

comparison constructible-set.agda @ 28:f36e40d5d2c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
OD continue
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 19 May 2019 18:13:42 +0900
parents bade0a35fdd9
children
comparison
equal deleted inserted replaced
27:bade0a35fdd9 28:f36e40d5d2c3
188 188
189 open OD 189 open OD
190 open import Data.Unit 190 open import Data.Unit
191 191
192 postulate -- this is proved by Godel numbering of def 192 postulate -- this is proved by Godel numbering of def
193 _c<_ : {n : Level } → (x y : OD {n} ) → Set n 193 _c<_ : {n : Level } → (x y : OD {n} ) → Set (suc n)
194 ODpre : {n : Level} → IsPreorder {suc n} {suc n} {n} _≡_ _c<_ 194 ODpre : {n : Level} → IsPreorder {suc n} {suc n} {suc n} _≡_ _c<_
195 195
196 -- o∋ : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n 196 -- o∋ : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
197 -- o∋ a x x<A = def a x x<A 197 -- o∋ a x x<A = def a x x<A
198 198
199 -- TC u : Transitive Closure of OD u 199 -- TC u : Transitive Closure of OD u
205 -- 205 --
206 -- TC u = TC ω u = ∪ ( TC n ) n ∈ ω 206 -- TC u = TC ω u = ∪ ( TC n ) n ∈ ω
207 -- 207 --
208 -- u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) .... 208 -- u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
209 -- 209 --
210 -- HOD = {x | TC x ⊆ OD } ⊆ OD 210 -- Heritic Ordinal Definable
211 --
212 -- ( HOD = {x | TC x ⊆ OD } ) ⊆ OD
211 -- 213 --
212 214
213 record HOD {n : Level} : Set (suc n) where 215 HOD = OD
214 field 216
215 hod : OD {n} 217 c∅ : {n : Level} → HOD {n}
216 tc : ? 218 c∅ {n} = record { α = o∅ ; def = λ x y → Lift n ⊥ }
219
220 HOD→ZF : {n : Level} → ZF {suc n} {suc n}
221 HOD→ZF {n} = record {
222 ZFSet = HOD
223 ; _∋_ = λ a b → b c< a
224 ; _≈_ = _≡_
225 ; ∅ = c∅
226 ; _,_ = _,_
227 ; Union = Union
228 ; Power = {!!}
229 ; Select = Select
230 ; Replace = Replace
231 ; infinite = {!!}
232 ; isZF = {!!}
233 } where
234 Select : (X : HOD {n}) → (HOD {n} → Set (suc n)) → HOD {n}
235 Select X ψ = record { α = α X ; def = λ x → {!!} } where
236 select : Ordinal → Set n
237 select x with ψ (record { α = x ; def = λ x → {!!} })
238 ... | t = Lift n ⊤
239 Replace : (X : HOD {n} ) → (HOD → HOD) → HOD
240 Replace X ψ = record { α = {!!} ; def = λ x → {!!} }
241 _,_ : HOD {n} → HOD → HOD
242 a , b = record { α = maxα (α a) (α b) ; def = λ x x<ab → ( ) } where
243 a∨b : Ordinal {suc n} → Set n
244 a∨b = {!!}
245 Union : HOD → HOD
246 Union a = {!!}