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

comparison OD.agda @ 405:85b328d3b96b

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 Tue, 28 Jul 2020 14:15:33 +0900
parents f7b844af9a50
children bf409d31184c
comparison
equal deleted inserted replaced
404:f7b844af9a50 405:85b328d3b96b
495 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) 495 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
496 496
497 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 497 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
498 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m 498 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m
499 499
500 ω-prev-eq1 : {x y : Ordinal} → od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → ¬ (x o< y)
501 ω-prev-eq1 {x} {y} eq not with eq→ (ord→== eq) {od→ord (ord→od y , ord→od y)} (λ not2 → not2 (od→ord (ord→od y , ord→od y))
502 record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord (ord→od y))) {!!} (case1 refl) } )
503 ... | t = {!!}
504
505 ω-prev-eq : {x y : Ordinal} → od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
506 ω-prev-eq {x} {y} eq with trio< x y
507 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = {!!}
508 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
509 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = {!!}
510
500 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i 511 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
501 nat→ω-iso {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where 512 nat→ω-iso {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where
502 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) → 513 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
503 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x 514 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
504 ind {x} prev lt = ind1 lt oiso where 515 ind {x} prev lt = ind1 lt oiso where
517 lemma0 : x ∋ ord→od x₁ 528 lemma0 : x ∋ ord→od x₁
518 lemma0 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not 529 lemma0 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not
519 (od→ord (ord→od x₁ , ord→od x₁)) record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } ) 530 (od→ord (ord→od x₁ , ord→od x₁)) record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
520 lemma1 : infinite ∋ ord→od x₁ 531 lemma1 : infinite ∋ ord→od x₁
521 lemma1 = subst (λ k → odef infinite k) (sym diso) ltd 532 lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
522 lemma5 : {x y : Ordinal} → od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
523 lemma5 {x} {y} eq = {!!}
524 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1 533 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
525 lemma3 iφ iφ refl = HE.refl 534 lemma3 iφ iφ refl = HE.refl
526 lemma3 iφ (isuc ltd1) eq = {!!} 535 lemma3 iφ (isuc ltd1) eq = {!!}
527 lemma3 (isuc ltd) iφ eq = {!!} 536 lemma3 (isuc ltd) iφ eq = {!!}
528 lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (lemma5 (sym eq)) 537 lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
529 ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (lemma5 eq)) t 538 ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t
530 lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1 539 lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
531 lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where 540 lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where
532 lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 541 lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
533 lemma6 refl HE.refl = refl 542 lemma6 refl HE.refl = refl
534 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ 543 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁