Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 253:0446b6c5e7bc
proudct uniquness done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Aug 2019 16:08:46 +0900 |
| parents | 8a58e2cd1f55 |
| children | 2ea2a19f9cd6 |
| files | cardinal.agda |
| diffstat | 1 files changed, 6 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/cardinal.agda Thu Aug 29 03:03:04 2019 +0900 +++ b/cardinal.agda Thu Aug 29 16:08:46 2019 +0900 @@ -125,8 +125,12 @@ p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > p-iso1 {ox} {oy} = pair ox oy -postulate - p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x +p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x +p-iso {x} p = ord≡→≡ (lemma2 p) where + lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op + lemma (pair ox oy) = refl + lemma2 : { x : OD } → (p : ZFProduct ∋ x ) → od→ord < ord→od (π1 p) , ord→od (π2 p) > ≡ od→ord x + lemma2 {x} p = lemma p ∋-p : (A x : OD ) → Dec ( A ∋ x )