Mercurial > hg > Members > kono > Proof > ZF-in-agda
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 { |