comparison OD.agda @ 403:ce2ce3f62023

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Jul 2020 10:51:08 +0900
parents d87492ae4040
children f7b844af9a50
comparison
equal deleted inserted replaced
402:d87492ae4040 403:ce2ce3f62023
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)
523 lemma2 {o∅} {iφ} = {!!}
524 lemma2 {x₁} {isuc ltd} = cong (λ k → Suc k ) ( lemma2 {_} {ltd} )
522 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ 525 lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁
523 lemma with prev {ord→od x₁} lemma0 lemma1 526 lemma = trans (cong (λ k → nat→ω k) lemma2) ( prev {ord→od x₁} lemma0 lemma1 )
524 ... | t = {!!}
525 527
526 ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y 528 ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y
527 ψiso {ψ} t refl = t 529 ψiso {ψ} t refl = t
528 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 530 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
529 selection {ψ} {X} {y} = record { 531 selection {ψ} {X} {y} = record {