Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
line wrap: on
line diff
--- a/OD.agda Tue Jul 28 10:32:33 2020 +0900 +++ b/OD.agda Tue Jul 28 10:51:08 2020 +0900 @@ -519,9 +519,11 @@ (od→ord (ord→od x₁ , ord→od x₁)) record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } ) lemma1 : infinite ∋ ord→od x₁ lemma1 = subst (λ k → odef infinite k) (sym diso) ltd + lemma2 : {x₁ : Ordinal} → {ltd : infinite-d x₁ } → ω→nato ltd ≡ ω→nat (ord→od x₁) (subst (λ k → odef infinite k) (sym diso) ltd) + lemma2 {o∅} {iφ} = {!!} + lemma2 {x₁} {isuc ltd} = cong (λ k → Suc k ) ( lemma2 {_} {ltd} ) lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ - lemma with prev {ord→od x₁} lemma0 lemma1 - ... | t = {!!} + lemma = trans (cong (λ k → nat→ω k) lemma2) ( prev {ord→od x₁} lemma0 lemma1 ) ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t