Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/ZProduct.agda @ 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 |
comparison
equal
deleted
inserted
replaced
1274:b15dd4438d50 | 1275:e7743ac5a070 |
---|---|
231 ; fiso→ = λ x lt → refl | 231 ; fiso→ = λ x lt → refl |
232 } | 232 } |
233 | 233 |
234 ZFPsym : (A B : HOD) → OrdBijection (& (ZFP A B)) (& (ZFP B A)) | 234 ZFPsym : (A B : HOD) → OrdBijection (& (ZFP A B)) (& (ZFP B A)) |
235 ZFPsym A B = record { | 235 ZFPsym A B = record { |
236 fun← = λ xy ab → & < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) > | 236 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 )) |
237 ; fun→ = λ xy ba → & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) > | 237 ; 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 )) |
238 ; funB = λ xy ab → subst (λ k → odef k (& | 238 ; funB = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl |
239 < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) >)) | 239 (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab)) |
240 (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ab)) (zp1 (subst (λ k → odef k xy) *iso ab)) ) | 240 ; funA = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl |
241 ; funA = λ xy ba → subst (λ k → odef k (& | 241 (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab)) |
242 < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) >)) | 242 ; fiso← = λ xy ab → trans (cong getord ( HE.≅-to-≡ (exchg² refl (ab-pair ? ? ))) ) (trans ? (is-prod (subst (λ k → odef k xy) *iso ab)) ) |
243 (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ba)) (zp1 (subst (λ k → odef k xy) *iso ba)) ) | 243 ; fiso→ = λ xy ab → ? |
244 ; 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) )) | |
245 ? ) ( zp-iso (subst (λ k → odef k xy) *iso ba )) | |
246 ; fiso→ = λ xy ab → trans (cong₂ (λ j k → & < * j , * k > ) (proj2 (zp-iso0 ? )) (proj1 (zp-iso0 ? )) ) ( zp-iso (subst (λ k → odef k xy) *iso ab )) | |
247 } where | 244 } where |
248 lemma1 : {A B : HOD} {xy : Ordinal} → (ba : odef (* (& (ZFP B A))) xy) → odef (ZFP A B) ( | 245 getord : {A B : HOD} {xy : Ordinal} → odef (ZFP A B) xy → Ordinal |
249 & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) > ) | 246 getord {A} {B} {xy} ab = xy |
250 lemma1 {A} {B} {xy} ba = ? -- with subst (λ k → odef k xy ) *iso ba | 247 is-prod : {A B : HOD} {xy : Ordinal} → (ab : odef (ZFP A B) xy) → getord ab ≡ xy |
251 -- ... | ab-pair ax by = ? | 248 is-prod {A} {B} {xy} ab = refl |
249 exchg : {A B : HOD} {x y xy : Ordinal} → xy ≡ & < * x , * y > → odef (ZFP A B) xy → odef (ZFP B A) (& < * y , * x >) | |
250 exchg {A} {B} {x} {y} eq (ab-pair {a} {b} ax by ) = subst (λ k → odef (ZFP B A) k) | |
251 (cong₂ (λ j k → & < j , k >) (proj2 (prod-≡ lemma2 )) (proj1 (prod-≡ lemma2 )) ) (ab-pair by ax) where | |
252 lemma2 : < * a , * b > ≡ < * x , * y > | |
253 lemma2 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq) | |
254 exchg² : {A B : HOD} {x y xy : Ordinal} → (eq : xy ≡ & < * x , * y >) → (ab : odef (ZFP A B) xy) → exchg refl ( exchg eq ab ) ≅ ab | |
255 exchg² {A} {B} eq (ab-pair ax by ) = ? | |
252 | 256 |
253 | 257 |
254 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 ) | 258 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 ) |
255 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where | 259 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where |
256 zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x | 260 zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x |