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

comparison ordinal-definable.agda @ 89:dccc9e2d1804

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 Wed, 05 Jun 2019 09:47:19 +0900
parents 296388c03358
children 38d139b5edac
comparison
equal deleted inserted replaced
88:975e72ae0541 89:dccc9e2d1804
232 lemma1 = cong ( λ k → od→ord k ) o∅≡od∅ 232 lemma1 = cong ( λ k → od→ord k ) o∅≡od∅
233 lemma o∅ ne | yes refl | () 233 lemma o∅ ne | yes refl | ()
234 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p)) 234 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p))
235 235
236 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 236 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
237
238 postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
239
237 240
238 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 241 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
239 OD→ZF {n} = record { 242 OD→ZF {n} = record {
240 ZFSet = OD {suc n} 243 ZFSet = OD {suc n}
241 ; _∋_ = _∋_ 244 ; _∋_ = _∋_
341 reg {y} t with proj1 t 344 reg {y} t with proj1 t
342 ... | x∈∅ = x∈∅ 345 ... | x∈∅ = x∈∅
343 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 346 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
344 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 347 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
345 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 348 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
346 pair-osuc : {x y : OD {suc n}} → (x , x) ∋ y → (od→ord y ) o< osuc (od→ord x) 349 xx-union : {x : OD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) }
347 pair-osuc {x} {y} z with union← (x , x) y {!!} 350 xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x))
348 ... | t = {!!} 351 xxx-union : {x : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))}
349 next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x)) 352 xxx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) lemma where
350 eq→ (next x ) {y} z = {!!} -- z : y o< osuc (osuc ox ) → y < osuc ox 353 lemma : {x : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
351 eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_} 354 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) {!!} ) ) ( cong ( λ k → osuc k ) {!!} )
352 (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where
353 lemma0 : (x , x) ∋ ord→od y
354 lemma0 = o<-subst {suc n} {od→ord (ord→od y)} {od→ord {!!}} (c<→o< z) {!!} {!!}
355 lemma1 : (x , (x , x)) ∋ ord→od (osuc y) -- z : def (ord→od (osuc (od→ord x))) y
356 lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< {!!}) oiso refl)
357 lemma1 | case1 x = {!!}
358 lemma1 | case2 t = {!!}
359 -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!}
360 lemma2 : ord→od (osuc y) ∋ ord→od y
361 lemma2 = o<→c< <-osuc
362 next' : (x : OD) → ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x))
363 next' x = subst ( λ k → k == ord→od (osuc (od→ord x))) (sym oiso) (next x)
364 infinite : OD {suc n} 355 infinite : OD {suc n}
365 infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) 356 infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
366 infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) ∋ od∅ {suc n} 357 infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) ∋ od∅ {suc n}
367 infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅} 358 infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
368 (o<→c< ( case1 (s≤s z≤n ))) refl (cong (λ k → od→ord k) o∅≡od∅ ) 359 (o<→c< ( case1 (s≤s z≤n ))) refl (cong (λ k → od→ord k) o∅≡od∅ )