|
1175
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2
|
|
1387
|
3 open import Level hiding (suc ; zero )
|
|
431
|
4 open import Ordinals
|
|
|
5 module cardinal {n : Level } (O : Ordinals {n}) where
|
|
|
6
|
|
|
7 open import logic
|
|
1095
|
8 -- import OD
|
|
|
9 import OD hiding ( _⊆_ )
|
|
|
10
|
|
431
|
11 import ODC
|
|
1387
|
12 open import Data.Nat
|
|
431
|
13 open import Relation.Binary.PropositionalEquality
|
|
1095
|
14 open import Data.Nat.Properties
|
|
431
|
15 open import Data.Empty
|
|
|
16 open import Relation.Nullary
|
|
|
17 open import Relation.Binary
|
|
|
18 open import Relation.Binary.Core
|
|
|
19
|
|
|
20 open inOrdinal O
|
|
|
21 open OD O
|
|
|
22 open OD.OD
|
|
|
23 open ODAxiom odAxiom
|
|
1218
|
24 open import ZProduct O
|
|
431
|
25
|
|
|
26 import OrdUtil
|
|
|
27 import ODUtil
|
|
|
28 open Ordinals.Ordinals O
|
|
|
29 open Ordinals.IsOrdinals isOrdinal
|
|
1300
|
30 -- open Ordinals.IsNext isNext
|
|
431
|
31 open OrdUtil O
|
|
|
32 open ODUtil O
|
|
|
33
|
|
1095
|
34 _⊆_ : ( A B : HOD ) → Set n
|
|
|
35 _⊆_ A B = {x : Ordinal } → odef A x → odef B x
|
|
|
36
|
|
431
|
37
|
|
|
38 open _∧_
|
|
|
39 open _∨_
|
|
|
40 open Bool
|
|
|
41 open _==_
|
|
|
42
|
|
|
43 open HOD
|
|
|
44
|
|
1124
|
45 record OrdBijection (A B : Ordinal ) : Set n where
|
|
431
|
46 field
|
|
|
47 fun← : (x : Ordinal ) → odef (* A) x → Ordinal
|
|
|
48 fun→ : (x : Ordinal ) → odef (* B) x → Ordinal
|
|
|
49 funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt )
|
|
|
50 funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt )
|
|
|
51 fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
|
|
|
52 fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
|
|
1095
|
53
|
|
1124
|
54 ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b
|
|
|
55 ordbij-refl {a} refl = record {
|
|
|
56 fun← = λ x _ → x
|
|
|
57 ; fun→ = λ x _ → x
|
|
|
58 ; funB = λ x lt → lt
|
|
|
59 ; funA = λ x lt → lt
|
|
|
60 ; fiso← = λ x lt → refl
|
|
|
61 ; fiso→ = λ x lt → refl
|
|
|
62 }
|
|
|
63
|
|
1095
|
64 open Injection
|
|
1124
|
65 open OrdBijection
|
|
1095
|
66
|
|
|
67 record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
|
|
|
68 field
|
|
1387
|
69 y : Ordinal
|
|
|
70 ay : odef (* a) y
|
|
|
71 x=fy : x ≡ i→ iab _ ay
|
|
1095
|
72
|
|
1391
|
73 Image : (a : Ordinal) { b : Ordinal } → Injection a b → HOD
|
|
|
74 Image a {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00 } where
|
|
1387
|
75 im00 : {x : Ordinal } → IsImage a b iab x → x o< b
|
|
|
76 im00 {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ ( λ j k → j o< k) (trans &iso (sym x=fy)) &iso
|
|
|
77 (c<→o< (subst ( λ k → odef (* b) k) (sym &iso) (iB iab y ay)) )
|
|
1095
|
78
|
|
1391
|
79 record IsInverseImage (a b : Ordinal) (iab : Injection a b ) (x y : Ordinal ) : Set n where
|
|
|
80 field
|
|
|
81 ax : odef (* a) x
|
|
|
82 x=fy : y ≡ i→ iab x ax
|
|
|
83
|
|
|
84 InverseImage : {a : Ordinal} ( b : Ordinal ) → Injection a b → (y : Ordinal ) → HOD
|
|
|
85 InverseImage {a} b iab y = record { od = record { def = λ x → IsInverseImage a b iab x y } ; odmax = & (* a) ; <odmax = im00 } where
|
|
|
86 im00 : {x : Ordinal } → IsInverseImage a b iab x y → x o< & (* a)
|
|
|
87 im00 {x} record { ax = ax ; x=fy = x=fy } = odef< ax
|
|
|
88
|
|
|
89 Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a iab ⊆ * b
|
|
1387
|
90 Image⊆b {a} {b} iab {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k) (sym x=fy) (iB iab y ay)
|
|
431
|
91
|
|
|
92 _=c=_ : ( A B : HOD ) → Set n
|
|
1124
|
93 A =c= B = OrdBijection ( & A ) ( & B )
|
|
431
|
94
|
|
1095
|
95 c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?)
|
|
|
96 c=→≡ = ?
|
|
|
97
|
|
|
98 ≡→c= : {A B : HOD} → A ≡ B → A =c= B
|
|
|
99 ≡→c= = ?
|
|
|
100
|
|
1124
|
101 open import BAlgebra O
|
|
|
102
|
|
|
103 _-_ : (a b : Ordinal ) → Ordinal
|
|
|
104 a - b = & ( (* a) ＼ (* b) )
|
|
|
105
|
|
|
106 -→< : (a b : Ordinal ) → (a - b) o≤ a
|
|
1387
|
107 -→< a b = subst₂ (λ j k → j o≤ k) &iso &iso ( ⊆→o≤ ( λ {x} a-b → proj1 (subst ( λ k → odef k x) *iso a-b) ) )
|
|
|
108
|
|
|
109 b-a⊆b : {a b x : Ordinal } → odef (* (b - a)) x → odef (* b) x
|
|
|
110 b-a⊆b {a} {b} {x} lt with subst (λ k → odef k x) *iso lt
|
|
|
111 ... | ⟪ bx , ¬ax ⟫ = bx
|
|
|
112
|
|
|
113 open Data.Nat
|
|
1124
|
114
|
|
1388
|
115 Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b
|
|
1389
|
116 Injection-⊆ {a} {b} {c} le f = record { i→ = λ x cx → i→ f x (le cx) ; iB = λ x cx → iB f x (le cx)
|
|
|
117 ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq }
|
|
1388
|
118
|
|
1393
|
119 Injection-∙ : {a b c : Ordinal } → Injection a b → Injection b c → Injection a c
|
|
|
120 Injection-∙ {a} {b} {c} f g = record { i→ = λ x ax → i→ g (i→ f x ax) (iB f x ax) ; iB = λ x ax → iB g (i→ f x ax) (iB f x ax)
|
|
|
121 ; inject = λ x y ix iy eq → inject f x y ix iy (inject g (i→ f x ix) (i→ f y iy) (iB f x ix) (iB f y iy) eq) }
|
|
|
122
|
|
1124
|
123
|
|
|
124 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
|
|
|
125 Bernstein {a} {b} iab iba = be00 where
|
|
|
126 be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥
|
|
|
127 be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ }
|
|
|
128 ind a b a<b iab iba where
|
|
|
129 ind :(x : Ordinal) →
|
|
|
130 ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) →
|
|
|
131 (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥
|
|
1392
|
132 ind a prev b x<b (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject })
|
|
|
133 ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })= prev _ ? _ ? Uf fU where
|
|
|
134
|
|
|
135 gf : Injection a a
|
|
|
136 gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax)
|
|
|
137 ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) }
|
|
|
138
|
|
|
139 data gfImage : (i : ℕ) (x : Ordinal) → Set n where
|
|
|
140 a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x
|
|
|
141 next-gf : {x y : Ordinal} → {i : ℕ} → (gfiy : gfImage i y )→ (ix : IsImage a a gf x) → gfImage (suc i) x
|
|
|
142
|
|
|
143 a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x
|
|
|
144 a∋gfImage 0 {x} (a-g ax ¬ib) = ax
|
|
|
145 a∋gfImage (suc i) {x} (next-gf lt record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) )
|
|
|
146
|
|
|
147 C : ℕ → HOD -- Image {& (C i)} {a} (gf i) does not work
|
|
|
148 C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) }
|
|
|
149
|
|
|
150 record CN (x : Ordinal) : Set n where
|
|
|
151 field
|
|
|
152 i : ℕ
|
|
|
153 gfix : gfImage i x
|
|
|
154
|
|
|
155 UC : HOD
|
|
|
156 UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt)) }
|
|
1393
|
157
|
|
|
158 b-UC : HOD
|
|
|
159 b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt) }
|
|
1392
|
160
|
|
|
161 -- UC ⊆ * a
|
|
|
162 -- f : UC → Image f UC is injection
|
|
|
163 -- g : Image f UC → UC is injection
|
|
|
164
|
|
|
165 UC⊆a : * (& UC) ⊆ * a
|
|
|
166 UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02) where
|
|
|
167 be02 : CN x
|
|
|
168 be02 = subst (λ k → odef k x) *iso lt
|
|
|
169
|
|
1393
|
170 b-UC⊆b : * (& b-UC) ⊆ * b
|
|
|
171 b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )
|
|
|
172
|
|
1394
|
173 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
|
174
|
|
|
175 fab-refl : {x : Ordinal } → {ax ax1 : odef (* a) x} → fab x ax ≡ fab x ax1
|
|
|
176 fab-refl {x} {ax} {ax1} = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))
|
|
|
177
|
|
|
178 fba-refl : {x : Ordinal } → {bx bx1 : odef (* b) x} → fba x bx ≡ fba x bx1
|
|
|
179 fba-refl {x} {bx} {bx1} = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))
|
|
|
180
|
|
1396
|
181 fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → fab x ax ≡ fab y ax1
|
|
|
182 fab-eq {x} {x} {ax} {ax1} refl = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))
|
|
|
183
|
|
|
184 fba-eq : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y} → x ≡ y → fba x bx ≡ fba y bx1
|
|
|
185 fba-eq {x} {x} {bx} {bx1} refl = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))
|
|
|
186
|
|
1393
|
187 be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) ))
|
|
1396
|
188 be10 = record { i→ = be12 ; iB = be13 ; inject = be14 } where
|
|
1393
|
189 be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal
|
|
|
190 be12 x lt = i→ g x (proj1 be02) where
|
|
|
191 be02 : odef (* b) x ∧ ( ¬ CN x )
|
|
|
192 be02 = subst (λ k → odef k x) *iso lt
|
|
1394
|
193 be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt)
|
|
|
194 be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-refl } where
|
|
|
195 be02 : odef (* b) x ∧ ( ¬ CN x )
|
|
|
196 be02 = subst (λ k → odef k x) *iso lt
|
|
1396
|
197 be14 : (x y : Ordinal) (ltx : odef (* (& b-UC)) x) (lty : odef (* (& b-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y
|
|
|
198 be14 x y ltx lty eq = inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq
|
|
1393
|
199
|
|
|
200 be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC)
|
|
1396
|
201 be11 = record { i→ = be13 ; iB = be14 ; inject = be15 } where
|
|
1393
|
202 be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal
|
|
|
203 be13 x lt with subst (λ k → odef k x) *iso lt
|
|
1396
|
204 ... | record { y = y ; ay = ay ; x=fy = x=fy } = y -- g⁻¹ x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay))
|
|
|
205 be14 : (x : Ordinal) (lt : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) → odef (* (& b-UC)) (be13 x lt)
|
|
|
206 be14 x lt with subst (λ k → odef k x) *iso lt
|
|
|
207 ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay
|
|
|
208 be15 : (x y : Ordinal) (ltx : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x)
|
|
|
209 (lty : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) y) →
|
|
|
210 be13 x ltx ≡ be13 y lty → x ≡ y
|
|
|
211 be15 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty
|
|
|
212 ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy }
|
|
|
213 = trans x=fix (trans ( fba-eq eq ) (sym x=fiy ) )
|
|
|
214
|
|
|
215 b-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& b-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx) ≡ x
|
|
|
216 b-UC-iso0 x cx with subst (λ k → odef k ( i→ be10 x cx ) ) *iso (iB be10 x cx)
|
|
|
217 ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ (proj1 be03) (proj1 be02) (sym x=fy) where
|
|
|
218 be02 : odef (* b) x ∧ ( ¬ CN x )
|
|
|
219 be02 = subst (λ k → odef k x) *iso cx
|
|
|
220 be03 : odef (* b) y ∧ ( ¬ CN y )
|
|
|
221 be03 = subst (λ k → odef k y) *iso ay
|
|
|
222
|
|
|
223 b-UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g)))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx) ≡ x
|
|
|
224 b-UC-iso1 x cx with subst (λ k → odef k x ) *iso cx
|
|
|
225 ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
|
|
1393
|
226
|
|
1392
|
227 fUC = & (Image (& UC) {b} (Injection-⊆ UC⊆a f) )
|
|
|
228 -- C n → f (C n)
|
|
|
229 fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a f) ))
|
|
1393
|
230 fU = record { i→ = be00 ; iB = λ x lt → be50 x lt ; inject = be51 } where
|
|
1392
|
231 be00 : (x : Ordinal) (lt : odef (* (& UC)) x) → Ordinal
|
|
|
232 be00 x lt = be03 where
|
|
|
233 be02 : CN x
|
|
|
234 be02 = subst (λ k → odef k x) *iso lt
|
|
|
235 be03 : Ordinal
|
|
|
236 be03 with CN.i be02 | CN.gfix be02
|
|
|
237 ... | zero | a-g {x} ax ¬ib = fab x ax
|
|
|
238 ... | suc i | next-gf {x} gfiy record { y = y ; ay = ay ; x=fy = x=fy }
|
|
|
239 = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) ))
|
|
|
240 be50 : (x : Ordinal) (lt : odef (* (& UC)) x)
|
|
|
241 → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f )))) (be00 x lt)
|
|
|
242 be50 x lt1 = subst (λ k → odef k (be00 x lt1 )) (sym *iso) be03 where
|
|
|
243 be02 : CN x
|
|
|
244 be02 = subst (λ k → odef k x) *iso lt1
|
|
|
245 be03 : odef (Image (& UC) (Injection-⊆ UC⊆a f )) (be00 x lt1 )
|
|
|
246 be03 with CN.i be02 | CN.gfix be02
|
|
|
247 ... | zero | a-g {x} ax ¬ib = record { y = x ; ay = lt1 ; x=fy = fab-refl }
|
|
|
248 ... | suc i | next-gf {x} gfiy record { y = y ; ay = ay ; x=fy = x=fy } = record { y = _ ; ay = lt1 ; x=fy = fab-refl }
|
|
|
249
|
|
1393
|
250 be51 : (x y : Ordinal) (ltx : odef (* (& UC)) x) (lty : odef (* (& UC)) y) → be00 x ltx ≡ be00 y lty → x ≡ y
|
|
|
251 be51 x y ltx lty eq = be04 where
|
|
|
252 be0x : CN x
|
|
|
253 be0x = subst (λ k → odef k x) *iso ltx
|
|
|
254 be0y : CN y
|
|
|
255 be0y = subst (λ k → odef k y) *iso lty
|
|
|
256 be04 : x ≡ y
|
|
|
257 be04 with CN.i be0x | CN.gfix be0x | CN.i be0y | CN.gfix be0y
|
|
|
258 ... | 0 | a-g ax ¬ib | 0 | a-g ax₁ ¬ib₁ = fab-inject _ _ ax ax₁ eq
|
|
|
259 ... | 0 | a-g ax ¬ib | suc j | next-gf gfyi iy = fab-inject _ _ ax ay eq where
|
|
|
260 ay : odef (* a) y
|
|
|
261 ay = a∋gfImage (suc j) (next-gf gfyi iy )
|
|
|
262 ... | suc i | next-gf gfxi ix | 0 | a-g ay ¬ib = fab-inject _ _ ax ay eq where
|
|
|
263 ax : odef (* a) x
|
|
|
264 ax = a∋gfImage (suc i) (next-gf gfxi ix )
|
|
|
265 ... | suc i | next-gf gfxi ix | suc j | next-gf gfyi iy = fab-inject _ _ ax ay eq where
|
|
|
266 ax : odef (* a) x
|
|
|
267 ax = a∋gfImage (suc i) (next-gf gfxi ix )
|
|
|
268 ay : odef (* a) y
|
|
|
269 ay = a∋gfImage (suc j) (next-gf gfyi iy )
|
|
|
270
|
|
|
271
|
|
1396
|
272 -- f (C n) → g (f (C n) ) ≡ C (suc i)
|
|
1392
|
273 Uf : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a f))) (& UC)
|
|
1395
|
274 Uf = record { i→ = be00 ; iB = be01 ; inject = ? } where
|
|
1393
|
275 be00 : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
|
|
1395
|
276 be00 x lt with subst (λ k → odef k x ) *iso lt
|
|
|
277 ... | record { y = y ; ay = ay ; x=fy = x=fy } = fba x (subst (λ k → odef (* b) k ) (trans fab-refl (sym x=fy)) (b∋fab y (UC⊆a ay) ) )
|
|
|
278 be01 : (x : Ordinal) → (lt : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ) → odef (* (& UC)) (be00 x lt)
|
|
1396
|
279 be01 x lt with subst (λ k → odef k x) *iso lt
|
|
|
280 ... | record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ (λ j k → odef j k ) (sym *iso) fba-refl
|
|
|
281 record { i = suc (CN.i be04 ) ; gfix = next-gf (CN.gfix be04) record { y = y ; ay = a∋gfImage (CN.i be04) (CN.gfix be04) ; x=fy = be06 } }
|
|
|
282 where
|
|
1395
|
283 be04 : CN y
|
|
|
284 be04 = subst (λ k → odef k y) *iso ay
|
|
1396
|
285 bx : odef (* b) x
|
|
|
286 bx = subst (λ k → odef (* b) k ) (sym x=fy) ( b∋fab y (a∋gfImage (CN.i be04) (CN.gfix be04)))
|
|
|
287 be06 : fba x bx ≡ fba (fab y (a∋gfImage (CN.i be04) (CN.gfix be04))) (b∋fab y (a∋gfImage (CN.i be04) (CN.gfix be04)) )
|
|
|
288 be06 = fba-eq x=fy
|
|
|
289 be02 : (x y : Ordinal) (ltx : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a (record { i→ = fab ; iB = b∋fab ; inject = fab-inject }))))) x)
|
|
|
290 (lty : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a (record { i→ = fab ; iB = b∋fab ; inject = fab-inject }))))) y) →
|
|
|
291 be00 x ltx ≡ be00 y lty → x ≡ y
|
|
|
292 be02 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty
|
|
|
293 ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy }
|
|
|
294 = inject g _ _ bx by (trans fba-refl (trans eq fba-refl )) where
|
|
|
295 be04 : CN ix
|
|
|
296 be04 = subst (λ k → odef k ix) *iso aix
|
|
|
297 be06 : CN iy
|
|
|
298 be06 = subst (λ k → odef k iy) *iso aiy
|
|
|
299 bx : odef (* b) x
|
|
|
300 bx = subst (λ k → odef (* b) k ) (sym x=fix) ( b∋fab ix (a∋gfImage (CN.i be04) (CN.gfix be04)))
|
|
|
301 by : odef (* b) y
|
|
|
302 by = subst (λ k → odef (* b) k ) (sym x=fiy) ( b∋fab iy (a∋gfImage (CN.i be06) (CN.gfix be06)))
|
|
|
303
|
|
|
304 UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x
|
|
1397
|
305 UC-iso0 x cx = ? where
|
|
|
306 be02 : CN x
|
|
|
307 be02 = subst (λ k → odef k x) *iso cx
|
|
|
308 be03 : i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x
|
|
|
309 be03 with CN.i be02 | CN.gfix be02 | iB fU x cx
|
|
|
310 ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb
|
|
|
311 ... | record { y = y ; ay = ay ; x=fy = x=fy } = ? -- fba (fab x _) _ = x
|
|
|
312 be03 | suc i | next-gf s ix | cb with subst (λ k → odef k (fab x _) ) *iso cb
|
|
|
313 ... | record { y = y ; ay = ay ; x=fy = x=fy } = ?
|
|
1396
|
314
|
|
|
315 UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) → i→ fU ( i→ Uf x cx ) (iB Uf x cx) ≡ x
|
|
|
316 UC-iso1 = ?
|
|
|
317
|
|
1392
|
318
|
|
1124
|
319 be00 : OrdBijection a b
|
|
|
320 be00 with trio< a b
|
|
|
321 ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )
|
|
|
322 ... | tri≈ ¬a b ¬c = ordbij-refl b
|
|
|
323 ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab )
|
|
1095
|
324
|
|
431
|
325 _c<_ : ( A B : HOD ) → Set n
|
|
|
326 A c< B = ¬ ( Injection (& A) (& B) )
|
|
|
327
|
|
|
328 Card : OD
|
|
1124
|
329 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection a x }
|
|
431
|
330
|
|
1387
|
331 record Cardinal (a : Ordinal ) : Set (Level.suc n) where
|
|
431
|
332 field
|
|
|
333 card : Ordinal
|
|
1124
|
334 ciso : OrdBijection a card
|
|
|
335 cmax : (x : Ordinal) → card o< x → ¬ OrdBijection a x
|
|
431
|
336
|
|
1095
|
337 Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t
|
|
431
|
338 Cardinal∈ = {!!}
|
|
|
339
|
|
|
340 Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t )
|
|
|
341 Cardinal⊆ = {!!}
|
|
|
342
|
|
|
343 Cantor1 : { u : HOD } → u c< Power u
|
|
|
344 Cantor1 = {!!}
|
|
|
345
|
|
|
346 Cantor2 : { u : HOD } → ¬ ( u =c= Power u )
|
|
|
347 Cantor2 = {!!}
|
|
1095
|
348
|
|
|
349
|
|
|
350
|
|
|
351
|
