Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1275:e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 05 Apr 2023 08:09:49 +0900 |
| parents | b15dd4438d50 |
| children | c077532416d9 |
| files | src/ZProduct.agda |
| diffstat | 1 files changed, 19 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ZProduct.agda Mon Apr 03 15:02:36 2023 +0900 +++ b/src/ZProduct.agda Wed Apr 05 08:09:49 2023 +0900 @@ -233,22 +233,26 @@ ZFPsym : (A B : HOD) → OrdBijection (& (ZFP A B)) (& (ZFP B A)) ZFPsym A B = record { - fun← = λ xy ab → & < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) > - ; fun→ = λ xy ba → & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) > - ; funB = λ xy ab → subst (λ k → odef k (& - < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) >)) - (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ab)) (zp1 (subst (λ k → odef k xy) *iso ab)) ) - ; funA = λ xy ba → subst (λ k → odef k (& - < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) >)) - (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ba)) (zp1 (subst (λ k → odef k xy) *iso ba)) ) - ; fiso← = λ xy ba → trans (cong₂ (λ j k → & < * j , * k > ) (proj2 (zp-iso0 {A} {B} {zπ2 (subst (λ k → odef k xy) *iso ba)} {zπ1 (subst (λ k → odef k xy) *iso ba)} (lemma1 ba) )) - ? ) ( zp-iso (subst (λ k → odef k xy) *iso ba )) - ; fiso→ = λ xy ab → trans (cong₂ (λ j k → & < * j , * k > ) (proj2 (zp-iso0 ? )) (proj1 (zp-iso0 ? )) ) ( zp-iso (subst (λ k → odef k xy) *iso ab )) + fun← = λ xy ab → getord ( exchg {A} {B} {zπ1 (subst (λ k → odef k xy) *iso ab)} {zπ2 (subst (λ k → odef k xy) *iso ab)} {_} refl (subst₂ (λ j k → odef j k) *iso (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) ab )) + ; fun→ = λ xy ba → getord ( exchg {B} {A} {zπ1 (subst (λ k → odef k xy) *iso ba)} {zπ2 (subst (λ k → odef k xy) *iso ba)} {_} refl (subst₂ (λ j k → odef j k) *iso (sym (zp-iso (subst (λ k → odef k xy) *iso ba))) ba )) + ; funB = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl + (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab)) + ; funA = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl + (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab)) + ; fiso← = λ xy ab → trans (cong getord ( HE.≅-to-≡ (exchg² refl (ab-pair ? ? ))) ) (trans ? (is-prod (subst (λ k → odef k xy) *iso ab)) ) + ; fiso→ = λ xy ab → ? } where - lemma1 : {A B : HOD} {xy : Ordinal} → (ba : odef (* (& (ZFP B A))) xy) → odef (ZFP A B) ( - & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) > ) - lemma1 {A} {B} {xy} ba = ? -- with subst (λ k → odef k xy ) *iso ba - -- ... | ab-pair ax by = ? + getord : {A B : HOD} {xy : Ordinal} → odef (ZFP A B) xy → Ordinal + getord {A} {B} {xy} ab = xy + is-prod : {A B : HOD} {xy : Ordinal} → (ab : odef (ZFP A B) xy) → getord ab ≡ xy + is-prod {A} {B} {xy} ab = refl + exchg : {A B : HOD} {x y xy : Ordinal} → xy ≡ & < * x , * y > → odef (ZFP A B) xy → odef (ZFP B A) (& < * y , * x >) + exchg {A} {B} {x} {y} eq (ab-pair {a} {b} ax by ) = subst (λ k → odef (ZFP B A) k) + (cong₂ (λ j k → & < j , k >) (proj2 (prod-≡ lemma2 )) (proj1 (prod-≡ lemma2 )) ) (ab-pair by ax) where + lemma2 : < * a , * b > ≡ < * x , * y > + lemma2 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq) + exchg² : {A B : HOD} {x y xy : Ordinal} → (eq : xy ≡ & < * x , * y >) → (ab : odef (ZFP A B) xy) → exchg refl ( exchg eq ab ) ≅ ab + exchg² {A} {B} eq (ab-pair ax by ) = ? ZFP∩ : {A B C : HOD} → ( ZFP (A ∩ B) C ≡ ZFP A C ∩ ZFP B C ) ∧ ( ZFP C (A ∩ B) ≡ ZFP C A ∩ ZFP C B )