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

comparison ordinal-definable.agda @ 77:75ba8cf64707

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Power Set on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Jun 2019 15:12:26 +0900
parents 8e8f54e7a030
children 9a7a64b2388c
comparison
equal deleted inserted replaced
76:8e8f54e7a030 77:75ba8cf64707
281 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅ 281 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
282 lemma1 = cong ( λ k → od→ord k ) o∅→od∅ 282 lemma1 = cong ( λ k → od→ord k ) o∅→od∅
283 lemma o∅ ne | yes refl | () 283 lemma o∅ ne | yes refl | ()
284 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p)) 284 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))
285 285
286 -- ∃-set : {n : Level} → ( x : OD {suc n} ) → ( ψ : OD {suc n} → Set (suc n) ) → Set (suc n)
287 -- ∃-set = {!!}
288
289 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n ))
290
291 -- ==∅→≡ : {n : Level} → { x : OD {suc n} } → ( x == od∅ {suc n} ) → x ≡ od∅ {suc n}
292 -- ==∅→≡ {n} {x} eq = cong ( λ k → record { def = k } ) (trans {!!} ∅-base-def ) where
293
294
295 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 286 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
296 287
297 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 288 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
298 OD→ZF {n} = record { 289 OD→ZF {n} = record {
299 ZFSet = OD {suc n} 290 ZFSet = OD {suc n}
314 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 305 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
315 _,_ : OD {suc n} → OD {suc n} → OD {suc n} 306 _,_ : OD {suc n} → OD {suc n} → OD {suc n}
316 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } 307 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
317 Union : OD {suc n} → OD {suc n} 308 Union : OD {suc n} → OD {suc n}
318 Union U = record { def = λ y → osuc y o< (od→ord U) } 309 Union U = record { def = λ y → osuc y o< (od→ord U) }
310 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
319 Power : OD {suc n} → OD {suc n} 311 Power : OD {suc n} → OD {suc n}
320 Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y ) } 312 Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) }
321 ZFSet = OD {suc n} 313 ZFSet = OD {suc n}
322 _∈_ : ( A B : ZFSet ) → Set (suc n) 314 _∈_ : ( A B : ZFSet ) → Set (suc n)
323 A ∈ B = B ∋ A 315 A ∈ B = B ∋ A
324 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 316 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
325 _⊆_ A B {x} = A ∋ x → B ∋ x 317 _⊆_ A B {x} = A ∋ x → B ∋ x
353 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 345 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
354 proj1 (pair A B ) = case1 refl 346 proj1 (pair A B ) = case1 refl
355 proj2 (pair A B ) = case2 refl 347 proj2 (pair A B ) = case2 refl
356 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 348 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
357 empty x () 349 empty x ()
358 -- Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y ) } 350 --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) }
359 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x 351 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
360 power→ A t P∋t {x} t∋x = transitive {n} {A} {t} {x} lemma t∋x where 352 power→ A t P∋t {x} t∋x = proj1 (P∋t (od→ord x) )
361 lemma : A ∋ t 353 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
362 lemma = proj1 (P∋t (od→ord x )) 354 power← A t t→A z = record { proj1 = lemma2 ; proj2 = lemma1 } where
363 power← : (A t : OD) {x : OD} → (t ∋ x → A ∋ x) → Power A ∋ t 355 lemma1 : def (ord→od (od→ord t)) z
364 power← A t {x} t→A y = record { proj1 = lemma1 ; proj2 = lemma2 } where
365 lemma1 : def A (od→ord t)
366 lemma1 = {!!} 356 lemma1 = {!!}
367 lemma2 : def (ord→od y) (od→ord t) 357 lemma2 : def A z
368 lemma2 = {!!} 358 lemma2 = {!!}
369 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} 359 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
370 union-u X z U>z = ord→od ( osuc ( od→ord z ) ) 360 union-u X z U>z = ord→od ( osuc ( od→ord z ) )
371 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z 361 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z
372 union-lemma-u {X} {z} U>z = lemma <-osuc where 362 union-lemma-u {X} {z} U>z = lemma <-osuc where