Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate 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 |
| 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 zf | |
| 8 open import logic | |
| 9 import OD | |
| 10 import ODUtil | |
| 11 import OrdUtil | |
| 12 | |
| 13 open import Relation.Nullary | |
| 14 open import Relation.Binary | |
| 15 open import Data.Empty | |
| 16 open import Relation.Binary | |
| 17 open import Relation.Binary.Core | |
| 18 open import Relation.Binary.PropositionalEquality | |
| 19 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) | |
| 20 | |
| 21 open OD O | |
| 22 open OD.OD | |
| 23 open OD.HOD | |
| 24 open ODAxiom odAxiom | |
| 25 | |
| 26 open Ordinals.Ordinals O | |
| 27 open Ordinals.IsOrdinals isOrdinal | |
| 28 open Ordinals.IsNext isNext | |
| 29 open OrdUtil O | |
| 30 open ODUtil O | |
| 31 | |
| 32 open _∧_ | |
| 33 open _∨_ | |
| 34 open Bool | |
| 35 | |
| 36 open _==_ | |
| 37 | |
| 38 <_,_> : (x y : HOD) → HOD | |
| 39 < x , y > = (x , x ) , (x , y ) | |
| 40 | |
| 41 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x ) | |
| 42 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where | |
| 43 left : {z : Ordinal} → odef (x , y) z → odef (y , x) z | |
| 44 left (case1 t) = case2 t | |
| 45 left (case2 t) = case1 t | |
| 46 right : {z : Ordinal} → odef (y , x) z → odef (x , y) z | |
| 47 right (case1 t) = case2 t | |
| 48 right (case2 t) = case1 t | |
| 49 | |
| 50 ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y | |
| 51 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq ) | |
| 52 | |
| 53 od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y | |
| 54 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq ) | |
| 55 | |
| 56 eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > | |
| 57 eq-prod refl refl = refl | |
| 58 | |
| 59 xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y | |
| 60 xx=zy→x=y {x} {y} eq with trio< (& x) (& y) | |
| 61 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) | |
| 62 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) | |
| 63 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) | |
| 64 xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b | |
| 65 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl) | |
| 66 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) | |
| 67 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) | |
| 68 | |
| 69 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) | |
| 70 prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where | |
| 71 lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y | |
| 72 lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq ) where | |
| 73 lemma3 : ( x , x ) =h= ( y , z ) | |
| 74 lemma3 = ==-trans eq exg-pair | |
| 75 lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y | |
| 76 lemma1 {x} {y} eq with eq← eq {& y} (case2 refl) | |
| 77 lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) | |
| 78 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) | |
| 79 lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z | |
| 80 lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl) | |
| 81 lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z | |
| 82 ... | refl with lemma2 (==-sym eq ) | |
| 83 ... | refl = refl | |
| 84 lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z | |
| 85 lemmax : x ≡ x' | |
| 86 lemmax with eq→ eq {& (x , x)} (case1 refl) | |
| 87 lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') | |
| 88 lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' | |
| 89 ... | refl = lemma1 (ord→== s ) | |
| 90 lemmay : y ≡ y' | |
| 91 lemmay with lemmax | |
| 92 ... | refl with lemma4 eq -- with (x,y)≡(x,y') | |
| 93 ... | eq1 = lemma4 (ord→== (cong (λ k → & k ) eq1 )) | |
| 94 | |
| 1098 | 95 prod-≡ : { x x' y y' : HOD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) |
| 96 prod-≡ eq = prod-eq (ord→== (cong (&) eq )) | |
| 97 | |
| 431 | 98 -- |
| 1098 | 99 -- unlike ordered pair, ZFPair is not a HOD |
| 431 | 100 |
| 101 data ord-pair : (p : Ordinal) → Set n where | |
| 102 pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) ) | |
| 103 | |
| 1098 | 104 ZFPair : OD |
| 105 ZFPair = record { def = λ x → ord-pair x } | |
| 431 | 106 |
| 107 _⊗_ : (A B : HOD) → HOD | |
| 108 A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) | |
| 109 | |
| 110 product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b > | |
| 1096 | 111 product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2 } where |
| 431 | 112 lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >))) |
| 113 lemma1 = replacement← B b B∋b | |
| 114 lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >) | |
| 115 lemma2 = replacement← A a A∋a | |
| 116 | |
| 1098 | 117 data ZFProduct (A B : HOD) : (p : Ordinal) → Set n where |
| 118 ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) ) | |
| 119 | |
| 431 | 120 ZFP : (A B : HOD) → HOD |
| 1098 | 121 ZFP A B = record { od = record { def = λ x → ZFProduct A B x } |
| 1169 | 122 ; odmax = odmax ( A ⊗ B ) ; <odmax = λ {y} px → <odmax ( A ⊗ B ) (lemma0 px) } |
| 431 | 123 where |
| 1169 | 124 lemma0 : {A B : HOD} {x : Ordinal} → ZFProduct A B x → odef (A ⊗ B) x |
| 125 lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by) | |
| 1098 | 126 |
| 127 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b → ZFP A B ∋ < a , b > | |
| 128 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 | 129 |
| 1104 | 130 zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal |
| 131 zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a | |
| 132 | |
| 133 zp1 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef A (zπ1 zx) | |
| 134 zp1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = aa | |
| 135 | |
| 136 zπ2 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal | |
| 137 zπ2 (ab-pair {a} {b} aa bb) = b | |
| 138 | |
| 139 zp2 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef B (zπ2 zx) | |
| 140 zp2 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = bb | |
| 141 | |
| 142 zp-iso : { A B : HOD } → {x : Ordinal } → (p : odef (ZFP A B) x ) → & < * (zπ1 p) , * (zπ2 p) > ≡ x | |
| 143 zp-iso {A} {B} {_} (ab-pair {a} {b} aa bb) = refl | |
| 144 | |
| 1216 | 145 zp-iso1 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (* (zπ1 p) ≡ (* a)) ∧ (* (zπ2 p) ≡ (* b)) |
| 146 zp-iso1 {A} {B} {a} {b} pab = prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) zz11) ) where | |
| 147 zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b > | |
| 148 zz11 = zp-iso pab | |
| 149 | |
| 1223 | 150 zp-iso0 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (zπ1 p ≡ a) ∧ (zπ2 p ≡ b) |
| 151 zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) )) | |
| 152 , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) ) ⟫ | |
| 153 | |
| 431 | 154 ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x |
| 1098 | 155 ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by) |
| 156 | |
| 157 ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x) | |
| 158 ⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where | |
| 159 zfp02 : Replace A (λ z → < z , * a >) ≡ * owner | |
| 160 zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa )) | |
| 161 zfp01 : odef (ZFP A B) (& x) | |
| 162 zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox | |
| 163 ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) | |
| 431 | 164 |
| 1105 | 165 ZFPproj1 : {A B X : HOD} → X ⊆ ZFP A B → HOD |
| 166 ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) )) | |
| 167 | |
| 168 ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B → HOD | |
| 169 ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) )) | |
| 1098 | 170 |
| 1218 | 171 ZFProj1-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a |
| 172 ZFProj1-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 173 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) | |
| 1105 | 174 |
| 1218 | 175 ZFProj2-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b |
| 176 ZFProj2-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 177 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) | |
| 1105 | 178 |
| 1274 | 179 record Func (A B : HOD) : Set n where |
| 180 field | |
| 181 func : {x : Ordinal } → odef A x → Ordinal | |
| 182 is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax ) | |
| 183 | |
| 184 data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where | |
| 185 felm : (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > ))) | |
| 186 | |
| 187 FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B | |
| 188 FuncHOD→F {A} {B} (felm F) = F | |
| 189 | |
| 190 FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡ Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > ) | |
| 191 FuncHOD=R {A} {B} (felm F) = *iso | |
| 192 | |
| 193 -- | |
| 194 -- Set of All function from A to B | |
| 195 -- | |
| 196 | |
| 197 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | |
| 198 | |
| 199 Funcs : (A B : HOD) → HOD | |
| 200 Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B)) | |
| 201 ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where | |
| 202 lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x | |
| 203 lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx | |
| 204 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k) | |
| 205 (sym x=ψz) lemma4 where | |
| 206 lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > ) | |
| 207 lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az)) | |
| 208 | |
| 209 record Injection (A B : Ordinal ) : Set n where | |
| 210 field | |
| 211 i→ : (x : Ordinal ) → odef (* A) x → Ordinal | |
| 212 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt ) | |
| 213 iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y | |
| 214 | |
| 215 record OrdBijection (A B : Ordinal ) : Set n where | |
| 216 field | |
| 217 fun← : (x : Ordinal ) → odef (* A) x → Ordinal | |
| 218 fun→ : (x : Ordinal ) → odef (* B) x → Ordinal | |
| 219 funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt ) | |
| 220 funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt ) | |
| 221 fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x | |
| 222 fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x | |
| 223 | |
| 224 ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b | |
| 225 ordbij-refl {a} refl = record { | |
| 226 fun← = λ x _ → x | |
| 227 ; fun→ = λ x _ → x | |
| 228 ; funB = λ x lt → lt | |
| 229 ; funA = λ x lt → lt | |
| 230 ; fiso← = λ x lt → refl | |
| 231 ; fiso→ = λ x lt → refl | |
| 232 } | |
| 233 | |
| 234 ZFPsym : (A B : HOD) → OrdBijection (& (ZFP A B)) (& (ZFP B A)) | |
| 235 ZFPsym A B = record { | |
|
1275
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
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 )) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
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 )) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
238 ; funB = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
239 (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab)) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
240 ; funA = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
241 (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab)) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
242 ; fiso← = λ xy ab → trans (cong getord ( HE.≅-to-≡ (exchg² refl (ab-pair ? ? ))) ) (trans ? (is-prod (subst (λ k → odef k xy) *iso ab)) ) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
243 ; fiso→ = λ xy ab → ? |
| 1274 | 244 } where |
|
1275
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
245 getord : {A B : HOD} {xy : Ordinal} → odef (ZFP A B) xy → Ordinal |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
246 getord {A} {B} {xy} ab = xy |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
247 is-prod : {A B : HOD} {xy : Ordinal} → (ab : odef (ZFP A B) xy) → getord ab ≡ xy |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
248 is-prod {A} {B} {xy} ab = refl |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
249 exchg : {A B : HOD} {x y xy : Ordinal} → xy ≡ & < * x , * y > → odef (ZFP A B) xy → odef (ZFP B A) (& < * y , * x >) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
250 exchg {A} {B} {x} {y} eq (ab-pair {a} {b} ax by ) = subst (λ k → odef (ZFP B A) k) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
251 (cong₂ (λ j k → & < j , k >) (proj2 (prod-≡ lemma2 )) (proj1 (prod-≡ lemma2 )) ) (ab-pair by ax) where |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
252 lemma2 : < * a , * b > ≡ < * x , * y > |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
253 lemma2 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq) |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
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 |
|
e7743ac5a070
OrdBijection (& (ZFP A B)) (& (ZFP B A))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1274
diff
changeset
|
255 exchg² {A} {B} eq (ab-pair ax by ) = ? |
| 1274 | 256 |
| 257 | |
| 1219 | 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 ) |
| 259 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where | |
| 260 zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x | |
| 261 zfp00 (ab-pair ⟪ pa , pb ⟫ qx) = ⟪ ab-pair pa qx , ab-pair pb qx ⟫ | |
| 262 zfp01 : {x : Ordinal} → odef (ZFP A C ∩ ZFP B C) x → ZFProduct (A ∩ B) C x | |
| 1220 | 263 zfp01 {x} ⟪ p , q ⟫ = subst (λ k → ZFProduct (A ∩ B) C k) zfp07 ( ab-pair (zfp02 ⟪ p , q ⟫ ) (zfp04 q) ) where |
| 264 zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x | |
| 265 zfp05 = zp-iso p | |
| 266 zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x | |
| 267 zfp06 = zp-iso q | |
| 268 zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x | |
| 269 zfp07 = trans (cong (λ k → & < k , * (zπ2 q) > ) | |
| 270 (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06)))))))) zfp06 | |
| 1219 | 271 zfp02 : {x : Ordinal } → (acx : odef (ZFP A C ∩ ZFP B C) x) → odef (A ∩ B) (zπ1 (proj1 acx)) |
| 1220 | 272 zfp02 {.(& < * _ , * _ >)} ⟪ ab-pair {a} {b} ax bx , bcx ⟫ = ⟪ ax , zfp03 bcx refl ⟫ where |
| 1219 | 273 zfp03 : {x : Ordinal } → (bc : odef (ZFP B C) x) → x ≡ (& < * a , * b >) → odef B (zπ1 (ab-pair {A} {C} ax bx)) |
| 1220 | 274 zfp03 (ab-pair {a1} {b1} x x₁) eq = subst (λ k → odef B k ) zfp08 x where |
| 275 zfp08 : a1 ≡ a | |
| 276 zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq))))) | |
| 1219 | 277 zfp04 : {x : Ordinal } (acx : odef (ZFP B C) x )→ odef C (zπ2 acx) |
| 1220 | 278 zfp04 (ab-pair x x₁) = x₁ |
| 279 proj2 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where | |
| 280 zfp00 : {x : Ordinal} → ZFProduct C (A ∩ B) x → odef (ZFP C A ∩ ZFP C B) x | |
| 281 zfp00 (ab-pair qx ⟪ pa , pb ⟫ ) = ⟪ ab-pair qx pa , ab-pair qx pb ⟫ | |
| 282 zfp01 : {x : Ordinal} → odef (ZFP C A ∩ ZFP C B ) x → ZFProduct C (A ∩ B) x | |
| 283 zfp01 {x} ⟪ p , q ⟫ = subst (λ k → ZFProduct C (A ∩ B) k) zfp07 ( ab-pair (zfp04 p) (zfp02 ⟪ p , q ⟫ ) ) where | |
| 284 zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x | |
| 285 zfp05 = zp-iso p | |
| 286 zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x | |
| 287 zfp06 = zp-iso q | |
| 288 zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x | |
| 289 zfp07 = trans (cong (λ k → & < * (zπ1 p) , k > ) | |
| 290 (sym (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06))))))))) zfp05 | |
| 291 zfp02 : {x : Ordinal } → (acx : odef (ZFP C A ∩ ZFP C B ) x) → odef (A ∩ B) (zπ2 (proj2 acx)) | |
| 292 zfp02 {.(& < * _ , * _ >)} ⟪ bcx , ab-pair {b} {a} ax bx ⟫ = ⟪ zfp03 bcx refl , bx ⟫ where | |
| 293 zfp03 : {x : Ordinal } → (bc : odef (ZFP C A ) x) → x ≡ (& < * b , * a >) → odef A (zπ2 (ab-pair {C} {B} ax bx )) | |
| 294 zfp03 (ab-pair {b1} {a1} x x₁) eq = subst (λ k → odef A k ) zfp08 x₁ where | |
| 295 zfp08 : a1 ≡ a | |
| 296 zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq))))) | |
| 297 zfp04 : {x : Ordinal } (acx : odef (ZFP C A ) x )→ odef C (zπ1 acx) | |
| 298 zfp04 (ab-pair x x₁) = x | |
| 1219 | 299 |
| 1224 | 300 open import BAlgebra O |
| 301 | |
| 302 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) ) | |
| 303 ZFP\Q {P} {Q} {p} = ⟪ ==→o≡ record { eq→ = ty70 ; eq← = ty71 } , ==→o≡ record { eq→ = ty73 ; eq← = ty75 } ⟫ where | |
| 304 ty70 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP p Q ) x → odef (ZFP (P ＼ p) Q) x | |
| 305 ty70 ⟪ ab-pair {a} {b} Pa pb , npq ⟫ = ab-pair ty72 pb where | |
| 306 ty72 : odef (P ＼ p ) a | |
| 307 ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫ | |
| 308 ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x | |
| 309 ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb | |
| 310 , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ | |
| 311 ty73 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP P p ) x → odef (ZFP P (Q ＼ p) ) x | |
| 312 ty73 ⟪ ab-pair {a} {b} pa Qb , npq ⟫ = ab-pair pa ty72 where | |
| 313 ty72 : odef (Q ＼ p ) b | |
| 314 ty72 = ⟪ Qb , (λ qb → npq (ab-pair pa qb ) ) ⟫ | |
| 315 ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x | |
| 316 ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb | |
| 317 , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫ | |
| 1219 | 318 |
| 319 | |
| 320 | |
| 321 | |
| 322 |