|
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
|
|
|
73 Image : { a b : Ordinal } → Injection a b → HOD
|
|
1387
|
74 Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00 } where
|
|
|
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
|
|
1387
|
79 Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image iab ⊆ * b
|
|
|
80 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
|
81
|
|
|
82 _=c=_ : ( A B : HOD ) → Set n
|
|
1124
|
83 A =c= B = OrdBijection ( & A ) ( & B )
|
|
431
|
84
|
|
1095
|
85 c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?)
|
|
|
86 c=→≡ = ?
|
|
|
87
|
|
|
88 ≡→c= : {A B : HOD} → A ≡ B → A =c= B
|
|
|
89 ≡→c= = ?
|
|
|
90
|
|
1124
|
91 open import BAlgebra O
|
|
|
92
|
|
|
93 _-_ : (a b : Ordinal ) → Ordinal
|
|
|
94 a - b = & ( (* a) ＼ (* b) )
|
|
|
95
|
|
|
96 -→< : (a b : Ordinal ) → (a - b) o≤ a
|
|
1387
|
97 -→< a b = subst₂ (λ j k → j o≤ k) &iso &iso ( ⊆→o≤ ( λ {x} a-b → proj1 (subst ( λ k → odef k x) *iso a-b) ) )
|
|
|
98
|
|
|
99 b-a⊆b : {a b x : Ordinal } → odef (* (b - a)) x → odef (* b) x
|
|
|
100 b-a⊆b {a} {b} {x} lt with subst (λ k → odef k x) *iso lt
|
|
|
101 ... | ⟪ bx , ¬ax ⟫ = bx
|
|
|
102
|
|
|
103 open Data.Nat
|
|
1124
|
104
|
|
1388
|
105 Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b
|
|
1389
|
106 Injection-⊆ {a} {b} {c} le f = record { i→ = λ x cx → i→ f x (le cx) ; iB = λ x cx → iB f x (le cx)
|
|
|
107 ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq }
|
|
1388
|
108
|
|
1124
|
109 Bernstein1 : {a b : Ordinal } → a o< b → Injection a b ∧ Injection b a → Injection (b - a) b ∧ Injection b (b - a)
|
|
1387
|
110 Bernstein1 {a} {b} a<b ⟪ f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject } , g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject } ⟫
|
|
|
111 = ⟪ record { i→ = f0 ; iB = b∋f0 ; inject = f0-inject } , record { i→ = f1 ; iB = b∋f1 ; inject = f1-inject } ⟫ where
|
|
|
112
|
|
1388
|
113 gf : Injection a a
|
|
|
114 gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax)
|
|
|
115 ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) }
|
|
|
116
|
|
|
117 data gfImage : (i : ℕ) (x : Ordinal) → Set n where
|
|
|
118 a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x
|
|
|
119 next-gf : {x y : Ordinal} → {i : ℕ} → (gfiy : gfImage i y )→ (ix : IsImage a a gf x) → gfImage (suc i) x
|
|
|
120
|
|
|
121 a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x
|
|
|
122 a∋gfImage 0 {x} (a-g ax ¬ib) = ax
|
|
|
123 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) )
|
|
|
124
|
|
|
125 C : ℕ → HOD -- Image {& (C i)} {a} (gf i) does not work
|
|
|
126 C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) }
|
|
1387
|
127
|
|
|
128 record CN (x : Ordinal) : Set n where
|
|
|
129 field
|
|
|
130 i : ℕ
|
|
1388
|
131 gfix : gfImage i x
|
|
1387
|
132
|
|
|
133 UC : HOD
|
|
1388
|
134 UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt)) }
|
|
|
135
|
|
|
136 -- UC ⊆ * a
|
|
|
137 -- f : UC → Image f UC is injection
|
|
|
138 -- g : Image f UC → UC is injection
|
|
|
139
|
|
|
140 UC⊆a : * (& UC) ⊆ * a
|
|
1389
|
141 UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02) where
|
|
|
142 be02 : CN x
|
|
|
143 be02 = subst (λ k → odef k x) *iso lt
|
|
1388
|
144
|
|
|
145 fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a f) ))
|
|
1390
|
146 fU = record { i→ = λ x lt → IsImage.y (be10 x lt) ; iB = λ x lt → be20 (IsImage.y (be10 x lt)) (be21 x lt) ; inject = ? } where
|
|
|
147 be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → IsImage _ _ (Injection-⊆ UC⊆a f) x
|
|
|
148 be20 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (Injection-⊆ UC⊆a f)))) x
|
|
|
149 be20 x lt = subst ( λ k → odef k x ) (sym *iso) (be10 x lt )
|
|
|
150 be21 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& UC)) (IsImage.y (be10 x lt))
|
|
|
151 be21 = ?
|
|
|
152 g⁻¹ : { x : Ordinal} → odef (* b) x → Ordinal
|
|
|
153 g⁻¹ = ?
|
|
|
154 a∋g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → odef (* a) (g⁻¹ bx )
|
|
|
155 a∋g⁻¹ = ?
|
|
|
156 is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → x ≡ fab (g⁻¹ bx ) (a∋g⁻¹ bx)
|
|
|
157 is-g⁻¹ = ?
|
|
|
158 be10 x lt = record { y = be14 _ (CN.gfix be02) ; ay = ? ; x=fy = ? } where
|
|
1389
|
159 be02 : CN x
|
|
|
160 be02 = subst (λ k → odef k x) *iso lt
|
|
|
161 be14 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal
|
|
1390
|
162 be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be14 i gfi )
|
|
1389
|
163 be14 0 {x} (a-g ax ¬ib) = x
|
|
1390
|
164 be14 (suc i) {x} (next-gf lt _) = fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
|
|
|
165 be05 0 {x} (a-g ax ¬ib) = ax
|
|
|
166 be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
|
|
|
167 be16 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 i gfi)
|
|
|
168 be16 0 {x} (a-g ax ¬ib) = record { y = g⁻¹ (b∋fab x ax)
|
|
|
169 ; ay = subst (λ k → odef k ( g⁻¹ (b∋fab x ax))) (sym *iso) record { i = 0 ; gfix = a-g ? ? } ; x=fy = is-g⁻¹ ? }
|
|
|
170 be16 (suc i) {x} (next-gf ix ix₁) = record { y = ? ; ay = ? ; x=fy = ? }
|
|
|
171 be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 _ (CN.gfix be02))
|
|
|
172 be11 = be16 _ (CN.gfix be02)
|
|
1388
|
173
|
|
|
174 gU : Injection (& (Image {& UC} {b} (Injection-⊆ UC⊆a f))) (& UC)
|
|
|
175 gU = ?
|
|
1387
|
176
|
|
|
177 -- Injection (b - a) b
|
|
|
178 f0 : (x : Ordinal) → odef (* (b - a)) x → Ordinal
|
|
|
179 f0 x lt with subst (λ k → odef k x) *iso lt
|
|
|
180 ... | ⟪ bx , ¬ax ⟫ = fab (fba x bx) (a∋fba x bx)
|
|
|
181 b∋f0 : (x : Ordinal) (lt : odef (* (b - a)) x) → odef (* b) (f0 x lt)
|
|
|
182 b∋f0 x lt with subst (λ k → odef k x) *iso lt
|
|
|
183 ... | ⟪ bx , ¬ax ⟫ = b∋fab (fba x bx) (a∋fba x bx)
|
|
|
184 f0-inject : (x y : Ordinal) (ltx : odef (* (b - a)) x) (lty : odef (* (b - a)) y) → f0 x ltx ≡ f0 y lty → x ≡ y
|
|
|
185 f0-inject x y ltx lty eq = fba-inject _ _ (b-a⊆b ltx) (b-a⊆b lty) ( fab-inject _ _ (a∋fba x (b-a⊆b ltx)) (a∋fba y (b-a⊆b lty)) eq )
|
|
|
186
|
|
|
187 -- Injection b (b - a)
|
|
|
188 f1 : (x : Ordinal) → odef (* b) x → Ordinal
|
|
|
189 f1 x lt = ?
|
|
|
190 b∋f1 : (x : Ordinal) (lt : odef (* b) x) → odef (* (b - a)) (f1 x lt)
|
|
|
191 b∋f1 x lt = ?
|
|
|
192 f1-inject : (x y : Ordinal) (ltx : odef (* b) x) (lty : odef (* b) y) → f1 x ltx ≡ f1 y lty → x ≡ y
|
|
|
193 f1-inject x y ltx lty eq = ?
|
|
1124
|
194
|
|
|
195 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
|
|
|
196 Bernstein {a} {b} iab iba = be00 where
|
|
|
197 be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥
|
|
|
198 be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ }
|
|
|
199 ind a b a<b iab iba where
|
|
|
200 ind :(x : Ordinal) →
|
|
|
201 ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) →
|
|
|
202 (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥
|
|
1387
|
203 ind x prev b x<b ixb ibx = prev _ be01 _ be02 (proj1 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) (proj2 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) where
|
|
|
204 be01 : (b - x) o< x
|
|
|
205 be01 = ?
|
|
|
206 be02 : (b - x) o< b
|
|
|
207 be02 = ?
|
|
1124
|
208 be00 : OrdBijection a b
|
|
|
209 be00 with trio< a b
|
|
|
210 ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )
|
|
|
211 ... | tri≈ ¬a b ¬c = ordbij-refl b
|
|
|
212 ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab )
|
|
1095
|
213
|
|
431
|
214 _c<_ : ( A B : HOD ) → Set n
|
|
|
215 A c< B = ¬ ( Injection (& A) (& B) )
|
|
|
216
|
|
|
217 Card : OD
|
|
1124
|
218 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection a x }
|
|
431
|
219
|
|
1387
|
220 record Cardinal (a : Ordinal ) : Set (Level.suc n) where
|
|
431
|
221 field
|
|
|
222 card : Ordinal
|
|
1124
|
223 ciso : OrdBijection a card
|
|
|
224 cmax : (x : Ordinal) → card o< x → ¬ OrdBijection a x
|
|
431
|
225
|
|
1095
|
226 Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t
|
|
431
|
227 Cardinal∈ = {!!}
|
|
|
228
|
|
|
229 Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t )
|
|
|
230 Cardinal⊆ = {!!}
|
|
|
231
|
|
|
232 Cantor1 : { u : HOD } → u c< Power u
|
|
|
233 Cantor1 = {!!}
|
|
|
234
|
|
|
235 Cantor2 : { u : HOD } → ¬ ( u =c= Power u )
|
|
|
236 Cantor2 = {!!}
|
|
1095
|
237
|
|
|
238
|
|
|
239
|
|
|
240
|
