|
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
|
|
|
27 open Ordinals.IsNext isNext
|
|
|
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
|
|
1286
|
38 < x , y > = (x , x) , (x , y)
|
|
431
|
39
|
|
|
40 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
|
|
|
41 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
|
|
1279
|
42 left : {z : Ordinal} → odef (x , y) z → odef (y , x) z
|
|
431
|
43 left (case1 t) = case2 t
|
|
|
44 left (case2 t) = case1 t
|
|
1279
|
45 right : {z : Ordinal} → odef (y , x) z → odef (x , y) z
|
|
431
|
46 right (case1 t) = case2 t
|
|
|
47 right (case2 t) = case1 t
|
|
|
48
|
|
|
49 ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
|
|
|
50 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )
|
|
|
51
|
|
|
52 od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
|
|
|
53 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )
|
|
|
54
|
|
|
55 eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
|
|
|
56 eq-prod refl refl = refl
|
|
|
57
|
|
|
58 xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
|
|
1279
|
59 xx=zy→x=y {x} {y} eq with trio< (& x) (& y)
|
|
|
60 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl)
|
|
431
|
61 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
|
|
|
62 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
|
|
|
63 xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
|
|
1279
|
64 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl)
|
|
431
|
65 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
|
|
|
66 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
|
|
|
67
|
|
|
68 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
|
|
|
69 prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
|
|
|
70 lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
|
|
|
71 lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq ) where
|
|
|
72 lemma3 : ( x , x ) =h= ( y , z )
|
|
|
73 lemma3 = ==-trans eq exg-pair
|
|
|
74 lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
|
|
|
75 lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
|
|
|
76 lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
|
|
|
77 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
|
|
|
78 lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
|
|
|
79 lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
|
|
|
80 lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
|
|
|
81 ... | refl with lemma2 (==-sym eq )
|
|
|
82 ... | refl = refl
|
|
|
83 lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
|
|
|
84 lemmax : x ≡ x'
|
|
1279
|
85 lemmax with eq→ eq {& (x , x)} (case1 refl)
|
|
431
|
86 lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x')
|
|
|
87 lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
|
|
|
88 ... | refl = lemma1 (ord→== s )
|
|
|
89 lemmay : y ≡ y'
|
|
|
90 lemmay with lemmax
|
|
|
91 ... | refl with lemma4 eq -- with (x,y)≡(x,y')
|
|
|
92 ... | eq1 = lemma4 (ord→== (cong (λ k → & k ) eq1 ))
|
|
|
93
|
|
1098
|
94 prod-≡ : { x x' y y' : HOD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
|
|
|
95 prod-≡ eq = prod-eq (ord→== (cong (&) eq ))
|
|
|
96
|
|
431
|
97 --
|
|
1098
|
98 -- unlike ordered pair, ZFPair is not a HOD
|
|
431
|
99
|
|
|
100 data ord-pair : (p : Ordinal) → Set n where
|
|
|
101 pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
|
|
|
102
|
|
1098
|
103 ZFPair : OD
|
|
|
104 ZFPair = record { def = λ x → ord-pair x }
|
|
431
|
105
|
|
1285
|
106 -- _⊗_ : (A B : HOD) → HOD
|
|
|
107 -- A ⊗ B = Union ( Replace' B (λ b lb → Replace' A (λ a la → < a , b > ) record { ≤COD = ? } ) ? )
|
|
431
|
108
|
|
1285
|
109 -- product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b >
|
|
|
110 -- product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2 } where
|
|
|
111 -- lemma1 : odef (Replace' B (λ b₁ lb → Replace' A (λ a₁ la → < a₁ , b₁ >) ? ) ? ) (& (Replace' A (λ a₁ la → < a₁ , b >) ? ))
|
|
|
112 -- lemma1 = ? -- replacement← B b B∋b ?
|
|
|
113 -- lemma2 : odef (Replace' A (λ a₁ la → < a₁ , b >) ? ) (& < a , b >)
|
|
|
114 -- lemma2 = ? -- replacement← A a A∋a ?
|
|
431
|
115
|
|
1286
|
116 -- & (x , x) o< next (osuc (& x))
|
|
|
117 -- & (x , y) o< next (omax (& x) (& y))
|
|
|
118 -- & ((x , x) , (x , y)) o< next (omax (next (osuc (& x))) (next (omax (& x) (& y))))
|
|
|
119 -- o≤ next (next (omax (& A) (& B)))
|
|
|
120
|
|
1098
|
121 data ZFProduct (A B : HOD) : (p : Ordinal) → Set n where
|
|
|
122 ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )
|
|
|
123
|
|
431
|
124 ZFP : (A B : HOD) → HOD
|
|
1279
|
125 ZFP A B = record { od = record { def = λ x → ZFProduct A B x }
|
|
1285
|
126 ; odmax = omax (& A) (& B) ; <odmax = λ {y} px → lemma0 px }
|
|
431
|
127 where
|
|
1285
|
128 lemma0 : {A B : HOD} {x : Ordinal} → ZFProduct A B x → x o< omax (& A) (& B)
|
|
1286
|
129 lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b | inspect (omax a) b
|
|
|
130 ... | tri< a<b ¬b ¬c | record { eq = eq1 } = ?
|
|
|
131 ... | tri≈ ¬a a=b ¬c | record { eq = eq1 } = ?
|
|
|
132 ... | tri> ¬a ¬b b<a | record { eq = eq1 } = ?
|
|
1098
|
133
|
|
|
134 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b → ZFP A B ∋ < a , b >
|
|
1279
|
135 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
|
136
|
|
1104
|
137 zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
|
|
|
138 zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a
|
|
|
139
|
|
|
140 zp1 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef A (zπ1 zx)
|
|
|
141 zp1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = aa
|
|
|
142
|
|
|
143 zπ2 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
|
|
|
144 zπ2 (ab-pair {a} {b} aa bb) = b
|
|
|
145
|
|
|
146 zp2 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef B (zπ2 zx)
|
|
|
147 zp2 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = bb
|
|
|
148
|
|
|
149 zp-iso : { A B : HOD } → {x : Ordinal } → (p : odef (ZFP A B) x ) → & < * (zπ1 p) , * (zπ2 p) > ≡ x
|
|
|
150 zp-iso {A} {B} {_} (ab-pair {a} {b} aa bb) = refl
|
|
|
151
|
|
1216
|
152 zp-iso1 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (* (zπ1 p) ≡ (* a)) ∧ (* (zπ2 p) ≡ (* b))
|
|
|
153 zp-iso1 {A} {B} {a} {b} pab = prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) zz11) ) where
|
|
|
154 zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b >
|
|
|
155 zz11 = zp-iso pab
|
|
|
156
|
|
1223
|
157 zp-iso0 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (zπ1 p ≡ a) ∧ (zπ2 p ≡ b)
|
|
1279
|
158 zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) ))
|
|
1223
|
159 , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) ) ⟫
|
|
|
160
|
|
1285
|
161 -- ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
|
|
|
162 -- ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
|
|
1098
|
163
|
|
1285
|
164 -- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x)
|
|
|
165 -- ⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
|
|
|
166 -- zfp02 : Replace' A (λ z lz → < z , * a >) record { ≤COD = ? } ≡ * owner
|
|
|
167 -- zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
|
|
|
168 -- zfp01 : odef (ZFP A B) (& x)
|
|
|
169 -- zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
|
|
|
170 -- ... | t = ?
|
|
|
171 -- -- ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba)
|
|
431
|
172
|
|
1276
|
173 ZPI1 : (A B : HOD) → HOD
|
|
1285
|
174 ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) ?
|
|
1105
|
175
|
|
1276
|
176 ZPI2 : (A B : HOD) → HOD
|
|
1285
|
177 ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) ?
|
|
1098
|
178
|
|
1218
|
179 ZFProj1-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
|
|
|
180 ZFProj1-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
|
|
|
181 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
|
|
1105
|
182
|
|
1218
|
183 ZFProj2-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b
|
|
|
184 ZFProj2-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
|
|
|
185 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d)
|
|
1105
|
186
|
|
1278
|
187 ZPI1-iso : (A B : HOD) → {b : Ordinal } → odef B b → ZPI1 A B ≡ A
|
|
|
188 ZPI1-iso P Q {q} qq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
|
|
|
189 ty21 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >)))
|
|
|
190 ty21 pz qz = subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz )
|
|
|
191 ty32 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → zπ1 (ty21 pz qz) ≡ a
|
|
|
192 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where
|
|
|
193 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
|
|
|
194 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
|
|
|
195 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
|
|
|
196 ty20 : {x : Ordinal} → odef (ZPI1 P Q) x → odef P x
|
|
|
197 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef P k) a=x pz where
|
|
|
198 ty24 : * x ≡ * a
|
|
|
199 ty24 = begin
|
|
|
200 * x ≡⟨ cong (*) x=ψz ⟩
|
|
|
201 _ ≡⟨ *iso ⟩
|
|
|
202 * (zπ1 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz))) ≡⟨ cong (*) (ty32 pz qz) ⟩
|
|
|
203 * a ∎ where open ≡-Reasoning
|
|
|
204 a=x : a ≡ x
|
|
|
205 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24))
|
|
|
206 ty22 : {x : Ordinal} → odef P x → odef (ZPI1 P Q) x
|
|
|
207 ty22 {x} px = record { z = _ ; az = ab-pair px qq ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where
|
|
|
208 ty12 : * x ≡ * (zπ1 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair px qq )))
|
|
|
209 ty12 = begin
|
|
|
210 * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩
|
|
|
211 * (zπ1 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair px qq ))) ∎ where open ≡-Reasoning
|
|
|
212
|
|
|
213 ZPI2-iso : (A B : HOD) → {b : Ordinal } → odef A b → ZPI2 A B ≡ B
|
|
|
214 ZPI2-iso P Q {p} pp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
|
|
|
215 ty21 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >)))
|
|
|
216 ty21 pz qz = subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz )
|
|
|
217 ty32 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → zπ2 (ty21 pz qz) ≡ b
|
|
|
218 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where
|
|
|
219 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b
|
|
|
220 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
|
|
|
221 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d)
|
|
|
222 ty20 : {x : Ordinal} → odef (ZPI2 P Q) x → odef Q x
|
|
|
223 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef Q k) a=x qz where
|
|
|
224 ty24 : * x ≡ * b
|
|
|
225 ty24 = begin
|
|
|
226 * x ≡⟨ cong (*) x=ψz ⟩
|
|
|
227 _ ≡⟨ *iso ⟩
|
|
|
228 * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz))) ≡⟨ cong (*) (ty32 pz qz) ⟩
|
|
|
229 * b ∎ where open ≡-Reasoning
|
|
|
230 a=x : b ≡ x
|
|
|
231 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24))
|
|
|
232 ty22 : {x : Ordinal} → odef Q x → odef (ZPI2 P Q) x
|
|
|
233 ty22 {x} qx = record { z = _ ; az = ab-pair pp qx ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where
|
|
|
234 ty12 : * x ≡ * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx)))
|
|
|
235 ty12 = begin
|
|
|
236 * x ≡⟨ sym (cong (*) (ty32 pp qx )) ⟩
|
|
|
237 * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx ))) ∎ where open ≡-Reasoning
|
|
|
238
|
|
1279
|
239 record Func (A B : HOD) : Set n where
|
|
|
240 field
|
|
|
241 func : {x : Ordinal } → odef A x → Ordinal
|
|
|
242 is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax )
|
|
|
243
|
|
|
244 data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where
|
|
1285
|
245 felm : (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > ) ? ))
|
|
1279
|
246
|
|
|
247 FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
|
|
|
248 FuncHOD→F {A} {B} (felm F) = F
|
|
|
249
|
|
1285
|
250 FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡ Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > ) ?
|
|
1279
|
251 FuncHOD=R {A} {B} (felm F) = *iso
|
|
|
252
|
|
|
253 --
|
|
|
254 -- Set of All function from A to B
|
|
|
255 --
|
|
|
256
|
|
|
257 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
|
258
|
|
|
259 Funcs : (A B : HOD) → HOD
|
|
|
260 Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B))
|
|
|
261 ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where
|
|
|
262 lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x
|
|
|
263 lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
|
|
|
264 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k)
|
|
|
265 (sym x=ψz) lemma4 where
|
|
|
266 lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > )
|
|
|
267 lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az))
|
|
|
268
|
|
|
269 record Injection (A B : Ordinal ) : Set n where
|
|
|
270 field
|
|
|
271 i→ : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
272 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt )
|
|
|
273 iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y
|
|
|
274
|
|
|
275 record HODBijection (A B : HOD ) : Set n where
|
|
|
276 field
|
|
|
277 fun← : (x : Ordinal ) → odef A x → Ordinal
|
|
|
278 fun→ : (x : Ordinal ) → odef B x → Ordinal
|
|
|
279 funB : (x : Ordinal ) → ( lt : odef A x ) → odef B ( fun← x lt )
|
|
|
280 funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun→ x lt )
|
|
|
281 fiso← : (x : Ordinal ) → ( lt : odef B x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
|
|
|
282 fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
|
|
|
283
|
|
|
284 hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b
|
|
|
285 hodbij-refl {a} refl = record {
|
|
|
286 fun← = λ x _ → x
|
|
|
287 ; fun→ = λ x _ → x
|
|
|
288 ; funB = λ x lt → lt
|
|
|
289 ; funA = λ x lt → lt
|
|
|
290 ; fiso← = λ x lt → refl
|
|
|
291 ; fiso→ = λ x lt → refl
|
|
|
292 }
|
|
|
293
|
|
|
294 pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) →
|
|
|
295 (zπ1 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ1 ab ))) ∧
|
|
|
296 (zπ2 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ2 ab )))
|
|
|
297 pj12 A B (ab-pair {x} {y} ax by) = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (prod-≡ pj24 )))
|
|
|
298 , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (prod-≡ pj24))) ⟫ where
|
|
|
299 pj22 : odef (ZFP A B) (& (* (& < * x , * y >)))
|
|
|
300 pj22 = subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by)
|
|
|
301 pj23 : & < * (zπ1 pj22 ) , * (zπ2 pj22) > ≡ & (* (& < * x , * y >) )
|
|
|
302 pj23 = zp-iso pj22
|
|
|
303 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))) >
|
|
|
304 ≡ < * (& (* x)) , * (& (* y)) >
|
|
|
305 pj24 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( trans pj23 (trans &iso
|
|
|
306 (sym (cong (&) (cong₂ (λ j k → < j , k >) *iso *iso)) ))))
|
|
|
307 pj02 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab)
|
|
|
308 pj02 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj2 (pj12 A B ab))) (sym &iso)) }
|
|
|
309 pj01 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI1 A B) (zπ1 ab)
|
|
|
310 pj01 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj1 (pj12 A B ab))) (sym &iso)) }
|
|
|
311
|
|
|
312 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) >)
|
|
|
313 pj2 A B x ab = ab-pair (pj02 A B x ab) (pj01 A B x ab)
|
|
|
314
|
|
|
315 aZPI1 : (A B : HOD) {y : Ordinal} → odef (ZPI1 A B) y → odef A y
|
|
|
316 aZPI1 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef A k) (trans (
|
|
|
317 trans (sym &iso) (trans (sym (proj1 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp1 az )
|
|
|
318 aZPI2 : (A B : HOD) {y : Ordinal} → odef (ZPI2 A B) y → odef B y
|
|
|
319 aZPI2 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef B k) (trans (
|
|
|
320 trans (sym &iso) (trans (sym (proj2 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp2 az )
|
|
|
321
|
|
|
322 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) >)
|
|
|
323 pj1 A B _ (ab-pair ax by) = ab-pair (aZPI1 A B by) (aZPI2 A B ax)
|
|
1278
|
324
|
|
|
325 ZFPsym1 : (A B : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B))
|
|
|
326 ZFPsym1 A B = record {
|
|
1276
|
327 fun← = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
|
|
|
328 ; fun→ = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
|
|
1277
|
329 ; funB = pj2 A B
|
|
|
330 ; funA = pj1 A B
|
|
1278
|
331 ; fiso← = λ xy ab → pj00 A B ab
|
|
1277
|
332 ; fiso→ = λ xy ab → zp-iso ab
|
|
1278
|
333 } where
|
|
1279
|
334 pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy )
|
|
1278
|
335 → & < * (zπ1 ab) , * (zπ2 ab) > ≡ & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) >
|
|
|
336 pj10 A B {.(& < * _ , * _ >)} (ab-pair ax by ) = refl
|
|
1279
|
337 pj00 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy )
|
|
|
338 → & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > ≡ xy
|
|
1278
|
339 pj00 A B {xy} ab = trans (sym (pj10 A B ab)) (zp-iso {ZPI2 A B} {ZPI1 A B} {xy} ab)
|
|
1274
|
340
|
|
1279
|
341 --
|
|
|
342 -- Bijection of (A x B) and (B x A) requires one element or axiom of choice
|
|
|
343 --
|
|
1278
|
344 ZFPsym : (A B : HOD) → {a b : Ordinal } → odef A a → odef B b → HODBijection (ZFP A B) (ZFP B A)
|
|
|
345 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
|
346
|
|
1219
|
347 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 )
|
|
|
348 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where
|
|
|
349 zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x
|
|
|
350 zfp00 (ab-pair ⟪ pa , pb ⟫ qx) = ⟪ ab-pair pa qx , ab-pair pb qx ⟫
|
|
|
351 zfp01 : {x : Ordinal} → odef (ZFP A C ∩ ZFP B C) x → ZFProduct (A ∩ B) C x
|
|
1220
|
352 zfp01 {x} ⟪ p , q ⟫ = subst (λ k → ZFProduct (A ∩ B) C k) zfp07 ( ab-pair (zfp02 ⟪ p , q ⟫ ) (zfp04 q) ) where
|
|
|
353 zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x
|
|
|
354 zfp05 = zp-iso p
|
|
|
355 zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x
|
|
|
356 zfp06 = zp-iso q
|
|
|
357 zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x
|
|
1279
|
358 zfp07 = trans (cong (λ k → & < k , * (zπ2 q) > )
|
|
1220
|
359 (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06)))))))) zfp06
|
|
1219
|
360 zfp02 : {x : Ordinal } → (acx : odef (ZFP A C ∩ ZFP B C) x) → odef (A ∩ B) (zπ1 (proj1 acx))
|
|
1220
|
361 zfp02 {.(& < * _ , * _ >)} ⟪ ab-pair {a} {b} ax bx , bcx ⟫ = ⟪ ax , zfp03 bcx refl ⟫ where
|
|
1219
|
362 zfp03 : {x : Ordinal } → (bc : odef (ZFP B C) x) → x ≡ (& < * a , * b >) → odef B (zπ1 (ab-pair {A} {C} ax bx))
|
|
1220
|
363 zfp03 (ab-pair {a1} {b1} x x₁) eq = subst (λ k → odef B k ) zfp08 x where
|
|
|
364 zfp08 : a1 ≡ a
|
|
|
365 zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq)))))
|
|
1219
|
366 zfp04 : {x : Ordinal } (acx : odef (ZFP B C) x )→ odef C (zπ2 acx)
|
|
1279
|
367 zfp04 (ab-pair x x₁) = x₁
|
|
1220
|
368 proj2 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where
|
|
|
369 zfp00 : {x : Ordinal} → ZFProduct C (A ∩ B) x → odef (ZFP C A ∩ ZFP C B) x
|
|
|
370 zfp00 (ab-pair qx ⟪ pa , pb ⟫ ) = ⟪ ab-pair qx pa , ab-pair qx pb ⟫
|
|
|
371 zfp01 : {x : Ordinal} → odef (ZFP C A ∩ ZFP C B ) x → ZFProduct C (A ∩ B) x
|
|
|
372 zfp01 {x} ⟪ p , q ⟫ = subst (λ k → ZFProduct C (A ∩ B) k) zfp07 ( ab-pair (zfp04 p) (zfp02 ⟪ p , q ⟫ ) ) where
|
|
|
373 zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x
|
|
|
374 zfp05 = zp-iso p
|
|
|
375 zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x
|
|
|
376 zfp06 = zp-iso q
|
|
|
377 zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x
|
|
1279
|
378 zfp07 = trans (cong (λ k → & < * (zπ1 p) , k > )
|
|
1220
|
379 (sym (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06))))))))) zfp05
|
|
|
380 zfp02 : {x : Ordinal } → (acx : odef (ZFP C A ∩ ZFP C B ) x) → odef (A ∩ B) (zπ2 (proj2 acx))
|
|
|
381 zfp02 {.(& < * _ , * _ >)} ⟪ bcx , ab-pair {b} {a} ax bx ⟫ = ⟪ zfp03 bcx refl , bx ⟫ where
|
|
|
382 zfp03 : {x : Ordinal } → (bc : odef (ZFP C A ) x) → x ≡ (& < * b , * a >) → odef A (zπ2 (ab-pair {C} {B} ax bx ))
|
|
|
383 zfp03 (ab-pair {b1} {a1} x x₁) eq = subst (λ k → odef A k ) zfp08 x₁ where
|
|
|
384 zfp08 : a1 ≡ a
|
|
|
385 zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq)))))
|
|
|
386 zfp04 : {x : Ordinal } (acx : odef (ZFP C A ) x )→ odef C (zπ1 acx)
|
|
1279
|
387 zfp04 (ab-pair x x₁) = x
|
|
1219
|
388
|
|
1224
|
389 open import BAlgebra O
|
|
|
390
|
|
|
391 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) )
|
|
|
392 ZFP\Q {P} {Q} {p} = ⟪ ==→o≡ record { eq→ = ty70 ; eq← = ty71 } , ==→o≡ record { eq→ = ty73 ; eq← = ty75 } ⟫ where
|
|
|
393 ty70 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP p Q ) x → odef (ZFP (P ＼ p) Q) x
|
|
|
394 ty70 ⟪ ab-pair {a} {b} Pa pb , npq ⟫ = ab-pair ty72 pb where
|
|
|
395 ty72 : odef (P ＼ p ) a
|
|
|
396 ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫
|
|
1279
|
397 ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x
|
|
|
398 ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb
|
|
|
399 , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫
|
|
1224
|
400 ty73 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP P p ) x → odef (ZFP P (Q ＼ p) ) x
|
|
|
401 ty73 ⟪ ab-pair {a} {b} pa Qb , npq ⟫ = ab-pair pa ty72 where
|
|
|
402 ty72 : odef (Q ＼ p ) b
|
|
|
403 ty72 = ⟪ Qb , (λ qb → npq (ab-pair pa qb ) ) ⟫
|
|
1279
|
404 ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x
|
|
|
405 ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb
|
|
|
406 , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫
|
|
1219
|
407
|
|
|
408
|
|
|
409
|
|
|
410
|
|
|
411
|
