Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 252:8a58e2cd1f55
give up product uniquness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Aug 2019 03:03:04 +0900 |
| parents | 9e0125b06e76 |
| children | 0446b6c5e7bc |
| files | cardinal.agda |
| diffstat | 1 files changed, 5 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/cardinal.agda Thu Aug 29 01:04:52 2019 +0900 +++ b/cardinal.agda Thu Aug 29 03:03:04 2019 +0900 @@ -119,43 +119,15 @@ od→ord < ord→od (od→ord x) , ord→od (od→ord y) > ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ od→ord < x , y > - ∎ ) - - -lemma44 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >) -lemma44 {ox} {oy} = pair ox oy - -lemma55 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > -lemma55 {ox} {oy} = pair ox oy - -lemma66 : {ox oy : Ordinal } → pair ( pi1 ( pair ox oy )) ( pi2 ( pair ox oy )) ≡ pair ox oy -lemma66 = refl - -lemma77 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od (pi1 ( pair ox oy )) , ord→od (pi2 ( pair ox oy )) > ≡ ZFProduct ∋ < ord→od ox , ord→od oy > -lemma77 = refl + ∎ ) -p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x -p-iso {x} p = {!!} where - -pair-iso : {op ox oy : Ordinal} (x : ord-pair (od→ord < ord→od ox , ord→od oy >) ) → pi1 x ≡ ox → pi2 x ≡ oy → x ≡ pair ox oy -pair-iso (pair ox oy) = {!!} +p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > +p-iso1 {ox} {oy} = pair ox oy -p-iso3 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → p ≡ pair ox oy -p-iso3 {ox} {oy} p with p-iso p -... | eq with prod-eq ( ord→== (cong (λ k → od→ord k) eq ) ) -... | record { proj1 = eq1 ; proj2 = eq2 } = lemma eq1 eq2 where - lemma : ord→od (pi1 p) ≡ ord→od ox → ord→od (pi2 p) ≡ ord→od oy → p ≡ pair ox oy - lemma eq1 eq2 with od≡→≡ eq1 | od≡→≡ eq2 - ... | eq1' | eq2' = pair-iso {od→ord < ord→od ox , ord→od oy >} {ox} {oy} p eq1' eq2' +postulate + p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x -p-iso2 : { ox oy : Ordinal } → p-cons (ord→od ox) (ord→od oy) ≡ pair ox oy -p-iso2 {ox} {oy} = p-iso3 (p-cons (ord→od ox) (ord→od oy)) - -p-iso1 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ < ord→od ox , ord→od oy > -p-iso1 {x} {y} p with p-cons (ord→od (π1 p)) (ord→od (π2 p)) -... | t with p-iso3 p | p-iso3 t -... | refl | refl = refl ∋-p : (A x : OD ) → Dec ( A ∋ x ) ∋-p A x with p∨¬p ( A ∋ x )