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

comparison OD.agda @ 404:f7b844af9a50

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 13:34:25 +0900
parents ce2ce3f62023
children 85b328d3b96b
comparison
equal deleted inserted replaced
403:ce2ce3f62023 404:f7b844af9a50
492 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc 492 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc
493 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc 493 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
494 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) 494 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl )
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 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i 500 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 501 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) → 502 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
517 lemma0 : x ∋ ord→od x₁ 517 lemma0 : x ∋ ord→od x₁
518 lemma0 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not 518 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 } ) 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 } )
520 lemma1 : infinite ∋ ord→od x₁ 520 lemma1 : infinite ∋ ord→od x₁
521 lemma1 = subst (λ k → odef infinite k) (sym diso) ltd 521 lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
522 lemma2 : {x₁ : Ordinal} → {ltd : infinite-d x₁ } → ω→nato ltd ≡ ω→nat (ord→od x₁) (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 lemma2 {o∅} {iφ} = {!!} 523 lemma5 {x} {y} eq = {!!}
524 lemma2 {x₁} {isuc ltd} = cong (λ k → Suc k ) ( lemma2 {_} {ltd} ) 524 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
525 lemma3 iφ iφ refl = HE.refl
526 lemma3 iφ (isuc ltd1) eq = {!!}
527 lemma3 (isuc ltd) iφ eq = {!!}
528 lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (lemma5 (sym eq))
529 ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (lemma5 eq)) t
530 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
532 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
525 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ 534 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁
526 lemma = trans (cong (λ k → nat→ω k) lemma2) ( prev {ord→od x₁} lemma0 lemma1 ) 535 lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym diso) ltd) diso ) ) ( prev {ord→od x₁} lemma0 lemma1 )
536
537 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
538 ω→nat-iso {Zero} = {!!}
539 ω→nat-iso {Suc i} = {!!}
527 540
528 ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y 541 ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y
529 ψiso {ψ} t refl = t 542 ψiso {ψ} t refl = t
530 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 543 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
531 selection {ψ} {X} {y} = record { 544 selection {ψ} {X} {y} = record {