Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 246:3506f53c7d83
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 26 Aug 2019 02:50:16 +0900 |
| parents | f0f9aede682f |
| children | d09437fcfc7c |
| files | cardinal.agda |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/cardinal.agda Mon Aug 26 02:34:14 2019 +0900 +++ b/cardinal.agda Mon Aug 26 02:50:16 2019 +0900 @@ -72,12 +72,12 @@ π1-cong : { p q : OD } → p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) -π1--iso : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ od→ord x -π1--iso {x} {y} p = {!!} where +π1--iso : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≅ od→ord x +π1--iso {x} {y} p = lemma (od→ord x) (od→ord y) {!!} {!!} refl where lemma1 : ( ox oy op : Ordinal ) → (p : ord-pair op) → op ≡ od→ord ( < ord→od ox , ord→od oy >) → p ≅ pair ox oy lemma1 ox oy op (pair x' y') eq = lemma34 {!!} {!!} {!!} - lemma : ( ox oy op : Ordinal ) → (p : ord-pair op ) → op ≡ od→ord ( < ord→od ox , ord→od oy > ) → pi1 p ≡ ox - lemma ox oy op (pair ox' oy') eq = {!!} + lemma : ( ox oy op : Ordinal ) → (p : ord-pair op ) → op ≡ od→ord ( < ord→od ox , ord→od oy > ) → pi1 p ≅ ox + lemma ox oy op p eq = {!!} -- HE.cong (λ k → pi1 k ) (lemma1 ox oy op p eq ) p-iso : { x : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x p-iso {x} {p} with p-cons (ord→od (π1 p)) (ord→od (π2 p))