Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/ZProduct.agda @ 1419:2da55d442e4f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jul 2023 06:19:03 +0900 |
| parents | 66a6804d867b |
| children | a7d46b1c2a70 |
| rev | line source |
|---|---|
| 431 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 | |
| 3 open import Level | |
| 4 open import Ordinals | |
| 1218 | 5 module ZProduct {n : Level } (O : Ordinals {n}) where |
| 431 | 6 |
| 7 open import logic | |
| 1279 | 8 import OD |
| 431 | 9 import ODUtil |
| 10 import OrdUtil | |
| 11 | |
| 12 open import Relation.Nullary | |
| 13 open import Relation.Binary | |
| 14 open import Data.Empty | |
| 15 open import Relation.Binary | |
| 16 open import Relation.Binary.Core | |
| 17 open import Relation.Binary.PropositionalEquality | |
| 1279 | 18 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 431 | 19 |
| 20 open OD O | |
| 21 open OD.OD | |
| 22 open OD.HOD | |
| 23 open ODAxiom odAxiom | |
| 24 | |
| 25 open Ordinals.Ordinals O | |
| 26 open Ordinals.IsOrdinals isOrdinal | |
| 1300 | 27 -- open Ordinals.IsNext isNext |
| 431 | 28 open OrdUtil O |
| 29 open ODUtil O | |
| 30 | |
| 31 open _∧_ | |
| 32 open _∨_ | |
| 33 open Bool | |
| 34 | |
| 35 open _==_ | |
| 36 | |
| 37 <_,_> : (x y : HOD) → HOD | |
| 38 < x , y > = (x , x ) , (x , y ) | |
| 39 | |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
40 ZFP<AB : {X Y x y : HOD} → X ∋ x → Y ∋ y → < x , y > ⊆ Power ( Union (X , Y )) |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
41 ZFP<AB {X} {Y} {x} {y} xx yy (case1 refl ) z lt with subst (λ k → odef k z) *iso lt |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
42 ... | case1 refl = record { owner = _ ; ao = case1 refl ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl xx } |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
43 ... | case2 refl = record { owner = _ ; ao = case1 refl ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl xx } |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
44 ZFP<AB {X} {Y} {x} {y} xx yy (case2 refl ) z lt with subst (λ k → odef k z) *iso lt |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
45 ... | case1 refl = record { owner = _ ; ao = case1 refl ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl xx } |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
46 ... | case2 refl = record { owner = _ ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl yy } |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
47 |
| 431 | 48 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x ) |
| 49 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where | |
| 1279 | 50 left : {z : Ordinal} → odef (x , y) z → odef (y , x) z |
| 431 | 51 left (case1 t) = case2 t |
| 52 left (case2 t) = case1 t | |
| 1279 | 53 right : {z : Ordinal} → odef (y , x) z → odef (x , y) z |
| 431 | 54 right (case1 t) = case2 t |
| 55 right (case2 t) = case1 t | |
| 56 | |
| 57 ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y | |
| 58 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq ) | |
| 59 | |
| 60 od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y | |
| 61 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq ) | |
| 62 | |
| 63 eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > | |
| 64 eq-prod refl refl = refl | |
| 65 | |
| 66 xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y | |
| 1279 | 67 xx=zy→x=y {x} {y} eq with trio< (& x) (& y) |
| 68 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) | |
| 431 | 69 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) |
| 70 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) | |
| 71 xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b | |
| 1279 | 72 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl) |
| 431 | 73 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) |
| 74 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) | |
| 75 | |
| 76 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) | |
| 77 prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where | |
| 78 lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y | |
| 79 lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq ) where | |
| 80 lemma3 : ( x , x ) =h= ( y , z ) | |
| 81 lemma3 = ==-trans eq exg-pair | |
| 82 lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y | |
| 83 lemma1 {x} {y} eq with eq← eq {& y} (case2 refl) | |
| 84 lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) | |
| 85 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) | |
| 86 lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z | |
| 87 lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl) | |
| 88 lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z | |
| 89 ... | refl with lemma2 (==-sym eq ) | |
| 90 ... | refl = refl | |
| 91 lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z | |
| 92 lemmax : x ≡ x' | |
| 1279 | 93 lemmax with eq→ eq {& (x , x)} (case1 refl) |
| 431 | 94 lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') |
| 95 lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' | |
| 96 ... | refl = lemma1 (ord→== s ) | |
| 97 lemmay : y ≡ y' | |
| 98 lemmay with lemmax | |
| 99 ... | refl with lemma4 eq -- with (x,y)≡(x,y') | |
| 100 ... | eq1 = lemma4 (ord→== (cong (λ k → & k ) eq1 )) | |
| 101 | |
| 1098 | 102 prod-≡ : { x x' y y' : HOD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) |
| 103 prod-≡ eq = prod-eq (ord→== (cong (&) eq )) | |
| 104 | |
| 431 | 105 -- |
| 1098 | 106 -- unlike ordered pair, ZFPair is not a HOD |
| 431 | 107 |
| 108 data ord-pair : (p : Ordinal) → Set n where | |
| 109 pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) ) | |
| 110 | |
| 1098 | 111 ZFPair : OD |
| 112 ZFPair = record { def = λ x → ord-pair x } | |
| 431 | 113 |
| 1285 | 114 -- _⊗_ : (A B : HOD) → HOD |
| 115 -- A ⊗ B = Union ( Replace' B (λ b lb → Replace' A (λ a la → < a , b > ) record { ≤COD = ? } ) ? ) | |
| 431 | 116 |
| 1285 | 117 -- product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b > |
| 118 -- product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2 } where | |
| 119 -- lemma1 : odef (Replace' B (λ b₁ lb → Replace' A (λ a₁ la → < a₁ , b₁ >) ? ) ? ) (& (Replace' A (λ a₁ la → < a₁ , b >) ? )) | |
| 120 -- lemma1 = ? -- replacement← B b B∋b ? | |
| 121 -- lemma2 : odef (Replace' A (λ a₁ la → < a₁ , b >) ? ) (& < a , b >) | |
| 122 -- lemma2 = ? -- replacement← A a A∋a ? | |
| 431 | 123 |
| 1098 | 124 data ZFProduct (A B : HOD) : (p : Ordinal) → Set n where |
| 125 ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) ) | |
| 126 | |
| 431 | 127 ZFP : (A B : HOD) → HOD |
| 1279 | 128 ZFP A B = record { od = record { def = λ x → ZFProduct A B x } |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
129 ; odmax = osuc (& ( Power ( Union (A , B )))) ; <odmax = λ {y} px → lemma0 px } |
| 431 | 130 where |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
131 lemma0 : {x : Ordinal } → ZFProduct A B x → x o< osuc (& ( Power ( Union (A , B )) )) |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
132 lemma0 ( ab-pair {a} {b} ax by ) = lemma1 where |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
133 lemma1 : & < * a , * b > o< osuc (& (Power (Union (A , B)))) |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
134 lemma1 = ⊆→o≤ (ZFP<AB (subst (λ k → odef A k) (sym &iso) ax) (subst (λ k → odef B k) (sym &iso) by) ) |
| 1098 | 135 |
| 136 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b → ZFP A B ∋ < a , b > | |
| 1279 | 137 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) |
| 431 | 138 |
| 1104 | 139 zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal |
| 140 zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a | |
| 141 | |
| 142 zp1 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef A (zπ1 zx) | |
| 143 zp1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = aa | |
| 144 | |
| 145 zπ2 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal | |
| 146 zπ2 (ab-pair {a} {b} aa bb) = b | |
| 147 | |
| 148 zp2 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef B (zπ2 zx) | |
| 149 zp2 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = bb | |
| 150 | |
| 151 zp-iso : { A B : HOD } → {x : Ordinal } → (p : odef (ZFP A B) x ) → & < * (zπ1 p) , * (zπ2 p) > ≡ x | |
| 152 zp-iso {A} {B} {_} (ab-pair {a} {b} aa bb) = refl | |
| 153 | |
| 1216 | 154 zp-iso1 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (* (zπ1 p) ≡ (* a)) ∧ (* (zπ2 p) ≡ (* b)) |
| 155 zp-iso1 {A} {B} {a} {b} pab = prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) zz11) ) where | |
| 156 zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b > | |
| 157 zz11 = zp-iso pab | |
| 158 | |
| 1223 | 159 zp-iso0 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (zπ1 p ≡ a) ∧ (zπ2 p ≡ b) |
| 1279 | 160 zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) )) |
| 1223 | 161 , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) ) ⟫ |
| 162 | |
| 1285 | 163 -- ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x |
| 164 -- ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by) | |
| 1098 | 165 |
| 1285 | 166 -- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x) |
| 167 -- ⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where | |
| 168 -- zfp02 : Replace' A (λ z lz → < z , * a >) record { ≤COD = ? } ≡ * owner | |
| 169 -- zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa )) | |
| 170 -- zfp01 : odef (ZFP A B) (& x) | |
| 171 -- zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox | |
| 172 -- ... | t = ? | |
| 173 -- -- ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) | |
| 431 | 174 |
| 1276 | 175 ZPI1 : (A B : HOD) → HOD |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
176 ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) {Union A} record { ≤COD = lemma1 } where |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
177 lemma1 : {x : Ordinal } (lt : odef (ZFP A B) x) → * (zπ1 lt) ⊆ Union A |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
178 lemma1 (ab-pair {a} {b} aa bb) {x} ax = record { owner = _ ; ao = aa ; ox = ax } |
| 1105 | 179 |
| 1276 | 180 ZPI2 : (A B : HOD) → HOD |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
181 ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) {Union B} record { ≤COD = lemma1 } where |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
182 lemma1 : {x : Ordinal } (lt : odef (ZFP A B) x) → * (zπ2 lt) ⊆ Union B |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
183 lemma1 (ab-pair {a} {b} aa bb) {x} bx = record { owner = _ ; ao = bb ; ox = bx } |
| 1098 | 184 |
| 1218 | 185 ZFProj1-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a |
| 186 ZFProj1-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 187 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) | |
| 1105 | 188 |
| 1218 | 189 ZFProj2-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b |
| 190 ZFProj2-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 191 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) | |
| 1105 | 192 |
| 1278 | 193 ZPI1-iso : (A B : HOD) → {b : Ordinal } → odef B b → ZPI1 A B ≡ A |
| 194 ZPI1-iso P Q {q} qq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where | |
| 195 ty21 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >))) | |
| 196 ty21 pz qz = subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz ) | |
| 197 ty32 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → zπ1 (ty21 pz qz) ≡ a | |
| 198 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where | |
| 199 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a | |
| 200 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 201 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) | |
| 202 ty20 : {x : Ordinal} → odef (ZPI1 P Q) x → odef P x | |
| 203 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef P k) a=x pz where | |
| 204 ty24 : * x ≡ * a | |
| 205 ty24 = begin | |
| 206 * x ≡⟨ cong (*) x=ψz ⟩ | |
| 207 _ ≡⟨ *iso ⟩ | |
| 208 * (zπ1 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz))) ≡⟨ cong (*) (ty32 pz qz) ⟩ | |
| 209 * a ∎ where open ≡-Reasoning | |
| 210 a=x : a ≡ x | |
| 211 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) | |
| 212 ty22 : {x : Ordinal} → odef P x → odef (ZPI1 P Q) x | |
| 213 ty22 {x} px = record { z = _ ; az = ab-pair px qq ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where | |
| 214 ty12 : * x ≡ * (zπ1 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair px qq ))) | |
| 215 ty12 = begin | |
| 216 * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩ | |
| 217 * (zπ1 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair px qq ))) ∎ where open ≡-Reasoning | |
| 218 | |
| 219 ZPI2-iso : (A B : HOD) → {b : Ordinal } → odef A b → ZPI2 A B ≡ B | |
| 220 ZPI2-iso P Q {p} pp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where | |
| 221 ty21 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >))) | |
| 222 ty21 pz qz = subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz ) | |
| 223 ty32 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → zπ2 (ty21 pz qz) ≡ b | |
| 224 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where | |
| 225 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b | |
| 226 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 227 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) | |
| 228 ty20 : {x : Ordinal} → odef (ZPI2 P Q) x → odef Q x | |
| 229 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef Q k) a=x qz where | |
| 230 ty24 : * x ≡ * b | |
| 231 ty24 = begin | |
| 232 * x ≡⟨ cong (*) x=ψz ⟩ | |
| 233 _ ≡⟨ *iso ⟩ | |
| 234 * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz))) ≡⟨ cong (*) (ty32 pz qz) ⟩ | |
| 235 * b ∎ where open ≡-Reasoning | |
| 236 a=x : b ≡ x | |
| 237 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) | |
| 238 ty22 : {x : Ordinal} → odef Q x → odef (ZPI2 P Q) x | |
| 239 ty22 {x} qx = record { z = _ ; az = ab-pair pp qx ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where | |
| 240 ty12 : * x ≡ * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx))) | |
| 241 ty12 = begin | |
| 242 * x ≡⟨ sym (cong (*) (ty32 pp qx )) ⟩ | |
| 243 * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx ))) ∎ where open ≡-Reasoning | |
| 244 | |
| 1297 | 245 record ZP1 (A B C : HOD) ( cab : C ⊆ ZFP A B ) (a : Ordinal) : Set n where |
| 246 field | |
| 247 b : Ordinal | |
| 248 aa : odef A a | |
| 249 bb : odef B b | |
| 250 c∋ab : odef C (& < * a , * b > ) | |
| 251 | |
| 252 ZP-proj1 : (A B C : HOD) → C ⊆ ZFP A B → HOD | |
| 253 ZP-proj1 A B C cab = record { od = record { def = λ x → ZP1 A B C cab x } ; odmax = & A ; <odmax = λ lt → odef< (ZP1.aa lt) } | |
| 254 | |
| 255 ZP-proj1⊆ZFP : {A B C : HOD} → {cab : C ⊆ ZFP A B} → C ⊆ ZFP (ZP-proj1 A B C cab) B | |
| 256 ZP-proj1⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc | |
| 257 ... | ab-pair {a} {b} aa bb = ab-pair record { b = _ ; aa = aa ; bb = bb ; c∋ab = cc } bb | |
| 258 | |
| 259 ZP-proj1=rev : {A B a m : HOD} {b : Ordinal } → {cab : m ⊆ ZFP A B} → odef B b → a ⊆ A → m ≡ ZFP a B → a ≡ ZP-proj1 A B m cab | |
| 260 ZP-proj1=rev {A} {B} {a} {m} {b} {cab} bb a⊆A refl = ==→o≡ record { eq→ = zp00 ; eq← = zp01 } where | |
| 261 zp00 : {x : Ordinal } → odef a x → ZP1 A B (ZFP a B) cab x | |
| 262 zp00 {x} ax = record { b = _ ; aa = a⊆A ax ; bb = bb ; c∋ab = ab-pair ax bb } | |
| 263 zp01 : {x : Ordinal } → ZP1 A B (ZFP a B) cab x → odef a x | |
| 264 zp01 {x} record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = zp02 c∋ab refl where | |
| 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 | |
| 267 zp03 : * a1 ≡ * x | |
| 268 zp03 = proj1 (prod-≡ (&≡&→≡ eq)) | |
| 269 | |
|
1298
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
270 ZP-proj1-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj1 A B (* z) zab ≡ od∅ → z ≡ & od∅ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
271 ZP-proj1-0 {A} {B} {z} {zab} eq = uf10 where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
272 uf10 : z ≡ & od∅ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
273 uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
274 uf11 : {y : Ordinal } → odef (* z) y → ⊥ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
275 uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ1 pqy)) eq uf12 ) ) where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
276 pqy : odef (ZFP A B) y |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
277 pqy = zab zy |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
278 uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
279 uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
280 uf12 : odef (ZP-proj1 A B (* z) zab) (zπ1 pqy) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
281 uf12 = record { b = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 } |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
282 |
| 1297 | 283 record ZP2 (A B C : HOD) ( cab : C ⊆ ZFP A B ) (b : Ordinal) : Set n where |
| 284 field | |
| 285 a : Ordinal | |
| 286 aa : odef A a | |
| 287 bb : odef B b | |
| 288 c∋ab : odef C (& < * a , * b > ) | |
| 289 | |
| 290 ZP-proj2 : (A B C : HOD) → C ⊆ ZFP A B → HOD | |
| 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 | |
|
1298
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
293 ZP-proj2⊆ZFP : {A B C : HOD} → {cab : C ⊆ ZFP A B} → C ⊆ ZFP A (ZP-proj2 A B C cab) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
294 ZP-proj2⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
295 ... | ab-pair {a} {b} aa bb = ab-pair aa record { a = _ ; aa = aa ; bb = bb ; c∋ab = cc } |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
296 |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
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 |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
298 ZP-proj2=rev {A} {B} {a} {m} {b} {cab} bb a⊆A refl = ==→o≡ record { eq→ = zp00 ; eq← = zp01 } where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
299 zp00 : {x : Ordinal } → odef a x → ZP2 A B (ZFP A a ) cab x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
300 zp00 {x} ax = record { a = _ ; aa = bb ; bb = a⊆A ax ; c∋ab = ab-pair bb ax } |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
301 zp01 : {x : Ordinal } → ZP2 A B (ZFP A a ) cab x → odef a x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
302 zp01 {x} record { a = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = zp02 c∋ab refl where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
303 zp02 : {z : Ordinal } → odef (ZFP A a ) z → z ≡ & < * b , * x > → odef a x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
304 zp02 {.(& < * _ , * _ >)} (ab-pair {a1} {b1} aa1 bb1) eq = subst (λ k → odef a k) (*≡*→≡ zp03) bb1 where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
305 zp03 : * b1 ≡ * x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
306 zp03 = proj2 (prod-≡ (&≡&→≡ eq)) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
307 |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
308 ZP-proj2-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj2 A B (* z) zab ≡ od∅ → z ≡ & od∅ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
309 ZP-proj2-0 {A} {B} {z} {zab} eq = uf10 where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
310 uf10 : z ≡ & od∅ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
311 uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
312 uf11 : {y : Ordinal } → odef (* z) y → ⊥ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
313 uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ2 pqy)) eq uf12 ) ) where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
314 pqy : odef (ZFP A B) y |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
315 pqy = zab zy |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
316 uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
317 uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
318 uf12 : odef (ZP-proj2 A B (* z) zab) (zπ2 pqy) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
319 uf12 = record { a = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 } |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
320 |
| 1279 | 321 record Func (A B : HOD) : Set n where |
| 322 field | |
| 323 func : {x : Ordinal } → odef A x → Ordinal | |
| 324 is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax ) | |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
325 fodmax : RXCod A (Power (Union (A , B))) (λ x ax → < x , * (func ax) >) |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
326 fodmax = record { ≤COD = λ {x} ax → lemma1 ax } where |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
327 lemma1 : {x : HOD} → (ax : odef A (& x)) → < x , * (func ax) > ⊆ Power (Union (A , B)) |
|
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
328 lemma1 {x} ax = ZFP<AB ax (subst (λ k → odef B k) (sym &iso) ( is-func ax ) ) |
| 1279 | 329 |
| 330 data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where | |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
331 felm : (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > ) (Func.fodmax F) )) |
| 1279 | 332 |
| 333 FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B | |
| 334 FuncHOD→F {A} {B} (felm F) = F | |
| 335 | |
|
1292
f29970636e01
ZProduct with Replace sup
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1285
diff
changeset
|
336 FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡ Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > ) (Func.fodmax (FuncHOD→F fc) ) |
| 1279 | 337 FuncHOD=R {A} {B} (felm F) = *iso |
| 338 | |
| 339 -- | |
| 340 -- Set of All function from A to B | |
| 341 -- | |
| 342 | |
| 343 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | |
| 344 | |
| 345 Funcs : (A B : HOD) → HOD | |
| 346 Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B)) | |
| 347 ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where | |
| 348 lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x | |
| 349 lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx | |
| 350 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k) | |
| 351 (sym x=ψz) lemma4 where | |
| 352 lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > ) | |
| 353 lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az)) | |
| 354 | |
| 1300 | 355 TwoHOD : HOD |
| 356 TwoHOD = ( od∅ , ( od∅ , od∅ )) | |
| 357 | |
| 358 Aleph1 : HOD | |
| 359 Aleph1 = Funcs Omega TwoHOD | |
| 360 | |
| 1279 | 361 record Injection (A B : Ordinal ) : Set n where |
| 362 field | |
| 363 i→ : (x : Ordinal ) → odef (* A) x → Ordinal | |
| 364 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt ) | |
| 1303 | 365 inject : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y |
| 1279 | 366 |
| 367 record HODBijection (A B : HOD ) : Set n where | |
| 368 field | |
| 369 fun← : (x : Ordinal ) → odef A x → Ordinal | |
| 370 fun→ : (x : Ordinal ) → odef B x → Ordinal | |
| 371 funB : (x : Ordinal ) → ( lt : odef A x ) → odef B ( fun← x lt ) | |
| 372 funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun→ x lt ) | |
| 373 fiso← : (x : Ordinal ) → ( lt : odef B x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x | |
| 374 fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x | |
| 375 | |
| 376 hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b | |
| 377 hodbij-refl {a} refl = record { | |
| 378 fun← = λ x _ → x | |
| 379 ; fun→ = λ x _ → x | |
| 380 ; funB = λ x lt → lt | |
| 381 ; funA = λ x lt → lt | |
| 382 ; fiso← = λ x lt → refl | |
| 383 ; fiso→ = λ x lt → refl | |
| 384 } | |
| 385 | |
| 386 pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) → | |
| 387 (zπ1 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ1 ab ))) ∧ | |
| 388 (zπ2 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ2 ab ))) | |
| 389 pj12 A B (ab-pair {x} {y} ax by) = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (prod-≡ pj24 ))) | |
| 390 , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (prod-≡ pj24))) ⟫ where | |
| 391 pj22 : odef (ZFP A B) (& (* (& < * x , * y >))) | |
| 392 pj22 = subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by) | |
| 393 pj23 : & < * (zπ1 pj22 ) , * (zπ2 pj22) > ≡ & (* (& < * x , * y >) ) | |
| 394 pj23 = zp-iso pj22 | |
| 395 pj24 : < * (zπ1 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) , * (zπ2 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) > | |
| 396 ≡ < * (& (* x)) , * (& (* y)) > | |
| 397 pj24 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( trans pj23 (trans &iso | |
| 398 (sym (cong (&) (cong₂ (λ j k → < j , k >) *iso *iso)) )))) | |
| 399 pj02 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab) | |
| 400 pj02 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj2 (pj12 A B ab))) (sym &iso)) } | |
| 401 pj01 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI1 A B) (zπ1 ab) | |
| 402 pj01 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj1 (pj12 A B ab))) (sym &iso)) } | |
| 403 | |
| 404 pj2 : (A B : HOD) (x : Ordinal) (lt : odef (ZFP A B) x) → odef (ZFP (ZPI2 A B) (ZPI1 A B)) (& < * (zπ2 lt) , * (zπ1 lt) >) | |
| 405 pj2 A B x ab = ab-pair (pj02 A B x ab) (pj01 A B x ab) | |
| 406 | |
| 407 aZPI1 : (A B : HOD) {y : Ordinal} → odef (ZPI1 A B) y → odef A y | |
| 408 aZPI1 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef A k) (trans ( | |
| 409 trans (sym &iso) (trans (sym (proj1 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp1 az ) | |
| 410 aZPI2 : (A B : HOD) {y : Ordinal} → odef (ZPI2 A B) y → odef B y | |
| 411 aZPI2 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef B k) (trans ( | |
| 412 trans (sym &iso) (trans (sym (proj2 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp2 az ) | |
| 413 | |
| 414 pj1 : (A B : HOD) (x : Ordinal) (lt : odef (ZFP (ZPI2 A B) (ZPI1 A B)) x) → odef (ZFP A B) (& < * (zπ2 lt) , * (zπ1 lt) >) | |
| 415 pj1 A B _ (ab-pair ax by) = ab-pair (aZPI1 A B by) (aZPI2 A B ax) | |
| 1278 | 416 |
| 417 ZFPsym1 : (A B : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B)) | |
| 418 ZFPsym1 A B = record { | |
| 1276 | 419 fun← = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) > |
| 420 ; fun→ = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) > | |
| 1277 | 421 ; funB = pj2 A B |
| 422 ; funA = pj1 A B | |
| 1278 | 423 ; fiso← = λ xy ab → pj00 A B ab |
| 1277 | 424 ; fiso→ = λ xy ab → zp-iso ab |
| 1278 | 425 } where |
| 1279 | 426 pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) |
| 1278 | 427 → & < * (zπ1 ab) , * (zπ2 ab) > ≡ & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > |
| 428 pj10 A B {.(& < * _ , * _ >)} (ab-pair ax by ) = refl | |
| 1279 | 429 pj00 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) |
| 430 → & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > ≡ xy | |
| 1278 | 431 pj00 A B {xy} ab = trans (sym (pj10 A B ab)) (zp-iso {ZPI2 A B} {ZPI1 A B} {xy} ab) |
| 1274 | 432 |
| 1279 | 433 -- |
| 434 -- Bijection of (A x B) and (B x A) requires one element or axiom of choice | |
| 435 -- | |
| 1278 | 436 ZFPsym : (A B : HOD) → {a b : Ordinal } → odef A a → odef B b → HODBijection (ZFP A B) (ZFP B A) |
| 437 ZFPsym A B aa bb = subst₂ ( λ j k → HODBijection (ZFP A B) (ZFP j k)) (ZPI2-iso A B aa) (ZPI1-iso A B bb) ( ZFPsym1 A B ) | |
| 1274 | 438 |
| 1294 | 439 ⊆-ZFP : {A B : HOD} {X Y x y : HOD} → X ⊆ A → Y ⊆ B → ZFP X Y ⊆ ZFP A B |
| 440 ⊆-ZFP {A} {B} {X} {y} X<A Y<B (ab-pair xx yy) = ab-pair (X<A xx) (Y<B yy) | |
| 441 | |
| 442 record ZPC (A B C : HOD) ( cab : C ⊆ ZFP A B ) (x : Ordinal) : Set n where | |
| 443 field | |
| 444 a b : Ordinal | |
| 445 aa : odef A a | |
| 446 bb : odef B b | |
| 447 c∋ab : odef C (& < * a , * b > ) | |
| 448 x=ba : x ≡ & < * b , * a > | |
| 449 | |
| 450 ZPmirror : (A B C : HOD) → C ⊆ ZFP A B → HOD | |
| 451 ZPmirror A B C cab = record { od = record { def = λ x → ZPC A B C cab x } ; odmax = osuc (& (Power (Union (B , A)))) ; <odmax = lemma0 } where | |
| 452 lemma0 : {x : Ordinal } → ZPC A B C cab x → x o< osuc (& ( Power ( Union (B , A )) )) | |
| 453 lemma0 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = subst (λ k → k o< _) (sym x=ba) lemma1 where | |
| 454 lemma1 : & < * b , * a > o< osuc (& (Power (Union (B , A)))) | |
| 455 lemma1 = ⊆→o≤ (ZFP<AB (subst (λ k → odef B k) (sym &iso) bb) (subst (λ k → odef A k) (sym &iso) aa) ) | |
| 456 | |
| 1295 | 457 ZPmirror⊆ZFPBA : (A B C : HOD) → (cab : C ⊆ ZFP A B ) → ZPmirror A B C cab ⊆ ZFP B A |
| 458 ZPmirror⊆ZFPBA A B C cab {z} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } | |
| 459 = subst (λ k → odef (ZFP B A) k) (sym x=ba) lemma2 where | |
| 460 lemma2 : odef (ZFP B A) (& < * b , * a > ) | |
| 461 lemma2 = ZFP→ (subst (λ k → odef B k ) (sym &iso) bb) (subst (λ k → odef A k ) (sym &iso) aa) | |
| 462 | |
| 1294 | 463 ZPmirror-iso : (A B C : HOD) → (cab : C ⊆ ZFP A B ) → ( {x y : HOD} → C ∋ < x , y > → ZPmirror A B C cab ∋ < y , x > ) |
| 464 ∧ ( {x y : HOD} → ZPmirror A B C cab ∋ < y , x > → C ∋ < x , y > ) | |
| 465 ZPmirror-iso A B C cab = ⟪ zs00 refl , zs01 ⟫ where | |
| 466 zs00 : {x y : HOD} → {z : Ordinal} → z ≡ & < x , y > → odef C z → ZPmirror A B C cab ∋ < y , x > | |
| 467 zs00 {x} {y} {z} eq cz with cab cz | |
| 468 ... | ab-pair {a} {b} aa bb = record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = cz | |
| 469 ; x=ba = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))))) | |
| 470 (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))))) } | |
| 471 zs01 : {x y : HOD} → ZPmirror A B C cab ∋ < y , x > → C ∋ < x , y > | |
| 472 zs01 {x} {y} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = subst (λ k → odef C k ) zs02 c∋ab where | |
| 473 zs02 : & < * a , * b > ≡ & < x , y > | |
| 474 zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) x=ba))))) | |
| 475 (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) x=ba))))) | |
| 476 | |
| 1297 | 477 ZPmirror-rev : {A B C m : HOD} → {cab : C ⊆ ZFP A B } → ZPmirror A B C cab ≡ m |
| 478 → {m⊆Z : m ⊆ ZFP B A } → ZPmirror B A m m⊆Z ≡ C | |
| 479 ZPmirror-rev {A} {B} {C} {m} {cab} eq {m⊆Z} = ==→o≡ record { eq→ = zs02 ; eq← = zs04 } where | |
| 480 zs02 : {x : Ordinal} → ZPC B A m m⊆Z x → odef C x | |
| 481 zs02 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } with subst (λ k → odef k (& < * a , * b > )) (sym eq) c∋ab | |
| 482 ... | record { a = b1 ; b = a1 ; aa = bb1 ; bb = aa1 ; c∋ab = c∋ab1 ; x=ba = x=ba1 } = subst (λ k → odef C k) zs03 c∋ab1 where | |
| 483 a=a1 : * a ≡ * a1 | |
| 484 a=a1 = proj1 (prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ba1))) | |
| 485 b=b1 : * b ≡ * b1 | |
| 486 b=b1 = proj2 (prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ba1))) | |
| 487 zs03 : & < * b1 , * a1 > ≡ x | |
| 488 zs03 = begin | |
| 489 & < * b1 , * a1 > ≡⟨ cong₂ (λ j k → & < j , k >) (sym b=b1) (sym a=a1) ⟩ | |
| 490 & < * b , * a > ≡⟨ sym x=ba ⟩ | |
| 491 x ∎ where open ≡-Reasoning | |
| 492 zs04 : {x : Ordinal} → odef C x → ZPC B A m m⊆Z x | |
| 493 zs04 {x} cx with cab cx | |
| 494 ... | ab-pair {a} {b} aa bb = record { a = b ; b = a ; aa = bb ; bb = aa | |
| 495 ; c∋ab = subst (λ k → odef k (& < * b , * a >)) eq zs05 ; x=ba = refl } where | |
| 496 zs05 : odef (ZPmirror A B C cab) (& < * b , * a >) | |
| 497 zs05 = record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = cx ; x=ba = refl } | |
| 498 | |
| 499 ZPmirror-⊆ : {A B C D : HOD} → (C⊆D : C ⊆ D) → {cab : C ⊆ ZFP A B } {dab : D ⊆ ZFP A B } → ZPmirror A B C cab ⊆ ZPmirror A B D dab | |
| 500 ZPmirror-⊆ {A} {B} {C} {D} C⊆D {cab} {dab} {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = | |
| 501 record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = C⊆D c∋ab ; x=ba = x=ba } | |
| 502 | |
| 503 ZPmirror-∩ : {A B C D : HOD} → {cdab : (C ∩ D) ⊆ ZFP A B } {cab : C ⊆ ZFP A B } {dab : D ⊆ ZFP A B } | |
| 504 → ZPmirror A B (C ∩ D) cdab ≡ ZPmirror A B C cab ∩ ZPmirror A B D dab | |
| 505 ZPmirror-∩ {A} {B} {C} {D} {cdab} {cab} {dab} = ==→o≡ record { eq→ = za06 ; eq← = za07 } where | |
| 506 za06 : ZPmirror A B (C ∩ D) cdab ⊆ ( ZPmirror A B C cab ∩ ZPmirror A B D dab ) | |
| 507 za06 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = ⟪ | |
| 508 record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = proj1 c∋ab ; x=ba = x=ba } , | |
| 509 record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = proj2 c∋ab ; x=ba = x=ba } ⟫ | |
| 510 za07 : ( ZPmirror A B C cab ∩ ZPmirror A B D dab ) ⊆ ZPmirror A B (C ∩ D) cdab | |
| 511 za07 {x} ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab1 ; x=ba = x=ba } , | |
| 512 record { a = a' ; b = b' ; aa = aa' ; bb = bb' ; c∋ab = c∋ab2 ; x=ba = x=ba' } ⟫ = | |
| 513 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 | |
| 514 zs02 : & < * a , * b > ≡ & < * a' , * b' > | |
| 515 zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba)))))) | |
| 516 (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba)))))) | |
| 517 | |
|
1298
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
518 ZPmirror-neg : {A B C D : HOD} → {cdab : (C ＼ D) ⊆ ZFP A B } {cab : C ⊆ ZFP A B } {dab : D ⊆ ZFP A B } |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
519 → ZPmirror A B (C ＼ D) cdab ≡ ZPmirror A B C cab ＼ ZPmirror A B D dab |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
520 ZPmirror-neg {A} {B} {C} {D} {cdab} {cab} {dab} = ==→o≡ record { eq→ = za08 ; eq← = za10 } where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
521 za08 : {x : Ordinal} → ZPC A B (C ＼ D) cdab x → odef (ZPmirror A B C cab ＼ ZPmirror A B D dab) x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
522 za08 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
523 ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = proj1 c∋ab ; x=ba = x=ba } , za09 ⟫ where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
524 za09 : ¬ odef (ZPmirror A B D dab) x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
525 za09 zd = ⊥-elim ( proj2 c∋ab (subst (λ k → odef D k) (sym zs02) (ZPC.c∋ab zd) ) ) where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
526 x=ba' = ZPC.x=ba zd |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
527 zs02 : & < * a , * b > ≡ & < * (ZPC.a zd) , * (ZPC.b zd) > |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
528 zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba' ) x=ba)))))) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
529 (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba' ) x=ba)))))) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
530 za10 : {x : Ordinal} → odef (ZPmirror A B C cab ＼ ZPmirror A B D dab) x → ZPC A B (C ＼ D) cdab x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
531 za10 {x} ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } , neg ⟫ = |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
532 record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ⟪ c∋ab , za11 ⟫ ; x=ba = x=ba } where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
533 za11 : ¬ odef D (& < * a , * b >) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
534 za11 zd = ⊥-elim (neg record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = zd ; x=ba = x=ba }) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
535 |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
536 |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
537 ZPmirror-whole : {A B : HOD} → ZPmirror A B (ZFP A B) (λ x → x) ≡ ZFP B A |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
538 ZPmirror-whole {A} {B} = ==→o≡ record { eq→ = za12 ; eq← = za13 } where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
539 za12 : {x : Ordinal} → ZPC A B (ZFP A B) (λ x₁ → x₁) x → ZFProduct B A x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
540 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) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
541 za13 : {x : Ordinal} → ZFProduct B A x → ZPC A B (ZFP A B) (λ x₁ → x₁) x |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
542 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 } |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
543 |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
544 ZPmirror-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZPmirror A B (* z) zab ≡ od∅ → z ≡ & od∅ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
545 ZPmirror-0 {A} {B} {z} {zab} eq = uf10 where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
546 uf10 : z ≡ & od∅ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
547 uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
548 uf11 : {y : Ordinal } → odef (* z) y → ⊥ |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
549 uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (& < * (zπ2 pqy) , * (zπ1 pqy) >) ) eq uf12 ) ) where |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
550 pqy : odef (ZFP A B) y |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
551 pqy = zab zy |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
552 uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
553 uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
554 uf12 : odef (ZPmirror A B (* z) zab) (& < * (zπ2 pqy) , * (zπ1 pqy) > ) |
|
2c34f2b554cf
Replace and filter projection fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1297
diff
changeset
|
555 uf12 = record { a = _ ; b = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 ; x=ba = refl } |
| 1297 | 556 |
| 1219 | 557 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 ) |
| 558 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where | |
| 559 zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x | |
| 560 zfp00 (ab-pair ⟪ pa , pb ⟫ qx) = ⟪ ab-pair pa qx , ab-pair pb qx ⟫ | |
| 561 zfp01 : {x : Ordinal} → odef (ZFP A C ∩ ZFP B C) x → ZFProduct (A ∩ B) C x | |
| 1220 | 562 zfp01 {x} ⟪ p , q ⟫ = subst (λ k → ZFProduct (A ∩ B) C k) zfp07 ( ab-pair (zfp02 ⟪ p , q ⟫ ) (zfp04 q) ) where |
| 563 zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x | |
| 564 zfp05 = zp-iso p | |
| 565 zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x | |
| 566 zfp06 = zp-iso q | |
| 567 zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x | |
| 1279 | 568 zfp07 = trans (cong (λ k → & < k , * (zπ2 q) > ) |
| 1220 | 569 (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06)))))))) zfp06 |
| 1219 | 570 zfp02 : {x : Ordinal } → (acx : odef (ZFP A C ∩ ZFP B C) x) → odef (A ∩ B) (zπ1 (proj1 acx)) |
| 1220 | 571 zfp02 {.(& < * _ , * _ >)} ⟪ ab-pair {a} {b} ax bx , bcx ⟫ = ⟪ ax , zfp03 bcx refl ⟫ where |
| 1219 | 572 zfp03 : {x : Ordinal } → (bc : odef (ZFP B C) x) → x ≡ (& < * a , * b >) → odef B (zπ1 (ab-pair {A} {C} ax bx)) |
| 1220 | 573 zfp03 (ab-pair {a1} {b1} x x₁) eq = subst (λ k → odef B k ) zfp08 x where |
| 574 zfp08 : a1 ≡ a | |
| 575 zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq))))) | |
| 1219 | 576 zfp04 : {x : Ordinal } (acx : odef (ZFP B C) x )→ odef C (zπ2 acx) |
| 1279 | 577 zfp04 (ab-pair x x₁) = x₁ |
| 1220 | 578 proj2 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where |
| 579 zfp00 : {x : Ordinal} → ZFProduct C (A ∩ B) x → odef (ZFP C A ∩ ZFP C B) x | |
| 580 zfp00 (ab-pair qx ⟪ pa , pb ⟫ ) = ⟪ ab-pair qx pa , ab-pair qx pb ⟫ | |
| 581 zfp01 : {x : Ordinal} → odef (ZFP C A ∩ ZFP C B ) x → ZFProduct C (A ∩ B) x | |
| 582 zfp01 {x} ⟪ p , q ⟫ = subst (λ k → ZFProduct C (A ∩ B) k) zfp07 ( ab-pair (zfp04 p) (zfp02 ⟪ p , q ⟫ ) ) where | |
| 583 zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x | |
| 584 zfp05 = zp-iso p | |
| 585 zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x | |
| 586 zfp06 = zp-iso q | |
| 587 zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x | |
| 1279 | 588 zfp07 = trans (cong (λ k → & < * (zπ1 p) , k > ) |
| 1220 | 589 (sym (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06))))))))) zfp05 |
| 590 zfp02 : {x : Ordinal } → (acx : odef (ZFP C A ∩ ZFP C B ) x) → odef (A ∩ B) (zπ2 (proj2 acx)) | |
| 591 zfp02 {.(& < * _ , * _ >)} ⟪ bcx , ab-pair {b} {a} ax bx ⟫ = ⟪ zfp03 bcx refl , bx ⟫ where | |
| 592 zfp03 : {x : Ordinal } → (bc : odef (ZFP C A ) x) → x ≡ (& < * b , * a >) → odef A (zπ2 (ab-pair {C} {B} ax bx )) | |
| 593 zfp03 (ab-pair {b1} {a1} x x₁) eq = subst (λ k → odef A k ) zfp08 x₁ where | |
| 594 zfp08 : a1 ≡ a | |
| 595 zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq))))) | |
| 596 zfp04 : {x : Ordinal } (acx : odef (ZFP C A ) x )→ odef C (zπ1 acx) | |
| 1279 | 597 zfp04 (ab-pair x x₁) = x |
| 1219 | 598 |
| 1224 | 599 open import BAlgebra O |
| 600 | |
| 601 ZFP\Q : {P Q p : HOD} → (( ZFP P Q ＼ ZFP p Q ) ≡ ZFP (P ＼ p) Q ) ∧ (( ZFP P Q ＼ ZFP P p ) ≡ ZFP P (Q ＼ p) ) | |
| 602 ZFP\Q {P} {Q} {p} = ⟪ ==→o≡ record { eq→ = ty70 ; eq← = ty71 } , ==→o≡ record { eq→ = ty73 ; eq← = ty75 } ⟫ where | |
| 603 ty70 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP p Q ) x → odef (ZFP (P ＼ p) Q) x | |
| 604 ty70 ⟪ ab-pair {a} {b} Pa pb , npq ⟫ = ab-pair ty72 pb where | |
| 605 ty72 : odef (P ＼ p ) a | |
| 606 ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫ | |
| 1279 | 607 ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x |
| 608 ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb | |
| 609 , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ | |
| 1224 | 610 ty73 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP P p ) x → odef (ZFP P (Q ＼ p) ) x |
| 611 ty73 ⟪ ab-pair {a} {b} pa Qb , npq ⟫ = ab-pair pa ty72 where | |
| 612 ty72 : odef (Q ＼ p ) b | |
| 613 ty72 = ⟪ Qb , (λ qb → npq (ab-pair pa qb ) ) ⟫ | |
| 1279 | 614 ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x |
| 615 ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb | |
| 616 , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫ | |
| 1219 | 617 |
| 618 | |
| 619 | |
| 620 | |
| 621 |