Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/ZProduct.agda @ 1298:2c34f2b554cf current

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replace and filter projection fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 03 Jun 2023 17:31:17 +0900
parents ad9ed7c4a0b3
children 47d3cc596d68
comparison
equal deleted inserted replaced
1297:ad9ed7c4a0b3 1298:2c34f2b554cf
265 zp02 : {z : Ordinal } → odef (ZFP a B) z → z ≡ & < * x , * b > → odef a x 265 zp02 : {z : Ordinal } → odef (ZFP a B) z → z ≡ & < * x , * b > → odef a x
266 zp02 {.(& < * _ , * _ >)} (ab-pair {a1} {b1} aa1 bb1) eq = subst (λ k → odef a k) (*≡*→≡ zp03) aa1 where 266 zp02 {.(& < * _ , * _ >)} (ab-pair {a1} {b1} aa1 bb1) eq = subst (λ k → odef a k) (*≡*→≡ zp03) aa1 where
267 zp03 : * a1 ≡ * x 267 zp03 : * a1 ≡ * x
268 zp03 = proj1 (prod-≡ (&≡&→≡ eq)) 268 zp03 = proj1 (prod-≡ (&≡&→≡ eq))
269 269
270 ZP-proj1-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj1 A B (* z) zab ≡ od∅ → z ≡ & od∅
271 ZP-proj1-0 {A} {B} {z} {zab} eq = uf10 where
272 uf10 : z ≡ & od∅
273 uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where
274 uf11 : {y : Ordinal } → odef (* z) y → ⊥
275 uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ1 pqy)) eq uf12 ) ) where
276 pqy : odef (ZFP A B) y
277 pqy = zab zy
278 uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >)
279 uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy
280 uf12 : odef (ZP-proj1 A B (* z) zab) (zπ1 pqy)
281 uf12 = record { b = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 }
282
270 record ZP2 (A B C : HOD) ( cab : C ⊆ ZFP A B ) (b : Ordinal) : Set n where 283 record ZP2 (A B C : HOD) ( cab : C ⊆ ZFP A B ) (b : Ordinal) : Set n where
271 field 284 field
272 a : Ordinal 285 a : Ordinal
273 aa : odef A a 286 aa : odef A a
274 bb : odef B b 287 bb : odef B b
275 c∋ab : odef C (& < * a , * b > ) 288 c∋ab : odef C (& < * a , * b > )
276 289
277 ZP-proj2 : (A B C : HOD) → C ⊆ ZFP A B → HOD 290 ZP-proj2 : (A B C : HOD) → C ⊆ ZFP A B → HOD
278 ZP-proj2 A B C cab = record { od = record { def = λ x → ZP2 A B C cab x } ; odmax = & B ; <odmax = λ lt → odef< (ZP2.bb lt) } 291 ZP-proj2 A B C cab = record { od = record { def = λ x → ZP2 A B C cab x } ; odmax = & B ; <odmax = λ lt → odef< (ZP2.bb lt) }
292
293 ZP-proj2⊆ZFP : {A B C : HOD} → {cab : C ⊆ ZFP A B} → C ⊆ ZFP A (ZP-proj2 A B C cab)
294 ZP-proj2⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc
295 ... | ab-pair {a} {b} aa bb = ab-pair aa record { a = _ ; aa = aa ; bb = bb ; c∋ab = cc }
296
297 ZP-proj2=rev : {A B a m : HOD} {b : Ordinal } → {cab : m ⊆ ZFP A B} → odef A b → a ⊆ B → m ≡ ZFP A a → a ≡ ZP-proj2 A B m cab
298 ZP-proj2=rev {A} {B} {a} {m} {b} {cab} bb a⊆A refl = ==→o≡ record { eq→ = zp00 ; eq← = zp01 } where
299 zp00 : {x : Ordinal } → odef a x → ZP2 A B (ZFP A a ) cab x
300 zp00 {x} ax = record { a = _ ; aa = bb ; bb = a⊆A ax ; c∋ab = ab-pair bb ax }
301 zp01 : {x : Ordinal } → ZP2 A B (ZFP A a ) cab x → odef a x
302 zp01 {x} record { a = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = zp02 c∋ab refl where
303 zp02 : {z : Ordinal } → odef (ZFP A a ) z → z ≡ & < * b , * x > → odef a x
304 zp02 {.(& < * _ , * _ >)} (ab-pair {a1} {b1} aa1 bb1) eq = subst (λ k → odef a k) (*≡*→≡ zp03) bb1 where
305 zp03 : * b1 ≡ * x
306 zp03 = proj2 (prod-≡ (&≡&→≡ eq))
307
308 ZP-proj2-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj2 A B (* z) zab ≡ od∅ → z ≡ & od∅
309 ZP-proj2-0 {A} {B} {z} {zab} eq = uf10 where
310 uf10 : z ≡ & od∅
311 uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where
312 uf11 : {y : Ordinal } → odef (* z) y → ⊥
313 uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ2 pqy)) eq uf12 ) ) where
314 pqy : odef (ZFP A B) y
315 pqy = zab zy
316 uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >)
317 uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy
318 uf12 : odef (ZP-proj2 A B (* z) zab) (zπ2 pqy)
319 uf12 = record { a = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 }
279 320
280 record Func (A B : HOD) : Set n where 321 record Func (A B : HOD) : Set n where
281 field 322 field
282 func : {x : Ordinal } → odef A x → Ordinal 323 func : {x : Ordinal } → odef A x → Ordinal
283 is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax ) 324 is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax )
466 record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ⟪ c∋ab1 , subst (λ k → odef D k) (sym zs02) c∋ab2 ⟫ ; x=ba = x=ba } where 507 record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ⟪ c∋ab1 , subst (λ k → odef D k) (sym zs02) c∋ab2 ⟫ ; x=ba = x=ba } where
467 zs02 : & < * a , * b > ≡ & < * a' , * b' > 508 zs02 : & < * a , * b > ≡ & < * a' , * b' >
468 zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba)))))) 509 zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba))))))
469 (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba)))))) 510 (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba))))))
470 511
512 ZPmirror-neg : {A B C D : HOD} → {cdab : (C ＼ D) ⊆ ZFP A B } {cab : C ⊆ ZFP A B } {dab : D ⊆ ZFP A B }
513 → ZPmirror A B (C ＼ D) cdab ≡ ZPmirror A B C cab ＼ ZPmirror A B D dab
514 ZPmirror-neg {A} {B} {C} {D} {cdab} {cab} {dab} = ==→o≡ record { eq→ = za08 ; eq← = za10 } where
515 za08 : {x : Ordinal} → ZPC A B (C ＼ D) cdab x → odef (ZPmirror A B C cab ＼ ZPmirror A B D dab) x
516 za08 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } =
517 ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = proj1 c∋ab ; x=ba = x=ba } , za09 ⟫ where
518 za09 : ¬ odef (ZPmirror A B D dab) x
519 za09 zd = ⊥-elim ( proj2 c∋ab (subst (λ k → odef D k) (sym zs02) (ZPC.c∋ab zd) ) ) where
520 x=ba' = ZPC.x=ba zd
521 zs02 : & < * a , * b > ≡ & < * (ZPC.a zd) , * (ZPC.b zd) >
522 zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba' ) x=ba))))))
523 (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba' ) x=ba))))))
524 za10 : {x : Ordinal} → odef (ZPmirror A B C cab ＼ ZPmirror A B D dab) x → ZPC A B (C ＼ D) cdab x
525 za10 {x} ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } , neg ⟫ =
526 record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ⟪ c∋ab , za11 ⟫ ; x=ba = x=ba } where
527 za11 : ¬ odef D (& < * a , * b >)
528 za11 zd = ⊥-elim (neg record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = zd ; x=ba = x=ba })
529
530
531 ZPmirror-whole : {A B : HOD} → ZPmirror A B (ZFP A B) (λ x → x) ≡ ZFP B A
532 ZPmirror-whole {A} {B} = ==→o≡ record { eq→ = za12 ; eq← = za13 } where
533 za12 : {x : Ordinal} → ZPC A B (ZFP A B) (λ x₁ → x₁) x → ZFProduct B A x
534 za12 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = subst (λ k → ZFProduct B A k) (sym x=ba) (ab-pair bb aa)
535 za13 : {x : Ordinal} → ZFProduct B A x → ZPC A B (ZFP A B) (λ x₁ → x₁) x
536 za13 {x} (ab-pair {b} {a} bb aa) = record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ab-pair aa bb ; x=ba = refl }
537
538 ZPmirror-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZPmirror A B (* z) zab ≡ od∅ → z ≡ & od∅
539 ZPmirror-0 {A} {B} {z} {zab} eq = uf10 where
540 uf10 : z ≡ & od∅
541 uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where
542 uf11 : {y : Ordinal } → odef (* z) y → ⊥
543 uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (& < * (zπ2 pqy) , * (zπ1 pqy) >) ) eq uf12 ) ) where
544 pqy : odef (ZFP A B) y
545 pqy = zab zy
546 uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >)
547 uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy
548 uf12 : odef (ZPmirror A B (* z) zab) (& < * (zπ2 pqy) , * (zπ1 pqy) > )
549 uf12 = record { a = _ ; b = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 ; x=ba = refl }
471 550
472 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 ) 551 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 )
473 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where 552 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where
474 zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x 553 zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x
475 zfp00 (ab-pair ⟪ pa , pb ⟫ qx) = ⟪ ab-pair pa qx , ab-pair pb qx ⟫ 554 zfp00 (ab-pair ⟪ pa , pb ⟫ qx) = ⟪ ab-pair pa qx , ab-pair pb qx ⟫